Imported Upstream version 8.6upstream/8.6

1 files changed, 4 insertions, 1 deletions

diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index 06188e7b..fc4c171e 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -2,8 +2,11 @@
 (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
+Declare ML Module "coretactics".
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y" (at level 70, no associativity).
+Delimit Scope type_scope with type.
+Bind Scope type_scope with Sortclass.
 Open Scope type_scope.
 Axiom admit : forall {T}, T.
 Notation "A -> B" := (forall (_ : A), B) : type_scope.
@@ -54,4 +57,4 @@ Goal forall (C D : PreCategory) (G G' : Functor C D)
   (** This [change] succeeded, but did not progress, in 07e4438bd758c2ced8caf09a6961ccd77d84e42b, because [T0 x o T1 x] was not found in the goal *)
   let T0 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T0) end in
   let T1 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T1) end in
-  progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)).
\ No newline at end of file
+  progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)).