aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-02 00:24:53 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-02 00:28:43 +0200
commitdef03f31c1c639629e6bb07e266319bf6930f8fb (patch)
treea49452925b94da614f06df0941892ea1af69ec58 /theories
parent1ae74bfd16f00bea0de14299cace8b638f768a70 (diff)
parentaf2df1ada04da94a41a400c637788db461a532d9 (diff)
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'theories')
-rw-r--r--theories/Compat/Coq84.v4
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 21b78b533..8ae1a9195 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -76,3 +76,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.