diff options
Diffstat (limited to 'parsing/coqast.mli')
| -rw-r--r-- | parsing/coqast.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/parsing/coqast.mli b/parsing/coqast.mli index b5ad45c74..a304aa06b 100644 --- a/parsing/coqast.mli +++ b/parsing/coqast.mli @@ -10,6 +10,7 @@ (*i*) open Names +open Libnames (*i*) (* Abstract syntax trees. *) @@ -25,7 +26,7 @@ type t = | Num of loc * int | Str of loc * string | Id of loc * string - | Path of loc * section_path + | Path of loc * kernel_name | Dynamic of loc * Dyn.t (* returns the list of metas occuring in the ast *) @@ -38,9 +39,11 @@ val subst_meta : (int * t) list -> t -> t (* hash-consing function *) val hcons_ast: (string -> string) * (Names.identifier -> Names.identifier) - * (section_path -> section_path) + * (kernel_name -> kernel_name) -> (t -> t) * (loc -> loc) +val subst_ast: Names.substitution -> t -> t + (* val map_tactic_expr : (t -> t) -> (tactic_expr -> tactic_expr) -> tactic_expr -> tactic_expr val fold_tactic_expr : |