diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:26 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:26 +0000 |
| commit | 45038a0bfd5621153ba0dd4b6e06755fd15da1e3 (patch) | |
| tree | 8a30a206d390e1b7450889189596641e5026ee46 /pretyping/glob_term.ml | |
| parent | 3854ae16ffbaf56b90fbb85bcce3d92cd65ea6a6 (diff) | |
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/glob_term.ml')
| -rw-r--r-- | pretyping/glob_term.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 616a85444..fc1e1247f 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -15,7 +15,6 @@ open Sign open Term open Libnames open Nametab -open Evd (*i*) (* Untyped intermediate terms, after ASTs and before constr. *) @@ -67,7 +66,7 @@ type glob_constr = | GRec of loc * fix_kind * identifier array * glob_decl list array * glob_constr array * glob_constr array | GSort of loc * glob_sort - | GHole of (loc * hole_kind) + | GHole of (loc * Evar_kinds.t) | GCast of loc * glob_constr * glob_constr cast_type and glob_decl = name * binding_kind * glob_constr option * glob_constr |