diff options
author | 2013-11-25 17:22:26 +0100 | |
---|---|---|
committer | 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 e4ac9426b..0e74a81c4 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 | _ -> |