diff options
Diffstat (limited to 'test-suite/bugs/closed/3649.v')
| -rw-r--r-- | test-suite/bugs/closed/3649.v | 5 |
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)). |