Merge pull request #20 from mattam82/coq-8.5

Record the arity of each branch in Case constructs

src/reify.ml4

@@ -243,10 +243,13 @@ struct
 	let (a',acc) = quote_term acc env a in
 	let (b',acc) = quote_term acc env b in
 	let (branches,acc) =
-	  List.fold_left (fun (xs,acc) x ->
-	    let (x,acc) = quote_term acc env x in (x :: xs, acc))
-	    ([],acc) (Array.to_list e) in
-	(Term.mkApp (tCase, [| npar ; a' ; b' ; to_coq_list tTerm (List.rev branches) |]), acc)
+          CArray.fold_left2 (fun (xs,acc) x nargs ->
+            let (x,acc) = quote_term acc env x in
+            let t = pair tnat tTerm (int_to_nat nargs) x in
+              (t :: xs, acc))
+          ([],acc) e ci.ci_cstr_nargs in
+        let tl = prod tnat tTerm in
+        (Term.mkApp (tCase, [| npar ; a' ; b' ; to_coq_list tl (List.rev branches) |]), acc)
       | Term.Fix fp ->
 	let (t,n,acc) = quote_fixpoint acc env fp in
 	(Term.mkApp (tFix, [| t ; int_to_nat n |]), acc)

theories/Ast.v

@@ -48,7 +48,7 @@ Inductive term : Set :=
 | tConst     : string -> term
 | tInd       : inductive -> term
 | tConstruct : inductive -> nat -> term
-| tCase      : nat (* # of parameters *) -> term (** type info **) -> term -> list term -> term
+| tCase      : nat (* # of parameters *) -> term (** type info **) -> term -> list (nat * term) -> term
 | tFix       : mfixpoint term -> nat -> term
 (*
 | CoFix     of ('constr, 'types) pcofixpoint