diff options
| author | Hugo Herbelin | 2014-09-16 09:41:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-16 09:48:36 +0200 |
| commit | 2e1b90f8b0a585c4a4dd65ffd4b297442cc66cc8 (patch) | |
| tree | a94d74fee3b2778dda692fcbe80525c3d77c3efe /interp | |
| parent | 62a552b508b747b6cdf4bd818233f001ae4ce555 (diff) | |
More on printing references applied to implicit arguments.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f71cf5a65b..2e6ab43544 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -460,7 +460,7 @@ let is_projection primprojapp nargs cf = | _ -> None, None -let is_hole = function CHole _ -> true | _ -> false +let is_hole = function CHole _ | CEvar _ -> true | _ -> false let is_significant_implicit a = not (is_hole a) @@ -547,7 +547,7 @@ let explicitize loc inctx impl (cf,primprojapp,f) args = CAppExpl (loc, (ip, f', us), args) let is_start_implicit = function - | imp :: _ -> is_status_implicit imp (* && maximal_insertion_of imp *) + | imp :: _ -> is_status_implicit imp && maximal_insertion_of imp | [] -> false let extern_global loc impl f us = |