diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 00:03:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 00:10:03 +0200 |
| commit | c5ecebf6fefbaa673dda506175a2aa4a69d79807 (patch) | |
| tree | e364fd928f247c249767ffb679b0265857327a6a /test-suite/bugs/closed/HoTT_coq_054.v | |
| parent | 4dc8746cac24ba72a1ec4dfa764a1ae88ce79277 (diff) | |
Revert specific syntax for primitive projections, avoiding ugly
contortions in internalization/externalization. It uses a fully typed
version of detyping, requiring the environment, to move from
primitive projection applications to regular applications of
the eta-expanded version. The kernel is unchanged, and only
constrMatching needs compatibility code now.
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_054.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_054.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v index b47bb3a20..c68796593 100644 --- a/test-suite/bugs/closed/HoTT_coq_054.v +++ b/test-suite/bugs/closed/HoTT_coq_054.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *) Inductive Empty : Prop := . Inductive paths {A : Type} (a : A) : A -> Type := @@ -47,10 +47,10 @@ Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B) | inl y' => ap g | inr y' => idmap end - | inr x' => match y as y return match y return Type with + | inr x' => match y as y return match y return Prop with inr y' => x' = y' | _ => Empty - end -> match f y return Type with + end -> match f y return Prop with | inr y' => h x' = y' | _ => Empty end with | inl y' => idmap |