new cicEnvironment implementation

[helm.git] / helm / ocaml / tactics / proofEngineReduction.ml

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index e7975793fa748d8d4f8cd46720f0aa7ec0b015ee..e53d69048dd0261210b71aee19bff913305467a5 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -389,7 +389,7 @@ let reduce context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-       (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+       (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         match o with
            C.Constant _ -> raise ReferenceToConstant
          | C.CurrentProof _ -> raise ReferenceToCurrentProof
@@ -430,7 +430,7 @@ let reduce context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
          match o with
             C.Constant (_,Some body,_,_) ->
              (reduceaux context l
@@ -492,7 +492,7 @@ let reduce context =
             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
              let (arity, r) =
-              let o,_ = CicEnvironment.get_obj mutind CicUniv.empty_ugraph in
+              let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
                 match o with
                      C.InductiveDefinition (tl,_,r) ->
                        let (_,_,arity,_) = List.nth tl i in
@@ -615,7 +615,7 @@ let simpl context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
          match o with
             C.Constant _ -> raise ReferenceToConstant
           | C.CurrentProof _ -> raise ReferenceToCurrentProof
@@ -656,7 +656,7 @@ let simpl context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
          match o with
            C.Constant (_,Some body,_,_) ->
             try_delta_expansion l
@@ -715,7 +715,7 @@ let simpl context =
             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
              let (arity, r) =
-              let o,_ = CicEnvironment.get_obj mutind CicUniv.empty_ugraph in
+              let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
                 match o with
                      C.InductiveDefinition (tl,ingredients,r) ->
                        let (_,_,arity,_) = List.nth tl i in