From 0945a87fbb5e07a47f018fe5ba518461c2280561 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 14 Jan 2019 14:48:49 +0100 Subject: [PATCH] fix(library/init/lean/elaborator): to_pexpr: explicitness modifiers --- library/init/lean/elaborator.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index 8546846de7..db499ebbef 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -254,8 +254,8 @@ def to_pexpr : syntax → elaborator_m expr | @explicit := do let v := view explicit stx, let ann := match v.mod with - | explicit_modifier.view.explicit _ := `explicit - | explicit_modifier.view.partial_explicit _ := `partial_explicit, + | explicit_modifier.view.explicit _ := `@ + | explicit_modifier.view.partial_explicit _ := `@@, expr.mk_annotation ann <$> to_pexpr (review ident_univs v.id) | @number := do let v := view number stx,