Merge PR#608: Allow Ltac2 as a plugin

4 files changed, 27 insertions, 24 deletions

diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 7d4075836..4dceb0331 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -31,7 +31,7 @@ let () =
   Obligations.default_tactic := tac
 
 let with_tac f tac =
-  let env = { Genintern.genv = Global.env (); ltacvars = Names.Id.Set.empty } in
+  let env = Genintern.empty_glob_sign (Global.env ()) in
   let tac = match tac with
   | None -> None
   | Some tac ->
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index da7f11472..6c7eb8c89 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -39,13 +39,12 @@ let error_tactic_expected ?loc =
 type glob_sign = Genintern.glob_sign = {
   ltacvars : Id.Set.t;
      (* ltac variables and the subset of vars introduced by Intro/Let/... *)
-  genv : Environ.env }
+  genv : Environ.env;
+  extra : Genintern.Store.t;
+}
 
-let fully_empty_glob_sign =
-  { ltacvars = Id.Set.empty; genv = Environ.empty_env }
-
-let make_empty_glob_sign () =
-  { fully_empty_glob_sign with genv = Global.env () }
+let fully_empty_glob_sign = Genintern.empty_glob_sign Environ.empty_env
+let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ())
 
 (* We have identifier <| global_reference <| constr *)
 
@@ -190,12 +189,13 @@ let intern_binding_name ist x =
      and if a term w/o ltac vars, check the name is indeed quantified *)
   x
 
-let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c =
+let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
   let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
   let ltacvars = {
     Constrintern.ltac_vars = lfun;
     ltac_bound = Id.Set.empty;
+    ltac_extra = extra;
   } in
   let c' =
     warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c
@@ -311,6 +311,7 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc =
   let ltacvars = {
     Constrintern.ltac_vars = ltacvars;
     ltac_bound = Id.Set.empty;
+    ltac_extra = ist.extra;
   } in
   let metas,pat = Constrintern.intern_constr_pattern
     ist.genv ~as_type ~ltacvars pc
@@ -342,7 +343,11 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
       let r = match r with
       | AN r -> r
       | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in
-      let sign = { Constrintern.ltac_vars = ist.ltacvars; Constrintern.ltac_bound = Id.Set.empty } in
+      let sign = {
+        Constrintern.ltac_vars = ist.ltacvars;
+        ltac_bound = Id.Set.empty;
+        ltac_extra = ist.extra;
+      } in
       let c = Constrintern.interp_reference sign r in
       match c.CAst.v with
       | GRef (r,None) ->
@@ -706,8 +711,7 @@ let glob_tactic_env l env x =
   let ltacvars =
     List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
   Flags.with_option strict_check
-  (intern_pure_tactic
-    { ltacvars; genv = env })
+  (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars })
     x
 
 let split_ltac_fun = function
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 71ca354fa..8ad52ca02 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -18,7 +18,9 @@ open Misctypes
 
 type glob_sign = Genintern.glob_sign = {
   ltacvars : Id.Set.t;
-  genv : Environ.env }
+  genv : Environ.env;
+  extra : Genintern.Store.t;
+}
 
 val fully_empty_glob_sign : glob_sign
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 8a10a4d76..8ed65c5d9 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -585,6 +585,7 @@ let interp_uconstr ist env sigma = function
       let ltacvars = {
         Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped));
         ltac_bound = Id.Map.domain ist.lfun;
+        ltac_extra = Genintern.Store.empty;
       } in
       { closure ; term =  intern_gen WithoutTypeConstraint ~ltacvars env ce }
 
@@ -612,6 +613,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
       let ltacvars = {
         ltac_vars = constr_context;
         ltac_bound = Id.Map.domain ist.lfun;
+        ltac_extra = Genintern.Store.empty;
       } in
       let kind_for_intern =
         match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
@@ -1964,8 +1966,7 @@ let interp_tac_gen lfun avoid_ids debug t =
   let ist = { lfun = lfun; extra = extra } in
   let ltacvars = Id.Map.domain lfun in
   interp_tactic ist
-    (intern_pure_tactic {
-      ltacvars; genv = env } t)
+    (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
   end }
 
 let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
@@ -1974,7 +1975,7 @@ let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
 (* [global] means that [t] should be internalized outside of goals. *)
 let hide_interp global t ot =
   let hide_interp env =
-    let ist = { ltacvars = Id.Set.empty; genv = env } in
+    let ist = Genintern.empty_glob_sign env in
     let te = intern_pure_tactic ist t in
     let t = eval_tactic te in
     match ot with
@@ -2097,17 +2098,13 @@ let interp_redexp env sigma r =
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
 let _ =
-  let eval ty env sigma lfun arg =
+  let eval lfun env sigma ty tac =
     let ist = { lfun = lfun; extra = TacStore.empty; } in
-    if Genarg.has_type arg (glbwit wit_tactic) then
-      let tac = Genarg.out_gen (glbwit wit_tactic) arg in
-      let tac = interp_tactic ist tac in
-      let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
-      (EConstr.of_constr c, sigma)
-    else
-      failwith "not a tactic"
+    let tac = interp_tactic ist tac in
+    let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
+    (EConstr.of_constr c, sigma)
   in
-  Hook.set Pretyping.genarg_interp_hook eval
+  Pretyping.register_constr_interp0 wit_tactic eval
 
 (** Used in tactic extension **)