diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-18 20:35:22 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-18 20:35:22 +0000 |
commit | 9d7499dcd4440aca458cb190ed108ae9b3adff17 (patch) | |
tree | 600b19fc9ca74cb6149676276b670e731e12ae66 /lib/flags.mli | |
parent | c79db26e91c61bfa085e667ae14733a463b73423 (diff) |
Generalizing flag use_evars_pattern_unification into a flag
use_pattern_unification common for evars and metas. As a compensation,
add a flag use_meta_bound_pattern_unification to restore the old
mechanism of pattern unification for metas applied to rels only (this
is used e.g. by auto). Not sure yet, what could be the most
appropriate set of flags. Added documentation of the flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14221 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/flags.mli')
-rw-r--r-- | lib/flags.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/flags.mli b/lib/flags.mli index f7e3c1759..4fd042e22 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -25,7 +25,7 @@ val load_proofs : load_proofs ref val raw_print : bool ref -type compat_version = V8_2 +type compat_version = V8_2 | V8_3 val compat_version : compat_version option ref val version_strictly_greater : compat_version -> bool val version_less_or_equal : compat_version -> bool |