diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-13 22:21:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-13 22:21:23 +0000 |
| commit | d5b1c83d0f0a60f9658c45ae902035f2fdef0c41 (patch) | |
| tree | 69a66d45f4e23eb9a979d571cdcf4cb099f8aa64 /pretyping/unification.mli | |
| parent | 463b54961c77aa7b5f21d2937628d9cc9cd5a06a (diff) | |
Added a flag to restrict conversion in tactic unification on the
strict subterms of the initial unification problem (inspired from
ssreflect rewriting strategy). Not activated however (a few
applications of setoid rewrite use this possibility on closed terms in
the stdlib, e.g. "flip le p (min n m)" identified with "le (min n m) p").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14198 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index aa0267698..44b1c3889 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -18,6 +18,7 @@ type unify_flags = { resolve_evars : bool; use_evars_pattern_unification : bool; frozen_evars : ExistentialSet.t; + restrict_conv_on_strict_subterms : bool; modulo_betaiota : bool; modulo_eta : bool; allow_K_in_toplevel_higher_order_unification : bool |