aboutsummaryrefslogtreecommitdiff
path: root/lib/flags.ml
diff options
context:
space:
mode:
authorherbelin2011-06-18 20:35:22 +0000
committerherbelin2011-06-18 20:35:22 +0000
commit9d7499dcd4440aca458cb190ed108ae9b3adff17 (patch)
tree600b19fc9ca74cb6149676276b670e731e12ae66 /lib/flags.ml
parentc79db26e91c61bfa085e667ae14733a463b73423 (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.ml')
-rw-r--r--lib/flags.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index e8763bc79f..b9965af5dd 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -36,7 +36,7 @@ let raw_print = ref false
(* Compatibility mode *)
-type compat_version = V8_2
+type compat_version = V8_2 | V8_3
let compat_version = ref None
let version_strictly_greater v =
match !compat_version with None -> true | Some v' -> v'>v