diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index d3b8da8f9e..27a46daf19 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -144,10 +144,3 @@ val interp_aconstr : implicits_env -> identifier list -> constr_expr -> (* Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b - -(* Coqdoc utility functions *) -type coqdoc_state -val coqdoc_freeze : unit -> coqdoc_state -val coqdoc_unfreeze : coqdoc_state -> unit - -val add_glob : Util.loc -> global_reference -> unit |