Changement des named_context

Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs


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

6 files changed, 14 insertions, 28 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index eb767694bc..8512e00c56 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -178,7 +178,7 @@ let get_target t ind =
 let prods_of t = 
   let rec aux acc d = match kind_of_term d with
     | Prod (_,c1,c2) -> aux (c1::acc) c2
-    | Cast (c,_) -> aux acc c
+    | Cast (c,_,_) -> aux acc c
     | _ -> (d,acc)
   in 
   aux [] t
@@ -244,7 +244,7 @@ let build_id_coercion idf_opt source =
   in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
-      { const_entry_body = mkCast (val_f, typ_f);
+      { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f);
 	const_entry_type = Some typ_f;
         const_entry_opaque = false;
 	const_entry_boxed = Options.boxed_definitions()} in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 0a97baf8b5..0c916f7038 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -75,7 +75,7 @@ let rec destSubCast c = match kind_of_term c with
       let (b,u) = destSubCast c in mkLambda (x,t,b), mkProd (x,t,u)
   | LetIn (x,b,t,c) ->
       let (d,u) = destSubCast c in mkLetIn (x,b,t,d), mkLetIn (x,b,t,u)
-  | Cast (b,u) -> (b,u)
+  | Cast (b,_, u) -> (b,u)
   | _ -> assert false
 
 let rec adjust_conclusion a cs = function
@@ -112,7 +112,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
     | Some comtyp ->
 	(* We use a cast to avoid troubles with evars in comtyp *)
 	(* that can only be resolved knowing com *)
-	let b = abstract_rawconstr (mkCastC (com,comtyp)) bl in
+	let b = abstract_rawconstr (mkCastC (com,DEFAULTcast,comtyp)) bl in
 	let (body,typ) = destSubCast (interp_constr sigma env b) in
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
@@ -124,7 +124,7 @@ let red_constant_entry bl ce = function
   | Some red ->
       let body = ce.const_entry_body in
       { ce with const_entry_body = 
-	under_binders (Global.env()) (reduction_of_red_expr red)
+	under_binders (Global.env()) (fst (reduction_of_red_expr red))
 	  (length_of_raw_binders bl)
 	  body }
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 7633e168f9..97ba5c81cf 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -144,9 +144,9 @@ let re_exec is_ide =
 
 (*s options for the virtual machine *)
 
-let boxed_val = ref true
-let boxed_def = ref true
-let use_vm = ref true
+let boxed_val = ref false
+let boxed_def = ref false
+let use_vm = ref false
 
 let set_vm_opt () =
   Vm.set_transp_values (not !boxed_val);
@@ -173,7 +173,7 @@ let parse_args is_ide =
     | [] -> ()
 
     | "-impredicative-set" :: rem -> 
-        set_engagement Environ.ImpredicativeSet; parse rem
+        set_engagement Declarations.ImpredicativeSet; parse rem
 
     | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()
@@ -239,13 +239,7 @@ let parse_args is_ide =
 
     | "-debug" :: rem -> set_debug (); parse rem
 
-    | "-unboxed-values" :: rem -> 
-	boxed_val := false; parse rem
-    | "-boxed-definitions" :: rem ->
-	boxed_def := true; parse rem
-    | "-no-vm" :: rem -> use_vm := false; parse rem
-    | "-draw-vm-instr" :: rem -> Vm.set_drawinstr ();
-	Options.set_print_bytecodes true; parse rem
+    | "-vm" :: rem -> use_vm := true; parse rem
     | "-emacs" :: rem -> Options.print_emacs := true; parse rem
 	  
     | "-where" :: _ -> print_endline Coq_config.coqlib; exit 0
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 6b412ea681..88bd4650c0 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -37,7 +37,7 @@ let interp_decl sigma env = function
   | Vernacexpr.DefExpr((_,id),c,t) ->
       let c = match t with
 	| None -> c
-	| Some t -> mkCastC (c,t)
+	| Some t -> mkCastC (c,DEFAULTcast,t)
       in
       let j = judgment_of_rawconstr Evd.empty env c in
       (id,Some j.uj_val, j.uj_type)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 124ad03c61..a93e6fd5e6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -764,14 +764,6 @@ let _ =
 
 let _ =
   declare_bool_option 
-    { optsync  = false;
-      optname  = "print the bytecode of global definitions";
-      optkey   = (SecondaryTable ("Print","Bytecode"));
-      optread  = Options.print_bytecodes;
-      optwrite = (fun b -> Options.set_print_bytecodes b) } 
-
-let _ =
-  declare_bool_option 
     { optsync  = true;
       optname  = "use of virtual machine inside the kernel";
       optkey   = (SecondaryTable ("Virtual","Machine"));
@@ -780,7 +772,7 @@ let _ =
 
 let _ =
   declare_bool_option 
-    { optsync  = false;
+    { optsync  = true;
       optname  = "use of boxed definitions";
       optkey   = (SecondaryTable ("Boxed","Definitions"));
       optread  = Options.boxed_definitions;
@@ -888,7 +880,7 @@ let vernac_check_may_eval redexp glopt rc =
 	if !pcoq <> None then (out_some !pcoq).print_check j
 	else msg (print_judgment env j)
     | Some r ->
-	let redfun = reduction_of_red_expr (interp_redexp env evmap r) in
+	let redfun = fst (reduction_of_red_expr (interp_redexp env evmap r)) in
 	if !pcoq <> None
 	then (out_some !pcoq).print_eval (redfun env evmap) env rc j
 	else msg (print_eval redfun env j)
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 292eb0c3f3..91a4f3cb75 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -135,7 +135,7 @@ let rec uri_of_constr c =
   | RLetIn (_,na,b,c) ->
       url_string "let "; url_of_name na; url_string "\\def ";
       uri_of_constr b; url_string " in "; uri_of_constr c
-  | RCast (_,c,t) ->
+  | RCast (_,c,_,t) ->
       uri_of_constr c; url_string ":"; uri_of_constr t
   | RRec _ | RIf _ | RLetTuple _ | ROrderedCase _ | RCases _ ->
       error "Whelp does not support pattern-matching and (co-)fixpoint"