Make ist (interp_sign) available to TACTIC EXTEND code

In order to do so I had to move the data base of tactics to
tacinterp (from tacintern).

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

5 files changed, 46 insertions, 36 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 2972651a9e..6e62504a3c 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -38,7 +38,7 @@ let rec make_when loc = function
   | _::l -> make_when loc l
 
 let rec make_let e = function
-  | [] -> e
+  | [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
   | GramNonTerminal(loc,t,_,Some p)::l ->
       let loc = of_coqloc loc in
       let p = Names.Id.to_string p in
@@ -159,7 +159,7 @@ let declare_tactic loc s cl =
   declare_str_items loc
     [ <:str_item< do {
       try
-        let _=Tacintern.add_tactic $se$ $make_fun_clauses loc s cl$ in
+        let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in
         List.iter
           (fun (s,l) -> match l with
            [ Some l ->
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index b7108f4d32..4662494aa1 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -129,30 +129,6 @@ let is_atomic_kn kn =
   let (_,_,l) = repr_kn kn in
   Id.Map.mem (Label.to_id l) !atomic_mactab
 
-(* Tactics table (TacExtend). *)
-
-let tac_tab = Hashtbl.create 17
-
-let add_tactic s t =
-  if Hashtbl.mem tac_tab s then
-    errorlabstrm ("Refiner.add_tactic: ")
-      (str ("Cannot redeclare tactic "^s^"."));
-  Hashtbl.add tac_tab s t
-
-let overwriting_add_tactic s t =
-  if Hashtbl.mem tac_tab s then begin
-    Hashtbl.remove tac_tab s;
-    msg_warning (strbrk ("Overwriting definition of tactic "^s))
-  end;
-  Hashtbl.add tac_tab s t
-
-let lookup_tactic s =
-  try
-    Hashtbl.find tac_tab s
-  with Not_found ->
-    errorlabstrm "Refiner.lookup_tactic"
-      (str"The tactic " ++ str s ++ str" is not installed.")
-
 (* Summary and Object declaration *)
 
 let mactab =
@@ -528,6 +504,9 @@ let clause_app f = function
   | { onhyps=Some l; concl_occs=nl } ->
       { onhyps=Some(List.map f l); concl_occs=nl}
 
+let assert_tactic_installed = ref (fun _ -> ())
+let set_assert_tactic_installed f = assert_tactic_installed := f
+
 (* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *)
 let rec intern_atomic lf ist x =
   match (x:raw_atomic_tactic_expr) with
@@ -660,7 +639,7 @@ let rec intern_atomic lf ist x =
 
   (* For extensions *)
   | TacExtend (loc,opn,l) ->
-      let _ = lookup_tactic opn in
+      !assert_tactic_installed opn;
       TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l)
   | TacAlias (loc,s,l,(dir,body)) ->
       let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index 5f302f1b9a..c928b73799 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -72,14 +72,6 @@ val add_tacdef :
   (Libnames.reference * bool * raw_tactic_expr) list -> unit
 val add_primitive_tactic : string -> glob_tactic_expr -> unit
 
-(** Tactic extensions *)
-val add_tactic :
-  string -> (typed_generic_argument list -> tactic) -> unit
-val overwriting_add_tactic :
-  string -> (typed_generic_argument list -> tactic) -> unit
-val lookup_tactic :
-  string -> (typed_generic_argument list) -> tactic
-
 val lookup_ltacref : ltac_constant -> glob_tactic_expr
 
 (** printing *)
@@ -89,3 +81,6 @@ val print_ltac : Libnames.qualid -> std_ppcmds
 
 val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr
 val dump_glob_red_expr : raw_red_expr -> unit
+
+(* Implemented in tacinterp *)
+val set_assert_tactic_installed : (string -> unit) -> unit
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 6e2aceaff9..6c66f4ced2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -137,6 +137,34 @@ let ((value_in : value -> Dyn.t),
 
 let valueIn t = TacDynamic (Loc.ghost,value_in t)
 
+(* Tactics table (TacExtend). *)
+
+let tac_tab = Hashtbl.create 17
+
+let add_tactic s t =
+  if Hashtbl.mem tac_tab s then
+    errorlabstrm ("Refiner.add_tactic: ")
+      (str ("Cannot redeclare tactic "^s^"."));
+  Hashtbl.add tac_tab s t
+
+let overwriting_add_tactic s t =
+  if Hashtbl.mem tac_tab s then begin
+    Hashtbl.remove tac_tab s;
+    msg_warning (strbrk ("Overwriting definition of tactic "^s))
+  end;
+  Hashtbl.add tac_tab s t
+
+let lookup_tactic s =
+  try
+    Hashtbl.find tac_tab s
+  with Not_found ->
+    errorlabstrm "Refiner.lookup_tactic"
+      (str"The tactic " ++ str s ++ str" is not installed.")
+
+let () =
+  Tacintern.set_assert_tactic_installed (fun opn ->
+     let _ignored = lookup_tactic opn in ())
+
 (** Generic arguments : table of interpretation functions *)
 
 type interp_genarg_type =
@@ -1855,7 +1883,7 @@ and interp_atomic ist gl tac =
 	  sigma , a_interp::acc
 	end l (project gl,[])
       in
-      tac args
+      tac args ist
   | TacAlias (loc,s,l,(_,body)) -> fun gl ->
     let evdref = ref gl.sigma in
     let f x = match genarg_tag x with
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index eba62f5d70..1352d72485 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -42,6 +42,14 @@ and interp_sign =
 val extract_ltac_constr_values : interp_sign -> Environ.env ->
   Pretyping.ltac_var_map
 
+(** Tactic extensions *)
+val add_tactic :
+  string -> (typed_generic_argument list -> interp_sign -> tactic) -> unit
+val overwriting_add_tactic :
+  string -> (typed_generic_argument list -> interp_sign -> tactic) -> unit
+val lookup_tactic :
+  string -> (typed_generic_argument list) -> interp_sign -> tactic
+
 (** To embed several objects in Coqast.t *)
 val tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t
 val tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr)