snapshot (first version in which some extensions work, e.g. infix +)

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 38e822c33cd468f5169fad859ea7b43caeed29aa..4a6e6cadf798ef6fd16c154da24d513a4520a968 100644 (file)
--- 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 
@@ -477,7 +480,6 @@ and type_of_aux' metasenv context t ugraph =
                match candidate with
                | None -> raise (Uncertain "can't solve an higher order unification problem") 
                | Some candidate ->
-                   prerr_endline ("CANDIDATE=" ^ (CicPp.ppterm candidate));
                    let s,m,u = 
                      fo_unif_subst subst context metasenv 
                        candidate outtype ugraph5
@@ -606,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
@@ -878,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