diff options
Diffstat (limited to 'toplevel/coqcompat.ml')
| -rw-r--r-- | toplevel/coqcompat.ml | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/toplevel/coqcompat.ml b/toplevel/coqcompat.ml new file mode 100644 index 000000000..8bf1e9bd0 --- /dev/null +++ b/toplevel/coqcompat.ml @@ -0,0 +1,33 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(* File initially created by Hugo Herbelin, Aug 2009 *) + +(* This file centralizes the support for compatibility with previous + versions of Coq *) + +open Pp +open Util +open Goptions + +let set_compat_options = function + | "8.2" -> + set_bool_option_value ["Tactic";"Evars";"Pattern";"Unification"] false; + set_bool_option_value ["Discriminate";"Introduction"] false; + set_bool_option_value ["Intuition";"Iff";"Unfolding"] true + + | "8.1" -> + warning "Compatibility with versions 8.1 not supported." + + | "8.0" -> + warning "Compatibility with versions 8.0 not supported." + + | s -> + error ("Unknown compatibility version \""^s^"\".") |