diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-25 18:19:21 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-25 18:19:21 +0000 |
| commit | 693d398b5e4e55a916bbdaa8e4c23c83d9dbcef7 (patch) | |
| tree | e015dc24293114d03433c2cf4412b4fa5df9b87c /interp/constrintern.mli | |
| parent | 217bbf499dc09f11a137fdc9aead1e0a78c760c2 (diff) | |
Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisation (add_glob* et dump_*)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
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 d3b8da8f9..27a46daf1 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 |