We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent f0d73df commit 303eca1Copy full SHA for 303eca1
plugins/ltac2/tac2intern.mli
@@ -63,10 +63,6 @@ val subst_rawexpr : substitution -> raw_tacexpr -> raw_tacexpr
63
64
(** {5 Notations} *)
65
66
-val globalize : Id.Set.t -> raw_tacexpr -> raw_tacexpr
67
-(** Replaces all qualified identifiers by their corresponding kernel name. The
68
- set represents bound variables in the context. *)
69
-
70
val debug_globalize_allow_ext : Id.Set.t -> raw_tacexpr -> raw_tacexpr
71
(** Variant of globalize which can accept CTacExt using the provided function.
72
Intended for debugging. *)
0 commit comments