use uniform naming for referencing cicNotation* modules

[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 f30e3c53c0314819a825f62310b3fd28cbc0ae2c..148450f5d17f1375b275186f3c08d807d0780a6b 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -47,76 +47,68 @@ let rec split l n =
 ;;
 
 let rec type_of_constant uri ugraph =
-  let module C = Cic in
-  let module R = CicReduction in
-  let module U = UriManager in
-    (*
-      let obj =
-      try
-      CicEnvironment.get_cooked_obj uri
-      with Not_found -> assert false
-      in
-    *)
-  let obj,u= CicEnvironment.get_obj ugraph uri in
-    match obj with
-       C.Constant (_,_,ty,_,_) -> ty,u
-      | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
-      | _ ->
-         raise
-           (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+  let _ = CicTypeChecker.typecheck uri in
+  let obj,u =
+   try
+    CicEnvironment.get_cooked_obj ugraph uri
+   with Not_found -> assert false
+  in
+   match obj with
+      C.Constant (_,_,ty,_,_) -> ty,u
+    | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
+    | _ ->
+       raise
+        (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
 
 and type_of_variable uri ugraph =
   let module C = Cic in
   let module R = CicReduction in
   let module U = UriManager in
-    (*
-      let obj =
-      try
-      CicEnvironment.get_cooked_obj uri
-      with Not_found -> assert false
-      in
-    *)
-  let obj,u = CicEnvironment.get_obj ugraph uri in
-    match obj with
-       C.Variable (_,_,ty,_,_) -> ty,u
-      |  _ ->
-          raise
-           (RefineFailure
-               ("Unknown variable definition " ^ UriManager.string_of_uri uri))
+  let _ = CicTypeChecker.typecheck uri in
+  let obj,u =
+   try
+    CicEnvironment.get_cooked_obj ugraph uri
+    with Not_found -> assert false
+  in
+   match obj with
+      C.Variable (_,_,ty,_,_) -> ty,u
+    | _ ->
+        raise
+         (RefineFailure
+          ("Unknown variable definition " ^ UriManager.string_of_uri uri))
 
 and type_of_mutual_inductive_defs uri i ugraph =
   let module C = Cic in
   let module R = CicReduction in
   let module U = UriManager in
-    (*
-      let obj =
-      try
-      CicEnvironment.get_cooked_obj uri
-      with Not_found -> assert false
-      in
-    *)
-  let obj,u = CicEnvironment.get_obj ugraph uri in
-    match obj with
-       C.InductiveDefinition (dl,_,_,_) ->
-         let (_,_,arity,_) = List.nth dl i in
-           arity,u
-      | _ ->
-         raise
-           (RefineFailure
-               ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
+  let _ = CicTypeChecker.typecheck uri in
+  let obj,u =
+   try
+    CicEnvironment.get_cooked_obj ugraph uri
+   with Not_found -> assert false
+  in
+   match obj with
+      C.InductiveDefinition (dl,_,_,_) ->
+        let (_,_,arity,_) = List.nth dl i in
+        arity,u
+    | _ ->
+       raise
+        (RefineFailure
+         ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
 
 and type_of_mutual_inductive_constr uri i j ugraph =
   let module C = Cic in
   let module R = CicReduction in
   let module U = UriManager in
-    (*
-      let obj =
-      try
-      CicEnvironment.get_cooked_obj uri
-      with Not_found -> assert false
-      in
-    *)
-  let obj,u = CicEnvironment.get_obj ugraph uri in
+  let _ = CicTypeChecker.typecheck uri in
+   let obj,u =
+    try
+     CicEnvironment.get_cooked_obj ugraph uri
+    with Not_found -> assert false
+   in
     match obj with
        C.InductiveDefinition (dl,_,_,_) ->
          let (_,_,_,cl) = List.nth dl i in
@@ -287,7 +279,7 @@ and type_of_aux' metasenv context t ugraph =
               * Moreover the inferred type is closer to the expected one. 
                *)
              C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
-                subst',metasenv',ugraph2
+                subst'',metasenv'',ugraph2
        | C.Appl (he::((_::_) as tl)) ->
            let he',hetype,subst',metasenv',ugraph1 = 
              type_of_aux subst metasenv context he ugraph 
@@ -342,7 +334,8 @@ and type_of_aux' metasenv context t ugraph =
            (* first, get the inductive type (and noparams) 
              * in the environment  *)
            let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
-             let obj,u = CicEnvironment.get_obj ugraph uri in
+              let _ = CicTypeChecker.typecheck uri in
+             let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
               match obj with
                  C.InductiveDefinition (l,expl_params,parsno,_) -> 
                    List.nth l i , expl_params, parsno, u
@@ -437,7 +430,7 @@ and type_of_aux' metasenv context t ugraph =
                (let candidate,ugraph5,metasenv,subst = 
                  let exp_name_subst, metasenv = 
                     let o,_ = 
-                      CicEnvironment.get_obj CicUniv.empty_ugraph uri 
+                      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri 
                     in
                     let uris = CicUtil.params_of_obj o in
                     List.fold_right (