diff options
| author | Pierre-Marie Pédrot | 2016-09-07 18:02:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-08 15:52:56 +0200 |
| commit | dfac5aa2285de5b89f08ada3c30c0a1594737440 (patch) | |
| tree | 37fa3f3481d03c4a777595e1ec0eab631cd528aa /ltac | |
| parent | 13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (diff) | |
Making Vernacexpr independent from Tacexpr.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/g_ltac.ml4 | 8 | ||||
| -rw-r--r-- | ltac/tacentries.ml | 4 | ||||
| -rw-r--r-- | ltac/tacentries.mli | 2 | ||||
| -rw-r--r-- | ltac/tacintern.ml | 6 |
4 files changed, 11 insertions, 9 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index c67af33e23..42276ad3f3 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -287,15 +287,15 @@ GEXTEND Gram (* Definitions for tactics *) tacdef_body: [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> - if redef then Vernacexpr.TacticRedefinition (name, TacFun (it, body)) + if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) else let id = reference_to_id name in - Vernacexpr.TacticDefinition (id, TacFun (it, body)) + Tacexpr.TacticDefinition (id, TacFun (it, body)) | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> - if redef then Vernacexpr.TacticRedefinition (name, body) + if redef then Tacexpr.TacticRedefinition (name, body) else let id = reference_to_id name in - Vernacexpr.TacticDefinition (id, body) + Tacexpr.TacticDefinition (id, body) ] ] ; tactic: diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 2fed0e14f2..2d7b7bf137 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -425,7 +425,7 @@ let warn_unusable_identifier = let register_ltac local tacl = let map tactic_body = match tactic_body with - | TacticDefinition ((loc,id), body) -> + | Tacexpr.TacticDefinition ((loc,id), body) -> let kn = Lib.make_kn id in let id_pp = pr_id id in let () = if is_defined_tac kn then @@ -441,7 +441,7 @@ let register_ltac local tacl = in let () = if is_shadowed then warn_unusable_identifier id in NewTac id, body - | TacticRedefinition (ident, body) -> + | Tacexpr.TacticRedefinition (ident, body) -> let loc = loc_of_reference ident in let kn = try Nametab.locate_tactic (snd (qualid_of_reference ident)) diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli index 27df819ee6..969c118fb5 100644 --- a/ltac/tacentries.mli +++ b/ltac/tacentries.mli @@ -13,7 +13,7 @@ open Tacexpr (** {5 Tactic Definitions} *) -val register_ltac : locality_flag -> Vernacexpr.tacdef_body list -> unit +val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit (** Adds new Ltac definitions to the environment. *) (** {5 Tactic Notations} *) diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index cd791398d9..b6ff32ac3d 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -796,11 +796,13 @@ let () = (* Backwarding recursive needs of tactic glob/interp/eval functions *) let _ = - let f l = + (** FIXME: use generic internalization *) + let f l tac = + let tac = out_gen (rawwit Constrarg.wit_ltac) tac in 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 { (make_empty_glob_sign()) with ltacvars }) + (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars }) tac in Hook.set Hints.extern_intern_tac f |