diff options
Diffstat (limited to 'test-suite/output/PatternsInBinders.v')
| -rw-r--r-- | test-suite/output/PatternsInBinders.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index 0c1b08f5a3..d671053c07 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -53,7 +53,7 @@ Module Suboptimal. (** This test shows an example which exposes the [let] introduced by the pattern notation in binders. *) -#[universes(template)] Inductive Fin (n:nat) := Z : Fin n. +Inductive Fin (n:nat) := Z : Fin n. Definition F '(n,p) : Type := (Fin n * Fin p)%type. Definition both_z '(n,p) : F (n,p) := (Z _,Z _). Print both_z. |