Move Program tactics into a proper theories/ directory as they are general purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module.

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

10 files changed, 18 insertions, 467 deletions

diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
deleted file mode 100644
index f047b729d..000000000
--- a/contrib/subtac/FixSub.v
+++ /dev/null
@@ -1,147 +0,0 @@
-Require Import Wf.
-Require Import Coq.subtac.Utils.
-
-(** Reformulation of the Wellfounded module using subsets where possible. *)
-
-Section Well_founded.
-  Variable A : Type.
-  Variable R : A -> A -> Prop.
-  Hypothesis Rwf : well_founded R.
-  
-  Section Acc.
-    
-    Variable P : A -> Type.
-    
-    Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
-    
-    Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x :=
-      F_sub x (fun y: { y : A | R y x}  => Fix_F_sub (proj1_sig y) 
-        (Acc_inv r (proj1_sig y) (proj2_sig y))).
-    
-    Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
-  End Acc.
-  
-  Section FixPoint.
-    Variable P : A -> Type.
-    
-    Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
-    
-    Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *)
-    
-    Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x).
-    
-    Hypothesis
-      F_ext :
-      forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)),
-        (forall y:{ y:A | R y x}, f y = g y) -> F_sub x f = F_sub x g.
-
-    Lemma Fix_F_eq :
-      forall (x:A) (r:Acc R x),
-        F_sub x (fun (y:{y:A|R y x}) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r.
-    Proof. 
-      destruct r using Acc_inv_dep; auto.
-    Qed.
-    
-    Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F x r = Fix_F x s.
-    Proof.
-      intro x; induction (Rwf x); intros.
-      rewrite <- (Fix_F_eq x r); rewrite <- (Fix_F_eq x s); intros.
-      apply F_ext; auto.
-      intros.
-      rewrite (proof_irrelevance (Acc R x) r s) ; auto.
-    Qed.
-
-    Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:{y:A|R y x}) => Fix (proj1_sig y)).
-    Proof.
-      intro x; unfold Fix in |- *.
-      rewrite <- (Fix_F_eq ).
-      apply F_ext; intros.
-      apply Fix_F_inv.
-    Qed.
-
-    Lemma fix_sub_eq :
-        forall x : A,
-          Fix_sub P F_sub x =
-          let f_sub := F_sub in
-            f_sub x (fun  {y : A | R y x}=> Fix (`y)).
-      exact Fix_eq.
-    Qed.
-
- End FixPoint.
-
-End Well_founded.
-
-Extraction Inline Fix_F_sub Fix_sub.
-
-Require Import Wf_nat.
-Require Import Lt.
-
-Section Well_founded_measure.
-  Variable A : Type.
-  Variable m : A -> nat.
-  
-  Section Acc.
-    
-    Variable P : A -> Type.
-    
-    Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x.
-    
-    Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
-      F_sub x (fun y: { y : A | m y < m x}  => Fix_measure_F_sub (proj1_sig y) 
-        (Acc_inv r (m (proj1_sig y)) (proj2_sig y))).
-    
-    Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)).
-  
-  End Acc.
-
-  Section FixPoint.
-    Variable P : A -> Type.
-    
-    Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x.
-    
-    Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *)
-    
-    Definition Fix_measure (x:A) := Fix_measure_F_sub P F_sub x (lt_wf (m x)).
-    
-    Hypothesis
-      F_ext :
-      forall (x:A) (f g:forall y:{y:A | m y < m x}, P (`y)),
-        (forall y:{ y:A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g.
-
-    Lemma Fix_measure_F_eq :
-      forall (x:A) (r:Acc lt (m x)),
-        F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (m (proj1_sig y)) (proj2_sig y))) = Fix_F x r.
-    Proof.
-      intros x.
-      set (y := m x).
-      unfold Fix_measure_F_sub.
-      intros r ; case r ; auto.
-    Qed.
-    
-    Lemma Fix_measure_F_inv : forall (x:A) (r s:Acc lt (m x)), Fix_F x r = Fix_F x s.
-    Proof.
-      intros x r s.
-      rewrite (proof_irrelevance (Acc lt (m x)) r s) ; auto.
-    Qed.
-
-    Lemma Fix_measure_eq : forall x:A, Fix_measure x = F_sub x (fun (y:{y:A| m y < m x}) => Fix_measure (proj1_sig y)).
-    Proof.
-      intro x; unfold Fix_measure in |- *.
-      rewrite <- (Fix_measure_F_eq ).
-      apply F_ext; intros.
-      apply Fix_measure_F_inv.
-    Qed.
-
-    Lemma fix_measure_sub_eq :
-        forall x : A,
-          Fix_measure_sub P F_sub x =
-          let f_sub := F_sub in
-            f_sub x (fun  {y : A | m y < m x}=> Fix_measure (`y)).
-      exact Fix_measure_eq.
-    Qed.
-
- End FixPoint.
-
-End Well_founded_measure.
-
-Extraction Inline Fix_measure_F_sub Fix_measure_sub.
diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v
deleted file mode 100644
index 4610f3467..000000000
--- a/contrib/subtac/FunctionalExtensionality.v
+++ /dev/null
@@ -1,47 +0,0 @@
-Lemma equal_f : forall A B : Type, forall (f g : A -> B), 
-  f = g -> forall x, f x = g x.
-Proof.
-  intros.
-  rewrite H.
-  auto.
-Qed.
-
-Axiom fun_extensionality : forall A B (f g : A -> B), 
-  (forall x, f x = g x) -> f = g.
-
-Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), forall (f g : forall x : A, B x), 
-  (forall x, f x = g x) -> f = g.
-
-Hint Resolve fun_extensionality fun_extensionality_dep : subtac.
-
-Require Import Coq.subtac.Utils.
-Require Import Coq.subtac.FixSub.
-
-Lemma fix_sub_eq_ext :
-  forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R)
-    (P : A -> Set)
-    (F_sub : forall x : A, (forall  {y : A | R y x}, P (`y)) -> P x),
-    forall x : A,
-      Fix_sub A R Rwf P F_sub x =
-        F_sub x (fun {y : A | R y x}=> Fix A R Rwf P F_sub (`y)).
-Proof.
-  intros ; apply Fix_eq ; auto.
-  intros.
-  assert(f = g).
-  apply (fun_extensionality_dep _ _ _ _ H).
-  rewrite H0 ; auto.
-Qed.
-
-Lemma fix_sub_measure_eq_ext :
-  forall (A : Type) (f : A -> nat) (P : A -> Type)
-    (F_sub : forall x : A, (forall  {y : A | f y < f x}, P (`y)) -> P x),
-    forall x : A,
-      Fix_measure_sub A f P F_sub x =
-        F_sub x (fun {y : A | f y < f x}=> Fix_measure_sub A f P F_sub (`y)).
-Proof.
-  intros ; apply Fix_measure_eq ; auto.
-  intros.
-  assert(f0 = g).
-  apply (fun_extensionality_dep _ _ _ _ H).
-  rewrite H0 ; auto.
-Qed.
diff --git a/contrib/subtac/Heq.v b/contrib/subtac/Heq.v
deleted file mode 100644
index f2b216d96..000000000
--- a/contrib/subtac/Heq.v
+++ /dev/null
@@ -1,34 +0,0 @@
-Require Export JMeq.
-
-(** Notation for heterogenous equality. *)
-
-Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level).
-
-(** Do something on an heterogeneous equality appearing in the context. *)
-
-Ltac on_JMeq tac := 
-  match goal with
-    | [ H : @JMeq ?x ?X ?y ?Y |- _ ] => tac H
-  end.
-
-(** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *)
-
-Ltac simpl_one_JMeq :=
-  on_JMeq 
-  ltac:(fun H => let H' := fresh "H" in 
-    assert (H' := JMeq_eq H) ; clear H ; rename H' into H).
-
-(** Repeat it for every possible hypothesis. *)
-
-Ltac simpl_JMeq := repeat simpl_one_JMeq.
-
-(** Just simplify an h.eq. without clearing it. *)
-
-Ltac simpl_one_dep_JMeq :=
-  on_JMeq
-  ltac:(fun H => let H' := fresh "H" in 
-    assert (H' := JMeq_eq H)).
-
-
-
-
diff --git a/contrib/subtac/Subtac.v b/contrib/subtac/Subtac.v
deleted file mode 100644
index 9912cd242..000000000
--- a/contrib/subtac/Subtac.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Require Export Coq.subtac.Utils.
-Require Export Coq.subtac.FixSub.
\ No newline at end of file
diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v
deleted file mode 100644
index a00234dde..000000000
--- a/contrib/subtac/SubtacTactics.v
+++ /dev/null
@@ -1,158 +0,0 @@
-Ltac induction_with_subterm c H :=
-  let x := fresh "x" in
-  let y := fresh "y" in
-  (remember c as x ; rewrite <- y in H ; induction H ; subst).
-
-Ltac induction_on_subterm c :=
-  let x := fresh "x" in
-  let y := fresh "y" in
-  (set(x := c) ; assert(y:x = c) by reflexivity ; clearbody x ; induction x ; inversion y ; try subst ; 
-  clear y).
-
-Ltac induction_with_subterms c c' H :=
-  let x := fresh "x" in
-  let y := fresh "y" in
-  let z := fresh "z" in
-  let w := fresh "w" in
-  (set(x := c) ; assert(y:x = c) by reflexivity ;
-  set(z := c') ; assert(w:z = c') by reflexivity ;
-  rewrite <- y in H ; rewrite <- w in H ; 
-  induction H ; subst).
-
-
-Ltac destruct_one_pair :=
- match goal with
-   | [H : (_ /\ _) |- _] => destruct H
-   | [H : prod _ _ |- _] => destruct H
- end.
-
-Ltac destruct_pairs := repeat (destruct_one_pair).
-
-Ltac destruct_one_ex :=
-  let tac H := let ph := fresh "H" in destruct H as [H ph] in
-    match goal with
-      | [H : (ex _) |- _] => tac H
-      | [H : (sig ?P) |- _ ] => tac H
-      | [H : (ex2 _) |- _] => tac H
-    end.
-
-Ltac destruct_exists := repeat (destruct_one_ex).
-
-Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht].
-
-Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H].
-
-Tactic Notation "contradiction" "by" constr(t) := 
-  let H := fresh in assert t as H by auto with * ; contradiction.
-
-Ltac discriminates :=
-  match goal with
-    | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity
-    | _ => discriminate
-  end.
-
-Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex).
-
-Ltac on_last_hyp tac := 
-  match goal with
-    [ H : _ |- _ ] => tac H
-  end.
-
-Tactic Notation "on_last_hyp" tactic(t) := on_last_hyp t.
-
-Ltac revert_last := 
-  match goal with
-    [ H : _ |- _ ] => revert H
-  end.
-
-Ltac reverse := repeat revert_last.
-
-Ltac on_call f tac :=
-  match goal with
-    | H : ?T |- _  =>
-      match T with
-        | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u)
-        | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v)
-        | context [f ?x ?y ?z ?w] => tac (f x y z w)
-        | context [f ?x ?y ?z] => tac (f x y z)
-        | context [f ?x ?y] => tac (f x y) 
-        | context [f ?x] => tac (f x)
-      end
-    | |- ?T  =>
-      match T with
-        | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u)
-        | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v)
-        | context [f ?x ?y ?z ?w] => tac (f x y z w)
-        | context [f ?x ?y ?z] => tac (f x y z)
-        | context [f ?x ?y] => tac (f x y)
-        | context [f ?x] => tac (f x)
-      end
-  end.
-
-(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *)
-Ltac destruct_call f :=
-  let tac t := destruct t in on_call f tac.
-
-Ltac destruct_call_as f l :=
-  let tac t := destruct t as l in on_call f tac.
-
-Tactic Notation "destruct_call" constr(f) := destruct_call f.
-Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := destruct_call_as f l.
-
-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 ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g'  |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H
-      | _ => idtac
-    end.
-
-Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0.
-
-Ltac bang :=
-  match goal with
-    | |- ?x => 
-      match x with
-        | context [False_rect _ ?p] => elim p
-      end
-  end.
-
-Require Import Eqdep.
-
-Ltac elim_eq_rect :=
-  match goal with
-    | [ |- ?t ] => 
-      match t with
-        | context [ @eq_rect _ _ _ _ _ ?p ] => 
-          let P := fresh "P" in 
-            set (P := p); simpl in P ; 
-	      try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
-        | context [ @eq_rect _ _ _ _ _ ?p _ ] => 
-          let P := fresh "P" in 
-            set (P := p); simpl in P ; 
-	      try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
-      end
-  end.
-
-Ltac real_elim_eq_rect :=
-  match goal with
-    | [ |- ?t ] => 
-      match t with
-        | context [ @eq_rect _ _ _ _ _ ?p ] => 
-          let P := fresh "P" in 
-            set (P := p); simpl in P ; 
-	      ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
-        | context [ @eq_rect _ _ _ _ _ ?p _ ] => 
-          let P := fresh "P" in 
-            set (P := p); simpl in P ; 
-	      ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
-      end
-  end.
- 
\ No newline at end of file
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
deleted file mode 100644
index 76f49dd3b..000000000
--- a/contrib/subtac/Utils.v
+++ /dev/null
@@ -1,65 +0,0 @@
-Require Export Coq.subtac.SubtacTactics.
-
-Set Implicit Arguments.
-
-(** Wrap a proposition inside a subset. *)
-
-Notation " {{ x }} " := (tt : { y : unit | x }).
-
-(** A simpler notation for subsets defined on a cartesian product. *)
-
-Notation "{ ( x , y )  :  A  |  P }" := 
-  (sig (fun anonymous : A => let (x,y) := anonymous in P))
-  (x ident, y ident) : type_scope.
-
-(** Generates an obligation to prove False. *)
-
-Notation " ! " := (False_rect _ _).
-
-(** Abbreviation for first projection and hiding of proofs of subset objects. *)
-
-Notation " ` t " := (proj1_sig t) (at level 10) : core_scope.
-Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
-
-(** Coerces objects to their support before comparing them. *)
-
-Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70).
-
-(** Quantifying over subsets. *)
-
-Notation "'fun' { x : A | P } => Q" :=
-  (fun x:{x:A|P} => Q)
-  (at level 200, x ident, right associativity).
-
-Notation "'forall' { x : A | P } , Q" :=
-  (forall x:{x:A|P}, Q)
-  (at level 200, x ident, right associativity).
-
-Require Import Coq.Bool.Sumbool.
-
-(** Construct a dependent disjunction from a boolean. *)
-
-Notation "'dec'" := (sumbool_of_bool) (at level 0). 
-
-(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *)
-
-Notation in_right := (@right _ _ _).
-Notation in_left := (@left _ _ _).
-
-(** Default simplification tactic. *)
-
-Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; 
-  try (solve [ red ; intros ; discriminate ]) ; auto with *.  
-
-(** Extraction directives *)
-Extraction Inline proj1_sig.
-Extract Inductive unit => "unit" [ "()" ].
-Extract Inductive bool => "bool" [ "true" "false" ].
-Extract Inductive sumbool => "bool" [ "true" "false" ].
-(* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *)
-(* Extract Inductive sigT => "prod" [ "" ]. *)
-
-Require Export ProofIrrelevance.
-Require Export Coq.subtac.Heq.
-
-Delimit Scope program_scope with program.
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index e774dd127..d38bdb79e 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -95,8 +95,8 @@ let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
 (*   check_required_library ["Coq";"Logic";"JMeq"]; *)
-  require_library "Coq.subtac.FixSub";
-  require_library "Coq.subtac.Utils";
+  require_library "Coq.Program.FixSub";
+  require_library "Coq.Program.Tactics";
   require_library "Coq.Logic.JMeq";
   let env = Global.env () in
   let isevars = ref (create_evar_defs Evd.empty) in
@@ -125,6 +125,10 @@ let subtac (loc, command) =
       | VernacAssumption (stre,nl,l) -> 
 	  vernac_assumption env isevars stre l nl
 
+(*       | VernacCoFixpoint (l, b) ->  *)
+(* 	  let _ = trace (str "Building cofixpoint") in *)
+(* 	    ignore(Subtac_command.build_recursive l b) *)
+
       (*| VernacEndProof e -> 
 	  subtac_end_proof e*)
 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 1bd85b92b..656c4397d 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -13,7 +13,7 @@ open Decl_kinds
 open Util
 open Evd
 
-let pperror cmd = Util.errorlabstrm "Subtac" cmd
+let pperror cmd = Util.errorlabstrm "Program" cmd
 let error s = pperror (str s)
 
 exception NoObligations of identifier option
@@ -96,7 +96,7 @@ let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
 let freeze () = !from_prg, !default_tactic_expr
 let unfreeze (v, t) = from_prg := v; set_default_tactic t
 let init () =
-  from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.utils_call "subtac_simpl" [])
+  from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "program_simpl" [])
 
 let _ = 
   Summary.declare_summary "program-tcc-table"
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index b557b4056..e5ac65878 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -10,7 +10,7 @@ let ($) f x = f x
 (****************************************************************************)
 (* Library linking *)
 
-let contrib_name = "subtac"
+let contrib_name = "Program"
 
 let subtac_dir = [contrib_name]
 let fix_sub_module = "FixSub"
@@ -28,8 +28,8 @@ let make_ref l s = lazy (init_reference l s)
 let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
 let acc_ref = make_ref  ["Init";"Wf"] "Acc"
 let acc_inv_ref = make_ref  ["Init";"Wf"] "Acc_inv"
-let fix_sub_ref = make_ref ["subtac";"FixSub"] "Fix_sub"
-let fix_measure_sub_ref = make_ref ["subtac";"FixSub"] "Fix_measure_sub"
+let fix_sub_ref = make_ref [contrib_name;"FixSub"] "Fix_sub"
+let fix_measure_sub_ref = make_ref [contrib_name;"FixSub"] "Fix_measure_sub"
 let lt_ref = make_ref ["Init";"Peano"] "lt"
 let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf"
 let refl_ref = make_ref ["Init";"Logic"] "refl_equal"
@@ -441,11 +441,11 @@ let pr_evar_defs evd =
       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 contrib_tactics_path =
+  make_dirpath (List.map id_of_string ["Tactics";contrib_name;"Coq"])
+let tactics_tac s =
+  lazy(make_kn (MPfile contrib_tactics_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 tactics_call tac args =
+  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args))
 
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 5a5dd4274..bbf536c41 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -125,6 +125,6 @@ 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
+val tactics_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr
 
 val pp_list : ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds