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 /parsing/g_constr.ml4 | |
| 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 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index abd1607d6..06d922a7c 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -34,12 +34,12 @@ let mk_cast = function let binders_of_names l = List.map (fun (loc, na) -> LocalRawAssum ([loc, na], Default Explicit, - CHole (loc, Some (Evd.BinderType na)))) l + CHole (loc, Some (Evar_kinds.BinderType na)))) l let binders_of_lidents l = List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Glob_term.Explicit, - CHole (loc, Some (Evd.BinderType (Name id))))) l + CHole (loc, Some (Evar_kinds.BinderType (Name id))))) l let mk_fixb (id,bl,ann,body,(loc,tyc)) = let ty = match tyc with |