diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-31 11:32:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-31 11:45:41 +0200 |
| commit | 12268bef28dea57fdbe29dc87d26ef453ad5cfed (patch) | |
| tree | 9c4088cd2c3d966bd5769522e21eb173de885468 /theories/Compat | |
| parent | 3da141c5dfed50e1b9a4ad5421b4abacdcc23dae (diff) | |
Fix bug #5043: [Admitted] lemmas pick up section variables.
We add a flag Keep Admitted Variables that allows to recover the legacy
v8.4 behaviour of admitted lemmas. The statement of such lemmas did not
depend on the current context variables.
Diffstat (limited to 'theories/Compat')
| -rw-r--r-- | theories/Compat/Coq84.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index c157c5e85..4f6118902 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -72,3 +72,7 @@ Require Coq.Lists.List. Require Coq.Vectors.VectorDef. Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. Notation " [ x ; .. ; y ] " := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope. + +(** In 8.4, the statement of admitted lemmas did not depend on the section + variables. *) +Unset Keep Admitted Variables. |