diff options
| author | letouzey | 2012-05-29 11:09:15 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-29 11:09:15 +0000 |
| commit | 6d961ac24305f26e896b602bdabe0e9c3c7cbf05 (patch) | |
| tree | dadc934c94e026149da2ae08144af769f4e9cb6c /intf | |
| parent | 255f7938cf92216bc134099c50bd8258044be644 (diff) | |
global_reference migrated from Libnames to new Globnames, less deps in grammar.cma
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/evar_kinds.mli | 2 | ||||
| -rw-r--r-- | intf/glob_term.mli | 1 | ||||
| -rw-r--r-- | intf/notation_term.mli | 2 | ||||
| -rw-r--r-- | intf/pattern.mli | 2 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 1 |
5 files changed, 5 insertions, 3 deletions
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index fae83ee959..a95e4f2c5a 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Libnames +open Globnames (** The kinds of existential variable *) diff --git a/intf/glob_term.mli b/intf/glob_term.mli index d89b5840db..7ee0320f08 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -19,6 +19,7 @@ open Names open Sign open Term open Libnames +open Globnames open Decl_kinds open Misctypes diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 2485fd7a69..c8acc0496c 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -8,7 +8,7 @@ open Names open Term -open Libnames +open Globnames open Misctypes open Glob_term diff --git a/intf/pattern.mli b/intf/pattern.mli index 63d4ffa7a3..96f6ac9f68 100644 --- a/intf/pattern.mli +++ b/intf/pattern.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Libnames +open Globnames open Term open Misctypes diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index e70fc13086..895eca2d95 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -9,6 +9,7 @@ open Names open Constrexpr open Libnames +open Globnames open Nametab open Genredexpr open Genarg |