diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-03 20:50:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-03 20:50:11 +0000 |
| commit | f9f35dc36f5249a2de18005ab59ae934e0fa7075 (patch) | |
| tree | 4d3dd839db319df1945c8fef474284e6f4e5f3e3 /toplevel | |
| parent | 25dde2366a4db47e5da13b2bbe4d03a31235706f (diff) | |
Added "etransitivity".
Added support for "injection" and "discriminate" on JMeq.
Seized the opportunity to update coqlib.ml and to rely more on it for
finding the equality lemmas.
Fixed typos in coqcompat.ml.
Propagated symmetry convert_concl fix to transitivity (see 11521).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqcompat.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqcompat.ml b/toplevel/coqcompat.ml index 8bf1e9bd0..59dca330c 100644 --- a/toplevel/coqcompat.ml +++ b/toplevel/coqcompat.ml @@ -24,10 +24,10 @@ let set_compat_options = function set_bool_option_value ["Intuition";"Iff";"Unfolding"] true | "8.1" -> - warning "Compatibility with versions 8.1 not supported." + warning "Compatibility with version 8.1 not supported." | "8.0" -> - warning "Compatibility with versions 8.0 not supported." + warning "Compatibility with version 8.0 not supported." | s -> error ("Unknown compatibility version \""^s^"\".") |