unsafe_type_of -> type_of in Tactics.intro_decomp_eq (hipattern changes)

4 files changed, 32 insertions, 30 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 96b61b6994..65f23ab0e4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1069,7 +1069,8 @@ let onEquality with_evars tac (c,lbindc) =
   let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
   let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
-  let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in
+  (* FIXME evar leak *)
+  let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in
   tclTHEN
     (Proofview.Unsafe.tclEVARS eq_clause'.evd)
     (tac (eq,eqn,eq_args) eq_clause')
@@ -1341,7 +1342,7 @@ let inject_if_homogenous_dependent_pair ty =
   Proofview.Goal.enter begin fun gl ->
   try
     let sigma = Tacmach.New.project gl in
-    let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
+    let eq,u,(t,t1,t2) = pf_apply find_this_eq_data_decompose gl ty in
     (* fetch the informations of the  pair *)
     let sigTconstr   = Coqlib.(lib_ref "core.sigT.type") in
     let existTconstr = Coqlib.lib_ref    "core.sigT.intro" in
@@ -1603,7 +1604,7 @@ let cutSubstInConcl l2r eqn =
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
-  let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
+  let (lbeq,u,(t,e1,e2)) = pf_apply find_eq_data_decompose gl eqn in
   let typ = pf_concl gl in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in
@@ -1620,7 +1621,7 @@ let cutSubstInHyp l2r eqn id =
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
-  let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
+  let (lbeq,u,(t,e1,e2)) = pf_apply find_eq_data_decompose gl eqn in
   let typ = pf_get_hyp_typ id gl in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in
@@ -1715,7 +1716,7 @@ let is_eq_x gl x d =
     | _ -> false
     in
     let c = pf_nf_evar gl (NamedDecl.get_type d) in
-    let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
+    let (_,lhs,rhs) = pi3 (pf_apply find_eq_data_decompose gl c) in
     if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true));
     if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false))
   with Constr_matching.PatternMatchingFailure ->
@@ -1812,7 +1813,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
   let find_equations gl =
     let env = Proofview.Goal.env gl in
     let sigma = project gl in
-    let find_eq_data_decompose = find_eq_data_decompose gl in
+    let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in
     let select_equation_name decl =
       try
         let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
@@ -1837,7 +1838,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
     Proofview.Goal.enter begin fun gl ->
     let sigma = project gl in
     let env = Proofview.Goal.env gl in
-    let find_eq_data_decompose = find_eq_data_decompose gl in
+    let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in
     let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
     let _,_,(_,x,y) = find_eq_data_decompose c in
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
@@ -1863,7 +1864,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
    let-ins *)
   Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
-  let find_eq_data_decompose = find_eq_data_decompose gl in
+  let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in
   let test (_,c) =
     try
       let lbeq,u,(_,x,y) = find_eq_data_decompose c in
@@ -1887,19 +1888,19 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
 
 let cond_eq_term_left c t gl =
   try
-    let (_,x,_) = pi3 (find_eq_data_decompose gl t) in
+    let (_,x,_) = pi3 (pf_apply find_eq_data_decompose gl t) in
     if pf_conv_x gl c x then true else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term_right c t gl =
   try
-    let (_,_,x) = pi3 (find_eq_data_decompose gl t) in
+    let (_,_,x) = pi3 (pf_apply find_eq_data_decompose gl t) in
     if pf_conv_x gl c x then false else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term c t gl =
   try
-    let (_,x,y) = pi3 (find_eq_data_decompose gl t) in
+    let (_,x,y) = pi3 (pf_apply find_eq_data_decompose gl t) in
     if pf_conv_x gl c x then true
     else if pf_conv_x gl c y then false
     else failwith "not convertible"
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 90a9a7acd9..1f68117a76 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -19,7 +19,6 @@ open Inductiveops
 open Constr_matching
 open Coqlib
 open Declarations
-open Tacmach.New
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -452,26 +451,26 @@ let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *)
   let hd,u = destInd sigma (fst (destApp sigma eqn)) in
     d,u,k
 
-let extract_eq_args gl = function
+let extract_eq_args env sigma = function
   | MonomorphicLeibnizEq (e1,e2) ->
-      let t = pf_unsafe_type_of gl e1 in (t,e1,e2)
+      let t = Typing.unsafe_type_of env sigma e1 in (t,e1,e2)
   | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
   | HeterogenousEq (t1,e1,t2,e2) ->
-      if pf_conv_x gl t1 t2 then (t1,e1,e2)
+      if Reductionops.is_conv env sigma t1 t2 then (t1,e1,e2)
       else raise PatternMatchingFailure
 
-let find_eq_data_decompose gl eqn =
-  let (lbeq,u,eq_args) = find_eq_data (project gl) eqn in
-  (lbeq,u,extract_eq_args gl eq_args)
+let find_eq_data_decompose env sigma eqn =
+  let (lbeq,u,eq_args) = find_eq_data sigma eqn in
+  (lbeq,u,extract_eq_args env sigma eq_args)
 
-let find_this_eq_data_decompose gl eqn =
+let find_this_eq_data_decompose env sigma eqn =
   let (lbeq,u,eq_args) =
     try (*first_match (match_eq eqn) inversible_equalities*)
-      find_eq_data (project gl) eqn
+      find_eq_data sigma eqn
     with PatternMatchingFailure ->
       user_err  (str "No primitive equality found.") in
   let eq_args =
-    try extract_eq_args gl eq_args
+    try extract_eq_args env sigma eq_args
     with PatternMatchingFailure ->
       user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in
   (lbeq,u,eq_args)
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 803305a1ca..0000f81d3f 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -122,11 +122,11 @@ val match_with_equation:
 
 (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u]
    Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *)
-val find_eq_data_decompose : Proofview.Goal.t -> constr ->
+val find_eq_data_decompose : Environ.env -> evar_map -> constr ->
       coq_eq_data * EInstance.t * (types * constr * constr)
 
 (** Idem but fails with an error message instead of PatternMatchingFailure *)
-val find_this_eq_data_decompose : Proofview.Goal.t -> constr ->
+val find_this_eq_data_decompose : Environ.env -> evar_map -> constr ->
       coq_eq_data * EInstance.t * (types * constr * constr)
 
 (** A variant that returns more informative structure on the equality found *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ca66f4bce2..3a4a2dc814 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2285,8 +2285,8 @@ let intro_decomp_eq_function = ref (fun _ -> failwith "Not implemented")
 
 let declare_intro_decomp_eq f = intro_decomp_eq_function := f
 
-let my_find_eq_data_decompose gl t =
-  try Some (find_eq_data_decompose gl t)
+let my_find_eq_data_decompose env sigma t =
+  try Some (find_eq_data_decompose env sigma t)
   with e when is_anomaly e
     (* Hack in case equality is not yet defined... one day, maybe,
        known equalities will be dynamically registered *)
@@ -2296,13 +2296,15 @@ let my_find_eq_data_decompose gl t =
 let intro_decomp_eq ?loc l thin tac id =
   Proofview.Goal.enter begin fun gl ->
   let c = mkVar id in
-  let t = Tacmach.New.pf_unsafe_type_of gl c in
-  let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
-  match my_find_eq_data_decompose gl t with
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let sigma, t = Typing.type_of env sigma c in
+  let _,t = reduce_to_quantified_ind env sigma t in
+  match my_find_eq_data_decompose env sigma t with
   | Some (eq,u,eq_args) ->
     !intro_decomp_eq_function
-    (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l)
-    (eq,t,eq_args) (c, t)
+      (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l)
+      (eq,t,eq_args) (c, t)
   | None ->
     Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
   end