diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 12 | ||||
| -rw-r--r-- | src/tac2env.ml | 6 | ||||
| -rw-r--r-- | src/tac2env.mli | 6 | ||||
| -rw-r--r-- | src/tac2intern.ml | 6 |
4 files changed, 21 insertions, 9 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index b8bec37d04..e1aa6eb48c 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -779,7 +779,7 @@ let gtypref kn = GTypRef (Other kn, []) let intern_constr self ist c = let (_, (c, _)) = Genintern.intern Stdarg.wit_constr ist c in - (c, gtypref t_constr) + (GlbVal c, gtypref t_constr) let interp_constr flags ist c = let open Pretyping in @@ -821,7 +821,7 @@ let () = let interp _ id = return (ValExt (Value.val_ident, id)) in let print _ id = str "ident:(" ++ Id.print id ++ str ")" in let obj = { - ml_intern = (fun _ _ id -> id, gtypref t_ident); + ml_intern = (fun _ _ id -> GlbVal id, gtypref t_ident); ml_interp = interp; ml_subst = (fun _ id -> id); ml_print = print; @@ -831,7 +831,7 @@ let () = let () = let intern self ist c = let _, pat = Constrintern.intern_constr_pattern ist.Genintern.genv ~as_type:false c in - pat, gtypref t_pattern + GlbVal pat, gtypref t_pattern in let print env pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env Evd.empty pat ++ str ")" in let interp _ c = return (ValExt (Value.val_pattern, c)) in @@ -846,14 +846,14 @@ let () = let () = let intern self ist qid = match qid with | Libnames.Ident (_, id) -> - Globnames.VarRef id, gtypref t_reference + GlbVal (Globnames.VarRef id), gtypref t_reference | Libnames.Qualid (loc, qid) -> let gr = try Nametab.locate qid with Not_found -> Nametab.error_global_not_found ?loc qid in - gr, gtypref t_reference + GlbVal gr, gtypref t_reference in let subst s c = Globnames.subst_global_reference s c in let interp _ gr = return (Value.of_reference gr) in @@ -875,7 +875,7 @@ let () = let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in let ist = { ist with Genintern.extra } in let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in - tac, gtypref t_unit + GlbVal tac, gtypref t_unit in let interp _ tac = (** FUCK YOU API *) diff --git a/src/tac2env.ml b/src/tac2env.ml index 56fd55ee84..5a817df713 100644 --- a/src/tac2env.ml +++ b/src/tac2env.ml @@ -251,10 +251,14 @@ let shortest_qualid_of_projection kn = let sp = KNmap.find kn tab.tab_proj_rev in KnTab.shortest_qualid Id.Set.empty sp tab.tab_proj +type 'a or_glb_tacexpr = +| GlbVal of 'a +| GlbTacexpr of glb_tacexpr + type ('a, 'b, 'r) intern_fun = Genintern.glob_sign -> 'a -> 'b * 'r glb_typexpr type ('a, 'b) ml_object = { - ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b, 'r) intern_fun; + ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun; ml_subst : Mod_subst.substitution -> 'b -> 'b; ml_interp : environment -> 'b -> valexpr Proofview.tactic; ml_print : Environ.env -> 'b -> Pp.t; diff --git a/src/tac2env.mli b/src/tac2env.mli index 15664db756..eb18dc8e39 100644 --- a/src/tac2env.mli +++ b/src/tac2env.mli @@ -105,10 +105,14 @@ val interp_primitive : ml_tactic_name -> ml_tactic (** {5 ML primitive types} *) +type 'a or_glb_tacexpr = +| GlbVal of 'a +| GlbTacexpr of glb_tacexpr + type ('a, 'b, 'r) intern_fun = Genintern.glob_sign -> 'a -> 'b * 'r glb_typexpr type ('a, 'b) ml_object = { - ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b, 'r) intern_fun; + ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun; ml_subst : Mod_subst.substitution -> 'b -> 'b; ml_interp : environment -> 'b -> valexpr Proofview.tactic; ml_print : Environ.env -> 'b -> Pp.t; diff --git a/src/tac2intern.ml b/src/tac2intern.ml index 5d2fc2b47b..2b234d7aec 100644 --- a/src/tac2intern.ml +++ b/src/tac2intern.ml @@ -789,7 +789,11 @@ let rec intern_rec env = function let ist = empty_glob_sign genv in let ist = { ist with extra = Store.set ist.extra ltac2_env env } in let arg, tpe = Flags.with_option Ltac_plugin.Tacintern.strict_check (fun () -> obj.ml_intern self ist arg) () in - (GTacExt (tag, arg), tpe) + let e = match arg with + | GlbVal arg -> GTacExt (tag, arg) + | GlbTacexpr e -> e + in + (e, tpe) and intern_rec_with_constraint env e exp = let loc = loc_of_tacexpr e in |