new cicEnvironment implementation

[helm.git] / helm / ocaml / cic_omdoc / doubleTypeInference.ml

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
index 235d8d835b47f7aac01f9ebe91e0c9f2d1d6c2c1..e16aa789f2412c07af939f663478d5ac0af817e9 100644 (file)
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -266,7 +266,7 @@ let type_of_constant uri =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri CicUniv.empty_ugraph with
+   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
       CicEnvironment.CheckedObj (cobj,_) -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked constant")
@@ -281,7 +281,7 @@ let type_of_variable uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
-  match CicEnvironment.is_type_checked uri CicUniv.empty_ugraph with
+  match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
      CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),_) -> ty
    | CicEnvironment.UncheckedObj (C.Variable _) ->
       raise (NotWellTyped "Reference to an unchecked variable")
@@ -293,7 +293,7 @@ let type_of_mutual_inductive_defs uri i =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri CicUniv.empty_ugraph with
+   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
       CicEnvironment.CheckedObj (cobj,_) -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked inductive type")
@@ -310,7 +310,7 @@ let type_of_mutual_inductive_constr uri i j =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri CicUniv.empty_ugraph with
+   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
       CicEnvironment.CheckedObj (cobj,_) -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked constructor")
@@ -539,7 +539,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          let (cl,parsno) =
            let obj,_ =
              try
-               CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
+               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
              with Not_found -> assert false
            in
           match obj with
@@ -642,7 +642,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
   let uris_and_types =
      let obj,_ =
        try
-         CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
+         CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
        with Not_found -> assert false
      in
     match obj with
@@ -654,7 +654,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
         (function uri ->
            let obj,_ =
              try
-               CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
+               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
              with Not_found -> assert false
            in
            match obj with