Déplacement de code dans command; MAJ DebugOn

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

1 files changed, 5 insertions, 9 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 33ecab345..8d21c4d76 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -335,8 +335,7 @@ let vernac_definition local id def hook =
         | Some r -> 
 	    let (evc,env)= Command.get_current_context () in
 	    Some (interp_redexp env evc r) in
-      let ref = declare_definition id local bl red_option c typ_opt in
-      hook local ref
+      declare_definition id local bl red_option c typ_opt hook
 
 let vernac_start_proof kind sopt (bl,t) lettop hook =
   if not(refining ()) then
@@ -362,11 +361,8 @@ let vernac_exact_proof c =
   by (Tactics.exact_proof c); 
   save_named true
 
-let vernac_assumption (islocal,_ as kind) l =
-  List.iter
-    (fun (is_coe,(id,c)) ->
-      let r = declare_assumption id kind [] c in
-      if is_coe then Class.try_add_new_coercion r islocal) l
+let vernac_assumption kind l =
+  List.iter (fun (is_coe,(id,c)) -> declare_assumption id is_coe kind [] c) l
 
 let vernac_inductive f indl = build_mutual indl f
 
@@ -707,7 +703,7 @@ let vernac_syntactic_definition id c = function
   | None -> syntax_definition id c
   | Some n ->
       let l = list_tabulate (fun _ -> (CHole (dummy_loc),None)) n in
-      let c = CApp (dummy_loc,c,l) in
+      let c = CApp (dummy_loc,(false,c),l) in
       syntax_definition id c
 
 let vernac_declare_implicits locqid = function
@@ -1054,7 +1050,7 @@ let vernac_check_guard () =
   msgnl message
 
 let vernac_debug b =
-  set_debug (if b then Tactic_debug.DebugOn else Tactic_debug.DebugOff)
+  set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
 
 
 (**************************)