new cicEnvironment implementation

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 0cb8aceadbaaf3a14bbc43d95fd65897b7a53468..92b89a679c987c293e4395f993930707c5ad3d2b 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -204,7 +204,7 @@ let
 =
  let module C = Cic in
   let params =
-    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 (_,_,_,params)
        | C.CurrentProof (_,_,_,_,params)
@@ -220,7 +220,7 @@ let
          [],[] -> []
        | uri::tl,[] ->
           let ty =
-           let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+           let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
               match o with
                  C.Variable (_,_,ty,_) ->
                    CicSubstitution.subst_vars !exp_named_subst_diff ty
@@ -492,7 +492,7 @@ let elim_tac ~term =
      let eliminator_uri =
       let buri = U.buri_of_uri uri in
       let name = 
-       let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+       let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
        match o with
           C.InductiveDefinition (tys,_,_) ->
            let (name,_,_,_) = List.nth tys typeno in