In Hipattern: some functions not working modulo evar instantiation.

In theory [Proofview.Goal.env] should be, itself, marked as requiring a normalised goals (as it includes [hyps] which does). However, it is impractical as it is very common to pass a goal environment to a function reasoning modulo evars. So I guess we are bound to mark the appropriate functions by hand.

4 files changed, 9 insertions, 9 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7343aa532a..91d774e6ee 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -924,7 +924,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   end
 
 let onEquality with_evars tac (c,lbindc) =
-  Proofview.Goal.raw_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let type_of = pf_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
   let t = type_of c in
@@ -1214,7 +1214,7 @@ let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 let eqdep_dec = qualid_of_string "Coq.Logic.Eqdep_dec"
 
 let inject_if_homogenous_dependent_pair ty =
-  Proofview.Goal.raw_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   try
     let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
     (* fetch the informations of the  pair *)
@@ -1484,9 +1484,9 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 exception NothingToRewrite
 
 let cutSubstInConcl_RL eqn =
-  Proofview.Goal.raw_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let (lbeq,u,(t,e1,e2 as eq)) = find_eq_data_decompose gl eqn in
-  let concl = pf_nf_concl gl in
+  let concl = pf_concl gl in
   let sigma,body,expected_goal = pf_apply subst_tuple_term gl e2 e1 concl in
   if not (dependent (mkRel 1) body) then raise NothingToRewrite;
     Proofview.V82.tclEVARS sigma <*>
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 3637be41d8..f74e7452e0 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -120,11 +120,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 : 'a Proofview.Goal.t -> constr ->
+val find_eq_data_decompose : [ `NF ] Proofview.Goal.t -> constr ->
       coq_eq_data * Univ.universe_instance * (types * constr * constr)
 
 (** Idem but fails with an error message instead of PatternMatchingFailure *)
-val find_this_eq_data_decompose : 'a Proofview.Goal.t -> constr ->
+val find_this_eq_data_decompose : [ `NF ] Proofview.Goal.t -> constr ->
       coq_eq_data * Univ.universe_instance * (types * constr * constr)
 
 (** A variant that returns more informative structure on the equality found *)
@@ -147,7 +147,7 @@ val match_eqdec : constr -> bool * constr * constr * constr * constr
 (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
 open Proof_type
 open Tacmach
-val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr)
+val dest_nf_eq : [ `NF ] Proofview.Goal.t -> constr -> (constr * constr * constr)
 
 (** Match a negation *)
 val is_matching_not : constr -> bool
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 36affb5412..5b3f7374cc 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -298,7 +298,7 @@ let projectAndApply thin id eqname names depids =
       (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
   in
   let substHypIfVariable tac id =
-    Proofview.Goal.raw_enter begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     (** We only look at the type of hypothesis "id" *)
     let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in
     let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2de4e26f3f..c2b7351bd2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1568,7 +1568,7 @@ let my_find_eq_data_decompose gl t =
       -> raise ConstrMatching.PatternMatchingFailure
 
 let intro_decomp_eq loc l thin tac id =
-  Proofview.Goal.raw_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let c = mkVar id in
   let t = Tacmach.New.pf_type_of gl c in
   let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in