Fix bug #2089: correctly dealing with parameters and real arguments in

Combined Scheme.


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

2 files changed, 23 insertions, 4 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2089.v b/test-suite/bugs/closed/shouldsucceed/2089.v
new file mode 100644
index 0000000000..aebccc9424
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2089.v
@@ -0,0 +1,17 @@
+Inductive even (x: nat): nat -> Prop :=
+  | even_base: even x O
+  | even_succ: forall n, odd x n -> even x (S n)
+
+with odd (x: nat): nat -> Prop :=
+  | odd_succ: forall n, even x n -> odd x (S n).
+
+Scheme even_ind2 := Minimality for even Sort Prop
+  with odd_ind2 := Minimality for odd Sort Prop.
+
+Combined Scheme even_odd_ind from even_ind2, odd_ind2.
+
+Check (even_odd_ind :forall (x : nat) (P P0 : nat -> Prop),
+  P 0 ->
+  (forall n : nat, odd x n -> P0 n -> P (S n)) ->
+  (forall n : nat, even x n -> P n -> P0 (S n)) ->
+  (forall n : nat, even x n -> P n) /\ (forall n : nat, odd x n -> P0 n)).
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d07c4973e0..cb772714d6 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1010,16 +1010,18 @@ let build_combined_scheme name schemes =
     let (ctx, arity) = decompose_prod ty in
     let (_, last) = List.hd ctx in
       match kind_of_term last with
-	| App (ind, args) -> ctx, destInd ind, Array.length args
+	| App (ind, args) -> 
+	    let ind = destInd ind in
+	    let (_,spec) = Inductive.lookup_mind_specif env ind in
+	      ctx, ind, spec.mind_nrealargs
 	| _ -> ctx, destInd last, 0
   in
   let defs =  
     List.map (fun x -> 
 		let refe = Ident x in
 		let qualid = qualid_of_reference refe in
-		let cst = try 
-                    Nametab.locate_constant (snd qualid) 
-                with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")
+		let cst = try Nametab.locate_constant (snd qualid) 
+                  with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")
                 in
 		let ty = Typeops.type_of_constant env cst in
 		  qualid, cst, ty)