Various subtac fixes. Add inequalities in pattern matching branches when needed, handle undo for the default tactic...

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

10 files changed, 164 insertions, 94 deletions

diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 4a2208cec..569c52e89 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -46,7 +46,8 @@ end.
 
 Ltac destruct_exists := repeat (destruct_one_pair) .
 
-Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; auto with arith.  
+Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; 
+  try (solve [ red ; intros ; discriminate ]) ; auto with arith.  
 
 (* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *)
 Ltac destruct_call f :=
@@ -65,6 +66,18 @@ Ltac destruct_call f :=
       end
     end.
 
+Ltac myinjection :=
+      let tac H := inversion H ; subst ; clear H in
+        match goal with
+          | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H
+          | [ H : ?f ?a ?b = ?f' ?a' ?b'  |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c = ?f' ?a' ?b' ?c' |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d' |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e' |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c ?d ?e ?f= ?f' ?a' ?b' ?c' ?d' ?e' ?f'  |- _ ] => tac H
+          | _ => idtac
+        end.
+
 Extraction Inline proj1_sig.
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 933ea94b3..d589c5c1f 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -112,7 +112,7 @@ VERNAC COMMAND EXTEND Subtac_Solve_Obligations
     END
 
 VERNAC COMMAND EXTEND Subtac_Set_Solver
-| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.interp t) ]
+| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.glob_tactic t) ]
 END
 
 VERNAC COMMAND EXTEND Subtac_Show_Obligations
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index a7ad70c8a..efc18703a 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -142,23 +142,11 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
       
 let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
 
-let subtac_utils_path =
-  make_dirpath (List.map id_of_string ["Utils";contrib_name;"Coq"])
-let utils_tac s =
-  lazy(make_kn (MPfile subtac_utils_path) (make_dirpath []) (mk_label s))
-
-let utils_call tac args =
-  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (utils_tac tac)),args))
-
 let start_proof_and_print env isevars idopt k t hook =
   start_proof_com env isevars idopt k t hook;
   print_subgoals ()
   (*if !pcoq <> None then (out_some !pcoq).start_proof ()*)
 
-let _ = Subtac_obligations.set_default_tactic 
-    (Tacinterp.eval_tactic (utils_call "subtac_simpl" []))
-
-
 let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 6da7567c8..b289afaa1 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1651,7 +1651,7 @@ let constr_of_pat env isevars ty pat idents =
   let pat', sign, y, z, idents = typ env ty pat idents in 
   let c = it_mkProd_or_LetIn y sign in
     trace (str "Constr_of_pat gives: " ++ my_print_constr env c);
-    pat', (sign, y, ty), idents
+    pat', (sign, y, ty, pat'), idents
 
 let mk_refl typ a = mkApp (Lazy.force eq_refl, [| typ; a |])
 
@@ -1661,33 +1661,62 @@ let vars_of_ctx =
 		  Anonymous -> raise (Invalid_argument "vars_of_ctx")
 		| Name n -> RVar (dummy_loc, n))
 
-let build_ineqs prevpatterns = ()
- (* List.fold_left 
-    (fun (sign, c) eqnpats -> 
-       let acc = List.fold_left
-	 (fun acc (ppat_sign, ppat_c, ppat_ty) ->
-	    match acc with
-		None -> None
-	      | Some (sign, len, n, c) ->
-(* 		  if is_included pat prevpat then *)
-		    let lens = List.length ppat_sign in
-		    let len' = lens + len in
-		    let acc = 
-		      (lift_rel_context len ppat_sign @ sign, 
-		       len',
-		       mkApp (Lazy.force eq_ind,
-			      [| ppat_ty ; ppat_c ; 
-				 mkRel (len' + n) |]) :: c)
-		    in Some acc
-(* 		  else None *))
-	 (sign, c) eqnpats
-       in match acc with 
-	   None -> (sign, c)
-	 | Some (sign, len, c) ->
-	     it_mkProd_or_LetIn c sign
-    )
-    ([], []) prevpatterns
-*)
+let unsafe_fold_right f = function
+    hd :: tl -> List.fold_right f tl hd
+  | [] -> raise (Invalid_argument "unsafe_fold_right")
+
+let mk_conj l =
+  let conj_typ = Lazy.force Subtac_utils.and_typ in
+    unsafe_fold_right
+      (fun c conj ->
+	 mkApp (conj_typ, [| c ; conj |]))
+      l
+
+let mk_not c =
+  let notc = Lazy.force Subtac_utils.not_ref in
+    mkApp (notc, [| c |])
+
+let rec is_included x y = 
+  match x, y with
+    | PatVar _, _ -> true
+    | _, PatVar _ -> true
+    | PatCstr (l, (_, i), args, alias), PatCstr (l', (_, i'), args', alias')  ->
+	if i = i' then List.for_all2 is_included args args'
+	else false
+
+let build_ineqs prevpatterns pats liftsign patargs =
+  let tomatchs = List.length pats in
+  let diffs = 
+    List.fold_left 
+      (fun c eqnpats -> 
+	 let acc = List.fold_left2
+	   (fun acc (ppat_sign, ppat_c, ppat_ty, ppat) curpat ->
+	      match acc with
+		  None -> None
+		| Some (sign, len, n, c) ->
+		    if is_included curpat ppat then
+		      let lens = List.length ppat_sign in
+		      let len' = lens + len in
+		      let acc = 
+			(lift_rel_context len ppat_sign @ sign, 
+			 len',
+			 succ n,
+			 mkApp (Lazy.force eq_ind,
+				[| lift (lens + liftsign) ppat_ty ; liftn liftsign (succ lens) ppat_c ; 
+				   mkRel (len' + patargs.(pred n)) |]) :: 
+			   List.map (lift lens) c)
+		      in Some acc
+		    else None)
+	   (Some ([], 0, 1, [])) eqnpats pats
+	 in match acc with 
+	     None -> c
+	   | Some (sign, len, _, c') ->
+	       let conj = it_mkProd_or_LetIn (mk_not (mk_conj c')) (lift_rel_context liftsign sign) in
+		 conj :: c)
+      [] prevpatterns
+  in match diffs with [] -> None
+    | _ -> Some (mk_conj diffs)
+       
 let constrs_of_pats typing_fun tycon env isevars eqns tomatchs =
   let i = ref 0 in
   let (x, y, z) = 
@@ -1700,11 +1729,11 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs =
 	     eqn.patterns tomatchs ([], [], [])
 	 in
 	 let rhs_rels, signlen = 
-	   List.fold_left (fun (renv, n) (sign,_,_) -> 
+	   List.fold_left (fun (renv, n) (sign,_,_,_) -> 
 			   ((lift_rel_context n sign) @ renv, List.length sign + n)) 
 	     ([], 0) pats in
 	 let eqs, _, _ = List.fold_left2 
-	   (fun (eqs, n, slen) (sign, c, _) (tm, ty) -> 
+	   (fun (eqs, n, slen) (sign, c, _, _) (tm, ty) -> 
 	      let len = n + signlen in (* Number of already defined equations + signature *)
 	      let csignlen = List.length sign in
 	      let slen' = slen - csignlen in (* Lift to get pattern variables signature *)	      
@@ -1721,18 +1750,27 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs =
 	   ([], 0, signlen) pats tomatchs
 	 in
 	 let eqs_rels = List.map (fun eq -> Name (id_of_string "H"), None, eq) eqs in
-	 (*let ineqs = build_ineqs prevpatterns newpatterns in*)
-	 let rhs_rels' = eqs_rels @ rhs_rels in
+	 let pattern_rels = fst (List.fold_right (fun (sign, pat_c, pat_ty, pat)  (l, acc) -> 
+						    acc :: l, List.length sign + acc) pats ([], 1))
+	 in
+	 let ineqs = build_ineqs prevpatterns newpatterns signlen (Array.of_list pattern_rels) in
+	 let rhs_rels', lift_ineqs = 
+	   match ineqs with
+	       None -> eqs_rels @ rhs_rels, 0
+	     | Some ineqs -> 
+		 let _ = trace (str"Generated inequalities: " ++ my_print_constr env ineqs) in
+		   lift_rel_context 1 eqs_rels @ ((Anonymous, None, ineqs) :: rhs_rels), 1
+	 in
 	 let rhs_env = push_rels rhs_rels' env in
-	   (*        (try trace (str "branch env: " ++ print_env rhs_env) *)
-	   (* 	with _ -> trace (str "error in print branch env")); *)
-	 let tycon = lift_tycon (List.length eqs + signlen) tycon in
+	          (try trace (str "branch env: " ++ print_env rhs_env)
+	   	with _ -> trace (str "error in print branch env"));
+	 let tycon = lift_tycon (List.length eqs + lift_ineqs + signlen) tycon in
 	   
 	 let j = typing_fun tycon rhs_env eqn.rhs.it in
-	   (* 	 (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++ *)
-	   (* 		       str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); *)
-	   (* 	  with _ -> *)
-	   (* 	    trace (str "Error in typed branch pretty printing")); *)
+	   	 (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++
+	   		       str "Typed branch: " ++ Prettyp.print_judgment rhs_env j);
+	   	  with _ ->
+	   	    trace (str "Error in typed branch pretty printing"));
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
 	 let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in
@@ -1745,6 +1783,10 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs =
 		 [] -> bref
 	       | l -> RApp (dummy_loc, bref, l)
 	 in
+	 let branch = match ineqs with
+	     Some _ -> RApp (dummy_loc, branch, [ RHole (dummy_loc, Evd.QuestionMark) ])
+	   | None -> branch
+	 in
 	   (* 	 let branch =  *)
 	   (* 	   List.fold_left (fun br (eqH, _, t) -> RLambda (dummy_loc, eqH, RHole (dummy_loc, Evd.InternalHole), br)) branch eqs_rels *)
 	   (* 	 in *)
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 539e186d5..30fd8281e 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -465,7 +465,7 @@ module Coercion = struct
 
 	
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-  let inh_conv_coerce_to loc env isevars cj ((n, t) as tycon) =
+  let inh_conv_coerce_to loc env isevars cj ((n, t) as _tycon) =
 (*     (try *)
 (*        trace (str "Subtac_coercion.inh_conv_coerce_to called for " ++ *)
 (* 	      Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++ *)
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 68ab8c46e..e624b5f32 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -178,10 +178,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let env = Global.env() in 
   let nc = named_context env in
   let nc_len = named_context_length nc in
-(*   let pr c = my_print_constr env c in *)
-(*   let prr = Printer.pr_rel_context env in *)
-(*   let prn = Printer.pr_named_context env in *)
-(*   let pr_rel env = Printer.pr_rel_context env in *)
+  let pr c = my_print_constr env c in
+  let prr = Printer.pr_rel_context env in
+  let prn = Printer.pr_named_context env in
+  let pr_rel env = Printer.pr_rel_context env in
 (*   let _ =  *)
 (*     try debug 2 (str "In named context: " ++ prn (named_context env) ++ str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++  *)
 (* 		 Ppconstr.pr_binders bl ++ str " : " ++  *)
@@ -193,40 +193,42 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let after, ((argname, _, argtyp) as arg), before = split_args (succ n) binders_rel in
   let before_length, after_length = List.length before, List.length after in
   let argid = match argname with Name n -> n | _ -> assert(false) in
-  let _liftafter = lift_binders 1 after_length after in
+  let liftafter = lift_binders 1 after_length after in
   let envwf = push_rel_context before env in
   let wf_rel, wf_rel_fun, measure_fn = 
     let rconstr_body, rconstr = 
       let app = mkAppC (r, [mkIdentC (id_of_name argname)]) in
        let env = push_rel_context [arg] envwf in
        let capp = interp_constr isevars env app in
- 	capp, mkLambda (argname, argtyp, capp)
+ 	 capp, mkLambda (argname, argtyp, capp)
      in
+      trace (str"rconstr_body: " ++ pr rconstr_body);
        if measure then
  	let lt_rel = constr_of_global (Lazy.force lt_ref) in
  	let name s = Name (id_of_string s) in
- 	let wf_rel_fun = 
- 	  (fun x y ->
- 	      mkApp (lt_rel, [| subst1 x rconstr_body; 
- 				subst1 y rconstr_body |])) 
- 	in
+ 	let wf_rel_fun lift x y = (* lift to before_env *)
+	  trace (str"lifter rconstr_body:" ++ pr (liftn lift 2 rconstr_body));
+ 	  mkApp (lt_rel, [| subst1 x (liftn lift 2 rconstr_body); 
+ 			    subst1 y (liftn lift 2 rconstr_body) |])
+	in
  	let wf_rel = 
  	  mkLambda (name "x", argtyp,
  		    mkLambda (name "y", lift 1 argtyp,
- 			      wf_rel_fun (mkRel 2) (mkRel 1)))
+ 			      wf_rel_fun 0 (mkRel 2) (mkRel 1)))
  	in
  	  wf_rel, wf_rel_fun , Some rconstr
-       else rconstr, (fun x y -> mkApp (rconstr, [|x; y|])), None
+       else rconstr, (fun lift x y -> mkApp (rconstr, [|x; y|])), None
   in
   let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |])
   in
   let argid' = id_of_string (string_of_id argid ^ "'") in
-  let wfarg len = (Name argid', None, 
+  let wfarg len = (Name argid', None,
   		   mkSubset (Name argid') (lift len argtyp) 
-		     (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
+		     (wf_rel_fun (succ len) (mkRel 1) (mkRel (len + 1))))
   in
   let top_bl = after @ (arg :: before) in
-  let intern_bl = after @ (wfarg 1 :: arg :: before) in
+  let intern_bl = liftafter @ (wfarg 1 :: arg :: before) in
+    (try trace (str "Intern bl: " ++ prr intern_bl) with _ -> ());
   let top_env = push_rel_context top_bl env in
   let _intern_env = push_rel_context intern_bl env in
   let top_arity = interp_type isevars top_env arityc in
@@ -234,36 +236,40 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let projection = 
     mkApp (proj, [| argtyp ;
 		    (mkLambda (Name argid', argtyp,
-			       (wf_rel_fun (mkRel 1) (mkRel 3)))) ;
+			       (wf_rel_fun 1 (mkRel 1) (mkRel 3)))) ;
 		    mkRel 1
 		 |])
   in
-    (*   (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ()); *)
-  let intern_arity = substnl [projection] after_length top_arity in 
-(*   (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ()); *)
+  (try trace (str "Top env: " ++ prr top_bl ++ spc () ++ str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ());
+  let intern_arity' = liftn 1 after_length top_arity in (* arity in after :: wfarg :: arg :: before *)
+  (try trace (str "intern_arity': " ++ my_print_constr _intern_env intern_arity') with _ -> ());
+  let intern_arity = substnl [projection] after_length intern_arity' in (* substitute the projection of wfarg for arg *)
+  (try trace (str "Top arity after subst: " ++ my_print_constr top_env intern_arity) with _ -> ());
+  let intern_arity = liftn 1 (succ after_length) intern_arity in (* back in after :: wfarg :: arg :: before (ie, jump over arg) *)
+  (try trace (str "Top arity after subst in intern_env: " ++ my_print_constr _intern_env intern_arity) with _ -> ());
   let intern_before_env = push_rel_context before env in
-  let intern_fun_bl = after @ [wfarg 1]  in
+  let intern_fun_bl = liftafter @ [wfarg 1]  in (* FixMe dependencies *)
 (*   (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ()); *)
   let intern_fun_arity = intern_arity in
-(*   (try debug 2 (str "Intern fun arity: " ++  *)
-(* 		  my_print_constr intern_env intern_fun_arity) with _ -> ()); *)
+  (try trace (str "Intern fun arity: " ++
+		  my_print_constr _intern_env intern_fun_arity) with _ -> ());
   let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in
   let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
-  let fun_bl = after @ (intern_fun_binder :: [arg]) in
+  let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in
 (*   (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ()); *)
   let fun_env = push_rel_context fun_bl intern_before_env in
   let fun_arity = interp_type isevars fun_env arityc in
   let intern_body = interp_casted_constr isevars fun_env body fun_arity in
   let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in
-(*   let _ =  *)
-(*       try debug 2 (str "Fun bl: " ++ prr fun_bl ++ spc () ++ *)
-(* 		   str "Intern bl" ++ prr intern_bl ++ spc () ++ *)
-(* 		   str "Top bl" ++ prr top_bl ++ spc () ++ *)
-(* 		   str "Intern arity: " ++ pr intern_arity ++ *)
-(* 		   str "Top arity: " ++ pr top_arity ++ spc () ++ *)
+  let _ =
+    try trace ((* str "Fun bl: " ++ prr fun_bl ++ spc () ++ *)
+		 str "Intern bl" ++ prr intern_bl ++ spc ())
+(* 		 str "Top bl" ++ prr top_bl ++ spc () ++ *)
+(* 		 str "Intern arity: " ++ pr intern_arity ++ *)
+(* 		 str "Top arity: " ++ pr top_arity ++ spc () ++ *)
 (* 		   str "Intern body " ++ pr intern_body_lam) *)
-(*       with _ -> () *)
-(*   in *)
+    with _ -> ()
+  in
   let _impl = 
     if Impargs.is_implicit_args()
     then Impargs.compute_implicits top_env top_arity
@@ -280,9 +286,12 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 		    prop ;
 		    intern_body_lam |])
       | Some f ->
-	  mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), 
-		 [| argtyp ; f ; prop ;
-		    intern_body_lam |])
+	  lift (succ after_length) 
+	    (mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), 
+		    [| argtyp ; 
+		       f ;
+		       prop ;
+		       intern_body_lam |]))
   in
   let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
   let def = it_mkLambda_or_LetIn def_appl binders_rel in
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index d6c1772f2..85c937cf2 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -36,8 +36,9 @@ let assumption_message id =
   Options.if_verbose message ((string_of_id id) ^ " is assumed")
 
 let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
+let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic 0)
 
-let set_default_tactic t = default_tactic := t
+let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t
 
 let evar_of_obligation o = { evar_hyps = Global.named_context_val () ;
 			     evar_concl = o.obl_type ; 
@@ -83,11 +84,11 @@ let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
 
 let _ = 
   Summary.declare_summary "program-tcc-table"
-    { Summary.freeze_function = (fun () -> !from_prg);
+    { Summary.freeze_function = (fun () -> !from_prg, !default_tactic_expr);
       Summary.unfreeze_function =
-        (fun v -> from_prg := v);
+        (fun (v, t) -> from_prg := v; set_default_tactic t);
       Summary.init_function =
-        (fun () -> from_prg := ProgMap.empty);
+        (fun () -> from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.utils_call "subtac_simpl" []));
       Summary.survive_module = false;
       Summary.survive_section = false }
 
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 3981d4c6c..ff6163b5b 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -2,7 +2,7 @@ open Util
 
 type obligation_info = (Names.identifier * Term.types * Intset.t) array
 
-val set_default_tactic : Proof_type.tactic -> unit
+val set_default_tactic : Tacexpr.glob_tactic_expr -> unit
 
 val add_definition : Names.identifier ->  Term.constr -> Term.types -> 
   obligation_info -> unit
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index fb76b35c4..258a1bdbd 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -54,6 +54,10 @@ let eq_refl = lazy (init_constant ["Init"; "Logic"] "refl_equal")
 let eq_ind_ref = lazy (init_reference ["Init"; "Logic"] "eq")
 let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal")
 
+let not_ref = lazy (init_constant ["Init"; "Logic"] "not")
+
+let and_typ = lazy (Coqlib.build_coq_and ())
+
 let eqdep_ind = lazy (init_constant [ "Logic";"Eqdep"] "eq_dep")
 let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
 let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
@@ -705,3 +709,11 @@ let pr_evar_defs evd =
     if meta_list evd = [] then mt() else
       str"METAS:"++brk(0,1)++pr_meta_map evd in
   v 0 (pp_evm ++ pp_met)
+
+let subtac_utils_path =
+  make_dirpath (List.map id_of_string ["Utils";contrib_name;"Coq"])
+let utils_tac s =
+  lazy(make_kn (MPfile subtac_utils_path) (make_dirpath []) (mk_label s))
+
+let utils_call tac args =
+  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (utils_tac tac)),args))
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 482640f9f..89a2b437b 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -40,6 +40,9 @@ val eq_refl : constr lazy_t
 val eq_ind_ref : global_reference lazy_t
 val refl_equal_ref : global_reference lazy_t
 
+val not_ref : constr lazy_t
+val and_typ : constr lazy_t
+
 val eqdep_ind : constr lazy_t
 val eqdep_rec : constr lazy_t
 val eqdep_ind_ref : global_reference lazy_t
@@ -114,3 +117,5 @@ val string_of_list : string -> ('a -> string) -> 'a list -> string
 val string_of_intset : Intset.t -> string
 
 val pr_evar_defs : evar_defs -> Pp.std_ppcmds
+
+val utils_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr