diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-07 07:53:42 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-07 07:53:42 +0200 |
| commit | 7e8612307f8393f12783bd9c591e6e26a3277b9d (patch) | |
| tree | 669e8e8e973871f693a8d1668273531f30957366 /tactics/tactics.ml | |
| parent | 876f202985d5bd463bd5b44c195b239bcfedad7c (diff) | |
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.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2de4e26f3..c2b7351bd 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 |