diff options
| author | letouzey | 2012-10-02 15:57:23 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-02 15:57:23 +0000 |
| commit | d863709ee2fcb920a256f1dfb96cbcbf25cdac80 (patch) | |
| tree | 00434fd94e72d71c92982c8a937de267004a3060 | |
| parent | 62aa6ad82ed5d986da1b979296a82fb46e64b55d (diff) | |
avoid referring to Term in constrexpr.mli and glob_term.mli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15842 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | intf/constrexpr.mli | 2 | ||||
| -rw-r--r-- | intf/glob_term.mli | 4 | ||||
| -rw-r--r-- | intf/misctypes.mli | 13 | ||||
| -rw-r--r-- | intf/notation_term.mli | 1 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 2 |
5 files changed, 13 insertions, 9 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 3acfc3d44c..3225284796 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -7,10 +7,8 @@ (************************************************************************) open Loc -open Pp open Names open Libnames -open Term open Misctypes open Decl_kinds diff --git a/intf/glob_term.mli b/intf/glob_term.mli index 560662423e..8e7b012b0a 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -14,11 +14,7 @@ and notations are done, but coercions, inference of implicit arguments and pattern-matching compilation are not. *) -open Pp open Names -open Sign -open Term -open Libnames open Globnames open Decl_kinds open Misctypes diff --git a/intf/misctypes.mli b/intf/misctypes.mli index e7f8b1b2ac..97b4b45fe0 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -40,6 +40,19 @@ type 'id move_location = type sort_info = string option type glob_sort = GProp | GSet | GType of sort_info +(** A synonym of [int], also defined in Term *) + +type existential_key = int + +(** Case style, shared with Term *) + +type case_style = Term.case_style = + | LetStyle + | IfStyle + | LetPatternStyle + | MatchStyle + | RegularStyle (** infer printing form from number of constructor *) + (** Casts *) type 'a cast_type = diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 4d90db7f3f..d7bd73588e 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open Globnames open Misctypes open Glob_term diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 669d60ac28..64a8c54eaa 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp -open Term open Names open Libnames open Constrexpr |