new cicEnvironment implementation

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

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 66a860a451115e14a8d745c5dd205cd87cd7bb56..781e6f5c8a183621be3300b651ac81710029f69e 100644 (file)
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -120,8 +120,8 @@ and injection1_tac ~term ~i =
  prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ;
  prerr_endline ("XXXX consno " ^ string_of_int consno) ;
                 let pattern =
-                      match fst(CicEnvironment.get_obj turi 
-                                 CicUniv.empty_ugraph ) with
+                      match fst(CicEnvironment.get_obj 
+                                 CicUniv.empty_ugraph turi ) with
                          C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx)  ->
                           let _,_,_,constructor_list = (List.nth ind_type_list typeno) in
                            let i_constr_id,_ = List.nth constructor_list (consno - 1) in
@@ -275,8 +275,8 @@ prerr_endline ("XXXX consno2 " ^ (string_of_int consno2)) ;
 
                    let pattern = 
                      (* a list of "True" except for the element in position consno2 which is "False" *)
-                     match fst(CicEnvironment.get_obj turi 
-                                CicUniv.empty_ugraph) with
+                     match fst(CicEnvironment.get_obj 
+                                CicUniv.empty_ugraph turi) with
                         C.InductiveDefinition (ind_type_list,_,nr_ind_params)  ->
 prerr_endline ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno)) ;
                          let _,_,_,constructor_list = (List.nth ind_type_list typeno) in