diff options
| -rw-r--r-- | test-suite/success/Case5.v (renamed from test-suite/ideal-features/Case5.v) | 1 | ||||
| -rw-r--r-- | test-suite/success/Cases.v (renamed from test-suite/ideal-features/Cases.v) | 0 | ||||
| -rw-r--r-- | test-suite/success/CasesDep.v (renamed from test-suite/ideal-features/CasesDep.v) | 7 |
3 files changed, 3 insertions, 5 deletions
diff --git a/test-suite/ideal-features/Case5.v b/test-suite/success/Case5.v index d703286f9..fe49cdf95 100644 --- a/test-suite/ideal-features/Case5.v +++ b/test-suite/success/Case5.v @@ -1,5 +1,4 @@ -Reset ff. Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m). Parameter discr_r : (n:nat) ~(O=(S n)). Parameter discr_l : (n:nat) ~((S n)=O). diff --git a/test-suite/ideal-features/Cases.v b/test-suite/success/Cases.v index 313f8f74a..313f8f74a 100644 --- a/test-suite/ideal-features/Cases.v +++ b/test-suite/success/Cases.v diff --git a/test-suite/ideal-features/CasesDep.v b/test-suite/success/CasesDep.v index 3a0c36b6d..0108c1e94 100644 --- a/test-suite/ideal-features/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -221,15 +221,15 @@ end. -Fixpoint equalT [t1:TERM]:TERM->Prop := +Definition equalT [t1:TERM]:TERM->Prop := [t2:TERM] Cases t1 t2 of (var v1) (var v2) => True | (oper op1 l1) (oper op2 l2) => False | _ _ => False - end + end. -with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := +Definition EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := [n2:posint][l2:(LTERM n2)] Cases l1 l2 of nil nil => True @@ -239,7 +239,6 @@ end. Reset equalT. -Reset EqListT. (* ------------------------------------------------------------------*) (* Initial exemple (without patterns) *) (*-------------------------------------------------------------------*) |