diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-06 19:31:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-07 11:10:09 +0100 |
| commit | 37cf90492cb6ed468e696fa052192f1a9fc4b003 (patch) | |
| tree | 9c8966e5b0808db27ac400db3766892e75fc45c5 /tactics/hipattern.mli | |
| parent | 8972a5ed75b7778ad992ef018b163c6ac6e27297 (diff) | |
Getting rid of pf_matches in Hipattern.
Funnily enough, the old code is completely bogus. It succeeds in early files
of the prelude just because the heterogeneous equality has not been required.
This raises an exception which is not the same one as if we tried to rewrite
with the identity type first.
The only user, the inversion tactic, was actually only relying on Logic.eq
and was furthermore not even using the convertibility algorithm. We just
perform a syntactic match now.
Diffstat (limited to 'tactics/hipattern.mli')
| -rw-r--r-- | tactics/hipattern.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 8ff6fe95c..237ed42d5 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -144,9 +144,6 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool [t,u,T] and a boolean telling if equality is on the left side *) val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr -(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) -val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr) - (** Match a negation *) val is_matching_not : Environ.env -> evar_map -> constr -> bool val is_matching_imp_False : Environ.env -> evar_map -> constr -> bool |