diff options
| author | Matthieu Sozeau | 2013-11-25 17:22:26 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:56 +0200 |
| commit | cd11c5d2ff5d91603a6043a667e5918e99ef303a (patch) | |
| tree | 173990017678e28e3a4ff4f582a189d596cd1213 /interp/constrextern.ml | |
| parent | 6f54f7411f6e42298e833215fde9f38dd899e5dc (diff) | |
Fix printing of projections with implicits.
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e4ac9426b3..0e74a81c47 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -672,7 +672,10 @@ let rec extern inctx scopes vars r = let args = extern_args (extern true) (snd scopes) vars (c :: args) subscopes in - extern_app loc inctx [] (Some ref, extern_reference loc vars ref) + extern_app loc inctx + (projection_implicits (Global.env ()) p + (select_stronger_impargs (implicits_of_global ref))) + (Some ref, extern_reference loc vars ref) None args | _ -> |