diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/success/mutual_ind.v | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/success/mutual_ind.v')
| -rw-r--r-- | test-suite/success/mutual_ind.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index 463efed3..f63dfc38 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -9,7 +9,7 @@ Require Export List. - Record signature : Type := + Record signature : Type := {sort : Set; sort_beq : sort -> sort -> bool; sort_beq_refl : forall f : sort, true = sort_beq f f; @@ -20,14 +20,14 @@ Require Export List. fsym_beq_refl : forall f : fsym, true = fsym_beq f f; fsym_beq_eq : forall f1 f2 : fsym, true = fsym_beq f1 f2 -> f1 = f2}. - + Variable F : signature. Definition vsym := (sort F * nat)%type. Definition vsym_sort := fst (A:=sort F) (B:=nat). Definition vsym_nat := snd (A:=sort F) (B:=nat). - + Inductive term : sort F -> Set := | term_var : forall v : vsym, term (vsym_sort v) |