diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-26 14:23:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-26 14:50:12 +0200 |
| commit | 55e46598fac67157a5b2c820be621d254581b888 (patch) | |
| tree | 61db2f9a76b3bb55c5fc0131be9600227efc31c2 /pretyping/inductiveops.ml | |
| parent | 68d60b7c33b11ad452eca3d2a7ec320963064a9d (diff) | |
Deactivate the "Standard Propositions Naming" flag, source of a lot of
incompatibilities, at least until the check of compilation of contribs
succeeds more often.
Incidentally adapted some proofs in Reals which were not agnostic
relatively to whether the option is on or off.
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index c64cd35e5..6fa93484f 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -370,10 +370,10 @@ let find_coinductive env sigma c = (* find appropriate names for pattern variables. Useful in the Case and Inversion (case_then_using et case_nodep_then_using) tactics. *) -let h_based_elimination_names = ref true +let h_based_elimination_names = ref false let use_h_based_elimination_names () = - !h_based_elimination_names && Flags.version_strictly_greater Flags.V8_4 + !h_based_elimination_names (* && Flags.version_strictly_greater Flags.V8_4 *) open Goptions |