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 | |
| parent | 6f54f7411f6e42298e833215fde9f38dd899e5dc (diff) | |
Fix printing of projections with implicits.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 5 | ||||
| -rw-r--r-- | interp/constrintern.ml | 9 |
2 files changed, 11 insertions, 3 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 | _ -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0905ad1d6b..d8cf9fd161 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -691,13 +691,18 @@ let is_projection_ref = function | ConstRef r -> if Environ.is_projection r (Global.env ()) then Some r else None | _ -> None +let proj_impls r impls = + let env = Global.env () in + let f (x, l) = x, projection_implicits env r l in + List.map f impls + let find_appl_head_data c = match c with | GRef (loc,ref,_) as x -> let impls = implicits_of_global ref in let isproj, impls = match is_projection_ref ref with - | Some r -> true, List.map (projection_implicits (Global.env ()) r) impls + | Some r -> true, proj_impls r impls | None -> false, impls in let scopes = find_arguments_scope ref in @@ -708,7 +713,7 @@ let find_appl_head_data c = let impls = implicits_of_global ref in let isproj, impls = match is_projection_ref ref with - | Some r -> true, List.map (projection_implicits (Global.env ()) r) impls + | Some r -> true, proj_impls r impls | None -> false, impls in x, isproj, List.map (drop_first_implicits n) impls, |