From 12268bef28dea57fdbe29dc87d26ef453ad5cfed Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 31 Aug 2016 11:32:28 +0200 Subject: 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. --- theories/Compat/Coq84.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'theories/Compat') 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. -- cgit v1.2.3