Termops API using EConstr.

1 files changed, 6 insertions, 5 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 3f0c01a29c..12d8e98c43 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -79,11 +79,12 @@ let up_to_delta = ref false (* true *)
 let general_decompose recognizer c =
   Proofview.Goal.enter { enter = begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
+  let sigma = project gl in
   let typc = type_of c in
   tclTHENS (cut typc)
     [ tclTHEN (intro_using tmphyp_name)
          (onLastHypId
-	    (ifOnHyp recognizer (general_decompose_aux recognizer)
+	    (ifOnHyp (recognizer sigma) (general_decompose_aux (recognizer sigma))
 	      (fun id -> clear [id])));
        exact_no_check c ]
   end }
@@ -102,17 +103,17 @@ let head_in indl t gl =
 let decompose_these c l =
   Proofview.Goal.enter { enter = begin fun gl ->
   let indl = List.map (fun x -> x, Univ.Instance.empty) l in
-  general_decompose (fun (_,t) -> head_in indl t gl) c
+  general_decompose (fun sigma (_,t) -> head_in indl t gl) c
   end }
 
 let decompose_and c =
   general_decompose
-    (fun (_,t) -> is_record t)
+    (fun sigma (_,t) -> is_record sigma t)
     c
 
 let decompose_or c =
   general_decompose
-    (fun (_,t) -> is_disjunction t)
+    (fun sigma (_,t) -> is_disjunction sigma t)
     c
 
 let h_decompose l c = decompose_these c l
@@ -133,7 +134,7 @@ let induction_trailer abs_i abs_j bargs =
        (fun id ->
           Proofview.Goal.nf_enter { enter = begin fun gl ->
 	  let idty = pf_unsafe_type_of gl (mkVar id) in
-	  let fvty = global_vars (pf_env gl) idty in
+	  let fvty = global_vars (pf_env gl) (project gl) (EConstr.of_constr idty) in
 	  let possible_bring_hyps =
 	    (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
           in