diff options
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 25 |
1 files changed, 14 insertions, 11 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 229930142e..78733784a7 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -84,7 +84,8 @@ let tag_var = tag Tag.variable | Any -> true let prec_of_prim_token = function - | Numeral (_,b) -> if b then lposint else lnegint + | Numeral (SPlus,_) -> lposint + | Numeral (SMinus,_) -> lnegint | String _ -> latom let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps = @@ -234,7 +235,8 @@ let tag_var = tag Tag.variable | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t let pr_prim_token = function - | Numeral (n,s) -> str (if s then n else "-"^n) + | Numeral (SPlus,n) -> str (NumTok.to_string n) + | Numeral (SMinus,n) -> str ("-"^NumTok.to_string n) | String s -> qs s let pr_evar pr id l = @@ -397,12 +399,12 @@ let tag_var = tag Tag.variable pr_opt_type_spc pr t ++ str " :=" ++ pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c - let pr_guard_annot pr_aux bl (n,ro) = - match n with + let pr_guard_annot pr_aux bl ro = + match ro with | None -> mt () - | Some {loc; v = id} -> - match (ro : Constrexpr.recursion_order_expr) with - | CStructRec -> + | Some {loc; v = ro} -> + match ro with + | CStructRec { v = id } -> let names_of_binder = function | CLocalAssum (nal,_,_) -> nal | CLocalDef (_,_,_) -> [] @@ -411,10 +413,11 @@ let tag_var = tag Tag.variable if List.length ids > 1 then spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" else mt() - | CWfRec c -> - spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_id id ++ str"}" - | CMeasureRec (m,r) -> - spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ spc() ++ pr_id id++ + | CWfRec (id,c) -> + spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_lident id ++ str"}" + | CMeasureRec (id,m,r) -> + spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ + match id with None -> mt() | Some id -> spc () ++ pr_lident id ++ (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}" let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) = |