aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/astterm.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 54c1ce5c2..b33c4b825 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -50,7 +50,9 @@ val fconstr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr
val raw_constr_of_compattern :
'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr
+*)
val globalize_command : Coqast.t -> Coqast.t
+(*
val globalize_ast : Coqast.t -> Coqast.t
(* Typing with Trad, and re-checking with Mach *)