X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=979c9637ede5591125cf64dfa4786d08299a2648;hb=8b8606be3b086e20ead16ca7417da5f1c4e02e79;hp=54fde9a45a6d49c4d8e8d33ce88e98af2282f552;hpb=04ca589d65bcef6bd46cf4d277a748a12e09234b;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 54fde9a45..979c9637e 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -34,7 +34,6 @@ exception ListTooShort;;
 exception WrongUriToMutualInductiveDefinitions of string;;
 exception RelToHiddenHypothesis;;
 exception MetasenvInconsistency;;
-exception MutCaseFixAndCofixRefineNotImplemented;;
 exception WrongArgumentNumber;;
 
 let fdebug = ref 0;;
@@ -174,7 +173,7 @@ and type_of_aux' metasenv context t =
        let _,subst',metasenv' =
         type_of_aux subst metasenv context ty in
        let inferredty,subst'',metasenv'' =
-        type_of_aux subst' metasenv' context ty
+        type_of_aux subst' metasenv' context te
        in
         (try
           let subst''',metasenv''' =
@@ -342,8 +341,50 @@ and type_of_aux' metasenv context t =
              (subst,metasenv) outtypeinstances in
         CicMetaSubst.whd metasenv subst
           context (C.Appl(outtype::right_args@[term])),subst,metasenv
-   | C.Fix _
-   | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
+   | C.Fix (i,fl) ->
+      let subst,metasenv,types =
+       List.fold_left
+        (fun (subst,metasenv,types) (n,_,ty,_) ->
+          let _,subst',metasenv' = type_of_aux subst metasenv context ty in
+           subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
+        ) (subst,metasenv,[]) fl
+      in
+       let len = List.length types in
+       let context' = types@context in
+       let subst,metasenv =
+        List.fold_left
+         (fun (subst,metasenv) (name,x,ty,bo) ->
+           let ty_of_bo,subst,metasenv =
+            type_of_aux subst metasenv context' bo
+           in
+            Un.fo_unif_subst subst context' metasenv
+              ty_of_bo (CicMetaSubst.lift metasenv subst len ty)
+         ) (subst,metasenv) fl in
+      
+        let (_,_,ty,_) = List.nth fl i in
+         ty,subst,metasenv
+   | C.CoFix (i,fl) ->
+      let subst,metasenv,types =
+       List.fold_left
+        (fun (subst,metasenv,types) (n,ty,_) ->
+          let _,subst',metasenv' = type_of_aux subst metasenv context ty in
+           subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
+        ) (subst,metasenv,[]) fl
+      in
+       let len = List.length types in
+       let context' = types@context in
+       let subst,metasenv =
+        List.fold_left
+         (fun (subst,metasenv) (name,ty,bo) ->
+           let ty_of_bo,subst,metasenv =
+            type_of_aux subst metasenv context' bo
+           in
+            Un.fo_unif_subst subst context' metasenv
+              ty_of_bo (CicMetaSubst.lift metasenv subst len ty)
+         ) (subst,metasenv) fl in
+      
+        let (_,ty,_) = List.nth fl i in
+         ty,subst,metasenv
 
  (* check_metasenv_consistency checks that the "canonical" context of a
  metavariable is consitent - up to relocation via the relocation list l -