diff options
| author | Emilio Jesus Gallego Arias | 2018-09-18 20:11:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-18 20:11:41 +0200 |
| commit | 65a5d6ce9a7a3c35bd426b7e5dcc88cb35f498b1 (patch) | |
| tree | 42cd98c5603025131c388ffd454093b4c1563089 /printing/printer.ml | |
| parent | 15649c16bc4e20ef2c2b1b0ac645f83ee03c3589 (diff) | |
[api] Deprecate two forgotten print functions that use global state.
Removal of the global state API is scheduled for 8.10, thus it is
crucial we ship this in 8.9.
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 5b3ead181f..f0ea6532de 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -930,8 +930,8 @@ let pr_assumptionset env sigma s = let mp,_,lab = Constant.repr3 kn in str (ModPath.to_string mp) ++ str "." ++ Label.print lab in - let safe_pr_ltype typ = - try str " : " ++ pr_ltype typ + let safe_pr_ltype env sigma typ = + try str " : " ++ pr_ltype_env env sigma typ with e when CErrors.noncritical e -> mt () in let safe_pr_ltype_relctx (rctx, typ) = @@ -942,7 +942,7 @@ let pr_assumptionset env sigma s = let pr_axiom env ax typ = match ax with | Constant kn -> - safe_pr_constant env kn ++ safe_pr_ltype typ + safe_pr_constant env kn ++ safe_pr_ltype env sigma typ | Positive m -> hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") | Guarded kn -> @@ -952,7 +952,7 @@ let pr_assumptionset env sigma s = let (v, a, o, tr) = accu in match t with | Variable id -> - let var = pr_id id ++ str " : " ++ pr_ltype typ in + let var = pr_id id ++ str " : " ++ pr_ltype_env env sigma typ in (var :: v, a, o, tr) | Axiom (axiom, []) -> let ax = pr_axiom env axiom typ in @@ -966,10 +966,10 @@ let pr_assumptionset env sigma s = l in (v, ax :: a, o, tr) | Opaque kn -> - let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in + let opq = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in (v, a, opq :: o, tr) | Transparent kn -> - let tran = safe_pr_constant env kn ++ safe_pr_ltype typ in + let tran = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in (v, a, o, tran :: tr) in let (vars, axioms, opaque, trans) = |