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/hipattern.mli | |
| 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/hipattern.mli')
| -rw-r--r-- | tactics/hipattern.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 3637be41d..f74e7452e 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 |