diff options
| author |  Jason Gross <jgross@mit.edu> | 2015-06-24 15:41:11 +0200 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2015-08-14 02:49:31 -0400 |
| commit | 6aa58955515dff338ea85d59073dfc0d0c7648ab (patch) | |
| tree | ed472dbf020c22a3080bc5e13a398914875bca11 /test-suite/bugs/closed/3649.v | |
| parent | 297b0cb44bbe8ec7304ca635c566815167266d4a (diff) | |
Move type_scope into user space, fix some output logs
Diffstat (limited to 'test-suite/bugs/closed/3649.v')
| -rw-r--r-- | test-suite/bugs/closed/3649.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v index 06188e7b1..fc60897d2 100644 --- a/test-suite/bugs/closed/3649.v +++ b/test-suite/bugs/closed/3649.v @@ -4,6 +4,8 @@ coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) 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 +56,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)). |