diff options
| author | Arnaud Spiwack | 2014-09-03 18:16:21 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-04 10:25:55 +0200 |
| commit | a93104d5462894d5d0651aa2e04e12c311eb5897 (patch) | |
| tree | 8619451aa37d699fc012f0e5f6509560d9c46726 /printing | |
| parent | 06e6a7b5a0d15f493a3f94fad905af2c44be9c09 (diff) | |
Remove [Infer] option of records.
Dead code formerly used by the now defunct [autoinstances].
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 514017d454..5ef7eb710e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -623,7 +623,7 @@ let rec pr_vernac = function hov 2 (pr_assumption_token (n > 1) stre ++ spc() ++ pr_ne_params_list pr_lconstr_expr l) - | VernacInductive (p,f,i,l) -> + | VernacInductive (p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ @@ -641,7 +641,6 @@ let rec pr_vernac = function let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) = hov 0 ( str key ++ spc() ++ - (if i then str"Infer " else str"") ++ (if coe then str"> " else str"") ++ pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ |