- Remove some dead code in subtac

- Fix an apparent bug in the printing of move, indeed by default
  move is _not_ dependent when parsed (see parsing/g_tactic.ml4).


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

3 files changed, 4 insertions, 49 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index c2309c833e..037911a196 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -53,10 +53,6 @@ let subst_evar_constr evs n t =
 	       | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
 	  in aux hyps args [] 
 	in
-  	  (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (List.length args) ++ str "arguments," ++
-			int (List.length hyps) ++ str " hypotheses" ++ spc () ++
-			pp_list (fun x -> my_print_constr (Global.env ()) x) args);
- 	   with _ -> ());
 	  if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then
 	    transparent := Idset.add idstr !transparent;
 	  mkApp (mkVar idstr, Array.of_list args)
@@ -124,9 +120,6 @@ let rec chop_product n t =
 let eterm_obligations env name isevars evm fs t ty = 
   (* 'Serialize' the evars, we assume that the types of the existentials
      refer to previous existentials in the list only *)
-  trace (str " In eterm: isevars: " ++ my_print_evardefs isevars);
-  trace (str "Term given to eterm" ++ spc () ++
-	    Termops.print_constr_env (Global.env ()) t);
   let nc = Environ.named_context env in
   let nc_len = Sign.named_context_length nc in
   let evl = List.rev (to_list evm) in
@@ -146,13 +139,7 @@ let eterm_obligations env name isevars evm fs t ty =
 	 let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in
 	 let evtyp, hyps, chop = 
 	   match chop_product fs evtyp with
-	       Some t -> 
-		 (try
-		    trace (str "Choped a product: " ++ spc () ++
-			     Termops.print_constr_env (Global.env ()) evtyp ++ str " to " ++ spc () ++
-			     Termops.print_constr_env (Global.env ()) t);
-		  with _ -> ());
-		 t, trunc_named_context fs hyps, fs
+	   Some t -> t, trunc_named_context fs hyps, fs
 	     | None -> evtyp, hyps, 0
 	 in
 	 let loc, k = evar_source id isevars in
@@ -169,26 +156,8 @@ let eterm_obligations env name isevars evm fs t ty =
   let evars = 
     List.map (fun (_, ((_, name), _, opaque, loc, typ, deps)) -> 
       name, typ, loc, not (opaque = None) && not (Idset.mem name transparent), deps) evts
-  in
-    (try
-       trace (str "Term constructed in eterm" ++ spc () ++
-		Termops.print_constr_env (Global.env ()) t');
-       ignore(iter
-		(fun (name, typ, _, _, deps) ->
-		   trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++
-			    Termops.print_constr_env (Global.env ()) typ))
-		evars);
-     with _ -> ());
-    Array.of_list (List.rev evars), t', ty
+  in Array.of_list (List.rev evars), t', ty
 
 let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
 
-(* let eterm evm t (tycon : types option) =  *)
-(*   let t, tycon, evs = eterm_term evm t tycon in *)
-(*     match tycon with *)
-(* 	Some typ -> Tactics.apply_term (mkCast (t, DEFAULTcast, typ)) [] *)
-(*       | None -> Tactics.apply_term t (mkMetas (List.length evs)) *)
-     
-(* open Tacmach *)
-
 let etermtac (evm, t) = assert(false) (*eterm evm t None *)
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 130d6858ba..563b228d89 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -260,19 +260,6 @@ let declare_obligation obl body =
     print_message (Subtac_utils.definition_message obl.obl_name);
     { obl with obl_body = Some (mkConst constant) }
       
-let try_tactics obls = 
-  Array.map
-    (fun obl ->
-       match obl.obl_body with
-	   None ->
-	     (try
-		let ev = evar_of_obligation obl in
-		let c = Subtac_utils.solve_by_tac ev Auto.default_full_auto in	       
-		  declare_obligation obl c		  
-	      with _ -> obl)
-	 | _ -> obl)
-    obls
-        
 let red = Reductionops.nf_betaiota
 
 let init_prog_info n b t deps fixkind notations obls impls kind hook =
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 933667ce32..0eaac6a635 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -805,10 +805,9 @@ and pr_atom1 = function
   | TacClearBody l ->
       hov 1 (str "clearbody" ++ spc () ++ prlist_with_sep spc pr_ident l)
   | TacMove (b,id1,id2) ->
-      (* Rem: only b = true is available for users *)
-      assert b;
       hov 1
-        (str "move" ++ brk (1,1) ++ pr_ident id1 ++ 
+        (str "move" ++ (if b then spc () ++ str"dependent" else mt ())
+	  ++ brk (1,1) ++ pr_ident id1 ++ 
 	 pr_move_location pr_ident id2)
   | TacRename l ->
       hov 1