diff options
| author | Yves Bertot | 2018-05-30 17:36:29 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-30 17:38:13 +0200 |
| commit | 2d6a9619f8cf87afff32e3e85da88a86b327bade (patch) | |
| tree | 95452180b7dd523c0b90eab48d5488f18394460a /tuto1/src | |
| parent | 46f908ab5a03998fa96c1a599b44e6e2b3fd9a10 (diff) | |
| parent | 470f48c60124aaad7d5825959630453108c99f1b (diff) | |
remove warnings and merge printing function for econstr terms
Diffstat (limited to 'tuto1/src')
| -rw-r--r-- | tuto1/src/g_tuto1.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4 index bd53053ec7..b152583824 100644 --- a/tuto1/src/g_tuto1.ml4 +++ b/tuto1/src/g_tuto1.ml4 @@ -91,7 +91,7 @@ VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY let (_, ctx) = v in let evd = Evd.from_ctx ctx in Feedback.msg_notice - (Termops.print_constr_env (Global.env()) evd + (Printer.pr_econstr_env (Global.env()) evd (Simple_check.simple_check1 v)) ] END @@ -101,7 +101,7 @@ VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY (Evd.from_env (Global.env())) e in let evd, ty = Simple_check.simple_check2 v in Feedback.msg_notice - (Termops.print_constr_env (Global.env()) evd ty) ] + (Printer.pr_econstr_env (Global.env()) evd ty) ] END VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY @@ -111,7 +111,7 @@ VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY let (a, ctx) = v in let evd = Evd.from_ctx ctx in Feedback.msg_notice - (Termops.print_constr_env (Global.env()) evd + (Printer.pr_econstr_env (Global.env()) evd (Simple_check.simple_check3 v)) ] END @@ -125,7 +125,7 @@ VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY [ let env = Global.env() in let evd = Evd.from_env env in Feedback.msg_notice - (Termops.print_constr_env env evd + (Printer.pr_econstr_env env evd (EConstr.of_constr (Simple_print.simple_body_access (Nametab.global r)))) ] END |