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

4 files changed, 22 insertions, 24 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c28cfde122..2bc94c2003 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -111,9 +111,9 @@ GEXTEND Gram
       |  -> <:ast< (VERNACARGLIST) >> ] ]
   ;
   onescheme:
-    [ [ id = identarg; ":="; dep = dep; c = comarg; IDENT "Sort";
+    [ [ id = identarg; ":="; dep = dep; indid = identarg; IDENT "Sort";
         s = sortdef ->
-          <:ast< (VERNACARGLIST $id $dep $c (COMMAND $s)) >> ] ]
+          <:ast< (VERNACARGLIST $id $dep $indid (COMMAND $s)) >> ] ]
   ;
   specifscheme:
     [ [ rec_ = onescheme; "with"; recl = specifscheme -> rec_ :: recl
@@ -133,8 +133,8 @@ GEXTEND Gram
       |  -> <:ast< (BINDERLIST) >> ] ]
   ;
   sortdef:
-    [ [ "Set" -> <:ast< (PROP {Pos}) >>
-      | "Prop" -> <:ast< (PROP {Null}) >>
+    [ [ "Set"  -> <:ast< (SET) >>
+      | "Prop" -> <:ast< (PROP) >>
       | "Type" -> <:ast< (TYPE) >> ] ]
   ;
   thm_tok:
@@ -264,17 +264,9 @@ GEXTEND Gram
       | IDENT "Abstraction"; id = identarg; "["; l = ne_numarg_list; "]";
         ":="; c = comarg; "." ->
           <:ast< (ABSTRACTION $id $c ($LIST $l)) >>
-      | f = finite_tok; "Set"; id = identarg; indpar = indpar; ":=";
+      | f = finite_tok; s = sortdef; id = identarg; indpar = indpar; ":=";
         lidcom = lidcom; "." ->
-          <:ast< (ONEINDUCTIVE $f $id (COMMAND (PROP {Pos})) $indpar
-                   $lidcom) >>
-      | f = finite_tok; "Type"; id = identarg; indpar = indpar; ":=";
-        lidcom = lidcom; "." ->
-          <:ast< (ONEINDUCTIVE $f $id (COMMAND (TYPE)) $indpar $lidcom) >>
-      | f = finite_tok; "Prop"; id = identarg; indpar = indpar; ":=";
-        lidcom = lidcom; "." ->
-          <:ast< (ONEINDUCTIVE $f $id (COMMAND (PROP {Null})) $indpar
-                   $lidcom) >>
+          <:ast< (ONEINDUCTIVE $f $id (COMMAND $s) $indpar $lidcom) >>
       | f = finite_tok; indl = block; "." ->
           <:ast< (MUTUALINDUCTIVE $f (VERNACARGLIST ($LIST $indl))) >>
 
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