diff options
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index ec1405f76a..784c977dd8 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -87,12 +87,12 @@ let pr_sort = function | RProp Term.Pos -> str "Set" | RType u -> str "Type" ++ pr_opt pr_universe u -let pr_explicitation = function - | None -> mt () - | Some n -> str "@" ++ int n ++ str ":=" - let pr_expl_args pr (a,expl) = - pr_explicitation expl ++ pr (lapp,L) a + match expl with + | None -> pr (lapp,L) a + | Some (_,ExplByPos n) -> str "@" ++ int n ++ str ":=" ++ pr (lapp,L) a + | Some (_,ExplByName id) -> + str "(" ++ pr_id id ++ str ":=" ++ pr (lapp,L) a ++ str ")" let pr_opt_type pr = function | CHole _ -> mt () |