diff options
| author | herbelin | 2011-12-17 20:53:37 +0000 |
|---|---|---|
| committer | herbelin | 2011-12-17 20:53:37 +0000 |
| commit | 2ae65af3007c5ed79e932135f27704cae00dd449 (patch) | |
| tree | 3834282b03e917ce6483c106f109d065ca45c315 | |
| parent | f0226504cfb179a4491d43764bfdb22a1fe2d106 (diff) | |
Deactivated automatic inference of _case schemes, as it was in 8.3
(mainly to avoid defining names that may clash with user names later
on). Best approach will probably be to define inductive types in
relevant "name spaces".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14804 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/indschemes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index c92f63d09d..51eddbae9f 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -53,7 +53,7 @@ let _ = optread = (fun () -> !elim_flag) ; optwrite = (fun b -> elim_flag := b) } -let case_flag = ref true +let case_flag = ref false let _ = declare_bool_option { optsync = true; |