diff options
Diffstat (limited to 'test-suite/success/CasesDep.v')
| -rw-r--r-- | test-suite/success/CasesDep.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index b625eb151a..49bd77fcd6 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -71,13 +71,9 @@ Inductive Setoid : Type := Definition elem (A : Setoid) := let (S, R, e) := A in S. -(* <Warning> : Grammar is replaced by Notation *) - Definition equal (A : Setoid) := let (S, R, e) as s return (Relation (elem s)) := A in R. -(* <Warning> : Grammar is replaced by Notation *) - Axiom prf_equiv : forall A : Setoid, Equivalence (elem A) (equal A). Axiom prf_refl : forall A : Setoid, Reflexive (elem A) (equal A). |