Les inductifs dans Scheme doivent être des ident d'inductifs

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

3 files changed, 16 insertions, 10 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index f0e40d7bf8..c1860012bb 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -337,15 +337,24 @@ let build_corecursive lnameardef =
   in
   ()
 
+exception NotInductive
+let inductive_of_ident id =
+  try match kind_of_term (global_reference CCI id) with
+    | IsMutInd ind -> ind
+    | _ -> raise NotInductive
+  with Not_found | NotInductive ->
+       errorlabstrm "inductive_of_ident"
+	 [< 'sTR (string_of_id id); 'sPC;
+	    'sTR "is not an inductive type" >]
+
 let build_scheme lnamedepindsort = 
   let lrecnames = List.map (fun (f,_,_,_) -> f) lnamedepindsort
   and sigma = Evd.empty
   and env0 = Global.env() in
   let lrecspec =
-    List.map (fun (_,dep,ind,sort) -> 
-                let indc = constr_of_com sigma env0 ind
-                and s = destSort (constr_of_com sigma env0 sort) in
-                (indc,dep,s)) lnamedepindsort
+    List.map (fun (_,dep,indid,sort) -> 
+                let s = destSort (constr_of_com sigma env0 sort) in
+                (inductive_of_ident indid,dep,s)) lnamedepindsort
   in
   let n = NeverDischarge in 
   let listdecl = Indrec.build_indrec env0 sigma lrecspec in 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 8b99e1657a..eaeb289c09 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -35,7 +35,5 @@ val build_recursive :
 
 val build_corecursive :  (identifier * Coqast.t * Coqast.t) list -> unit
 
-val mkProdCit : (identifier * Coqast.t) list -> Coqast.t -> Coqast.t 
-
-val build_scheme : (identifier * bool * Coqast.t * Coqast.t) list -> unit
+val build_scheme : (identifier * bool * identifier * Coqast.t) list -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a0a4848f4c..280274788b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -119,7 +119,6 @@ let locate_id id =
     mSG [< 'sTR (string_of_path (Nametab.sp_of_id CCI id)); 'fNL >]
   with Not_found -> 
     error ((string_of_id id) ^ " not a defined object")
-
 let print_loadpath () =
   let l = search_paths () in
   mSGNL [< 'sTR"Load Path:"; 'fNL; 'sTR"  ";
@@ -1037,14 +1036,14 @@ let _ =
 		  | (VARG_VARGLIST 
 		       [VARG_IDENTIFIER fid;
 			VARG_STRING depstr;
-			VARG_COMMAND ind; 
+			VARG_IDENTIFIER indid;
 			VARG_COMMAND sort]) ->
 		      let dep = match depstr with 
 			| "DEP" -> true
                         | "NODEP" -> false
                         | _ -> anomaly "Unexpected string"
 		      in 
-		      (fid,dep,ind,sort)
+		      (fid,dep,indid,sort)
 		  | _ -> bad_vernac_args "INDUCTIONSCHEME") lmi
 	   in 
 	   fun () -> build_scheme lnamedepindsort