- Reforme de la gestion des args recursifs (via arbres reguliers)

- coqtop -byte -opt bouclait!


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

4 files changed, 12 insertions, 9 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4a517144ec..e34d6b9199 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -204,8 +204,7 @@ let interp_mutual lparams lnamearconstrs finite =
 	   List.map 
 	     (interp_type_with_implicits sigma ind_env_params ind_impls) bodies
 	 in
-	 { mind_entry_nparams = nparams;
-	   mind_entry_params = params';
+	 { mind_entry_params = params';
 	   mind_entry_typename = name;
 	   mind_entry_arity = ar;
 	   mind_entry_consnames = constrnames;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 4013fcd0e9..b273034df9 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -81,12 +81,17 @@ let add_compile verbose s =
 let compile_files () =
   List.iter (fun (v,f) -> Vernac.compile v f) (List.rev !compile_list)
 
+let re_exec_version = ref ""
+let set_byte () = re_exec_version := "byte"
+let set_opt () = re_exec_version := "opt"
+
 (* Re-exec Coq in bytecode or native code if necessary. [s] is either
    ["byte"] or ["opt"]. Notice that this is possible since the nature of
    the toplevel has already been set in [Mltop] by the main file created
    by coqmktop (see scripts/coqmktop.ml). *)
 
-let re_exec s =
+let re_exec () =
+  let s = !re_exec_version in
   let is_native = (Mltop.get()) = Mltop.Native in
   if (is_native && s = "byte") || ((not is_native) && s = "opt") then begin
     let prog = Sys.argv.(0) in
@@ -125,8 +130,8 @@ let parse_args () =
 
     | "-q" :: rem -> no_load_rc (); parse rem
 
-    | "-opt" :: rem -> re_exec "opt"; parse rem
-    | "-byte" :: rem -> re_exec "byte"; parse rem
+    | "-opt" :: rem -> set_opt(); parse rem
+    | "-byte" :: rem -> set_byte(); parse rem
     | "-full" :: rem -> warning "option -full deprecated\n"; parse rem
 
     | "-batch" :: rem -> set_batch_mode (); parse rem
@@ -217,6 +222,7 @@ let start () =
     Lib.init();
     try
       parse_args ();
+      re_exec ();
       if_verbose print_header ();
       init_load_path ();
       inputstate ();
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 6a3e135ff8..9ee3a56211 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -96,8 +96,7 @@ let abstract_inductive ids_to_abs hyps inds =
 		| (Name id,Some p,_) -> id, LocalDef p
 		| (Anonymous,_,_) -> anomaly"Unnamed inductive local variable")
 	     params in
-	 { mind_entry_nparams = nparams';
-	   mind_entry_params = params';
+	 { mind_entry_params = params';
 	   mind_entry_typename = a;
 	   mind_entry_arity = short_arity;
 	   mind_entry_consnames = c;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 71443abb56..5beedfff83 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -185,8 +185,7 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
   let named_type_constructor = it_mkNamedProd_or_LetIn ind fields in
   let type_constructor = subst_vars subst named_type_constructor in
   let mie_ind =
-    { mind_entry_nparams = nparams;
-      mind_entry_params = degenerate_decl params;
+    { mind_entry_params = degenerate_decl params;
       mind_entry_typename = idstruc;
       mind_entry_arity = mkSort s;
       mind_entry_consnames = [idbuild];