- Correction bug calcul mind_consnrealargs, introduit à la révision

  7833, et que la révision 8644 n'avait pas corrigé dans le bon sens;
  renommage en mind_consnrealdecls pour éviter la confusion de sens
  avec mind_nrealargs
- Correction de la description du type one_inductive_body
- Ajout test avec let-in dans params et dans type constructeur 
  (fichier Case12.v)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8653 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 0 deletions

diff --git a/test-suite/success/Case12.v b/test-suite/success/Case12.v
index 20073aa73..f6a0d5780 100644
--- a/test-suite/success/Case12.v
+++ b/test-suite/success/Case12.v
@@ -57,3 +57,17 @@ Check
      | nil'' => 0
      | cons'' n l0 => S (length (mult2 n) l0)
      end).
+
+(* Check let-in in both parameters and in constructors *)
+
+Inductive list''' (A:Set) (B:=(A*A)%type) (a:A) : B -> Set :=
+  | nil''' : list''' A a (a,a)
+  | cons''' : 
+     forall a' : A, let m := (a',a) in list''' A a m -> list''' A a (a,a).
+
+Fixpoint length''' (A:Set) (B:=(A*A)%type) (a:A) (m:B) (l:list''' A a m) 
+  {struct l} : nat :=
+  match l with
+  | nil''' => 0
+  | cons''' _ m l0 => S (length''' A a m l0)
+  end.