diff options
Diffstat (limited to 'test-suite/success/implicit.v')
| -rw-r--r-- | test-suite/success/implicit.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index 9034d6a6f..aabb057a4 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -12,7 +12,7 @@ Infix "#" := op (at level 70). Check (forall x : A, x # x). (* Example submitted by Christine *) -Record stack : Type := +Record stack : Type := {type : Set; elt : type; empty : type -> bool; proof : empty elt = true}. Check @@ -42,7 +42,7 @@ Inductive P n : nat -> Prop := c : P n n. Require Import List. Fixpoint plus n m {struct n} := - match n with + match n with | 0 => m | S p => S (plus p m) end. |