diff options
| author | herbelin | 2011-09-26 11:46:59 +0000 |
|---|---|---|
| committer | herbelin | 2011-09-26 11:46:59 +0000 |
| commit | 446155d07c89e148ec61bb0c414f4cd8a73311e0 (patch) | |
| tree | 6e7bfa33c9cf4422ab97444aab287a18def92e2e /tactics | |
| parent | 91c9a1294d236f55ff6fecdf1d763e7185590ea1 (diff) | |
Adding subst_term up to conv
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14497 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ac91af5d2e..1cc5c585dd 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1660,6 +1660,25 @@ let letin_tac with_eq name c occs gl = (* Implementation without generalisation: abbrev will be lost in hyps in *) (* in the extracted proof *) +let default_matching_flags = { + modulo_conv_on_closed_terms = Some empty_transparent_state; + use_metas_eagerly_in_conv_on_closed_terms = false; + modulo_delta = empty_transparent_state; + modulo_delta_types = full_transparent_state; + resolve_evars = false; + use_pattern_unification = false; + use_meta_bound_pattern_unification = false; + frozen_evars = ExistentialSet.empty; + restrict_conv_on_strict_subterms = false; + modulo_betaiota = false; + modulo_eta = false; + allow_K_in_toplevel_higher_order_unification = false +} + +let matching_fun sigma c1 c2 = + w_unify false env CONV flags:default_matching_flags + + let letin_abstract id c (occs,check_occs) gl = let env = pf_env gl in let compute_dependency _ (hyp,_,_ as d) depdecls = |