X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=4a6e6cadf798ef6fd16c154da24d513a4520a968;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=8401ad5ade42339c3a24b56b06627273d10440cd;hpb=07b55308c296ec8537a176d829d161a975306e58;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 8401ad5ad..4a6e6cadf 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -47,6 +47,8 @@ let rec split l n =
 ;;
 
 let look_for_coercion src tgt =
+  None
+  (*
   if (src = (CicUtil.term_of_uri "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)")) &&
      (tgt = (CicUtil.term_of_uri "cic:/Coq/Reals/Rdefinitions/R.con")) 
   then
@@ -60,6 +62,7 @@ let look_for_coercion src tgt =
       (CicPp.ppterm tgt));
     None
     end
+  *)
 ;;
 
 
@@ -224,17 +227,17 @@ and type_of_aux' metasenv context t ugraph =
 		   canonical_context l ugraph 
                in
 		 (* trust or check ??? *)
-		 C.Meta (n,l'),CicSubstitution.lift_meta l' ty, 
+		 C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
                    subst', metasenv', ugraph1
 		   (* type_of_aux subst metasenv 
-		      context (CicSubstitution.lift_meta l term) *)
+		      context (CicSubstitution.subst_meta l term) *)
              with CicUtil.Subst_not_found _ ->
                let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
                let l',subst',metasenv', ugraph1 =
 		 check_metasenv_consistency n subst metasenv context
 		   canonical_context l ugraph
                in
-		 C.Meta (n,l'),CicSubstitution.lift_meta l' ty, 
+		 C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
                    subst', metasenv',ugraph1)
 	| C.Sort (C.Type tno) -> 
             let tno' = CicUniv.fresh() in 
@@ -605,14 +608,14 @@ and type_of_aux' metasenv context t ugraph =
 	function
             [] -> []
 	  | (Some (n,C.Decl t))::tl ->
-              (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+              (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 	  | (Some (n,C.Def (t,None)))::tl ->
-              (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
+              (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 	  | None::tl -> None::(aux (i+1) tl)
 	  | (Some (n,C.Def (t,Some ty)))::tl ->
               (Some (n,
-		     C.Def ((S.lift_meta l (S.lift i t)),
-			    Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
+		     C.Def ((S.subst_meta l (S.lift i t)),
+			    Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
       in
 	aux 1 canonical_context 
     in
@@ -877,6 +880,13 @@ and type_of_aux' metasenv context t ugraph =
     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) 
 ;;
 
+let type_of_aux' metasenv context term ugraph =
+  try 
+    type_of_aux' metasenv context term ugraph
+  with 
+    CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
+    
+
 (* DEBUGGING ONLY 
 let type_of_aux' metasenv context term =
  try