blob: cfe4d1b455900640fa4c5e2bc25a1b7f5b1f30e9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
(* Printers for the ocaml toplevel. *)
open System
open Pp
open Ast
open Names
open Sign
open Univ
open Proof_trees
open Environ
open Printer
open Refiner
open Tacmach
open Clenv
let pP s = pP (hOV 0 s)
let prast c = pP(print_ast c)
let prastpat c = pP(print_astpat c)
let prastpatl c = pP(print_astlpat c)
let ppterm0 = (fun x -> pP(term0 (gLOB nil_sign) x))
let pprawterm = (fun x -> pP(prrawterm x))
let pppattern = (fun x -> pP(prpattern x))
let pptype = (fun x -> pP(prtype x))
let prid id = pP [< 'sTR(string_of_id id) >]
let prconst (sp,j) =
pP [< 'sTR"#"; 'sTR(string_of_path sp);
'sTR"="; term0 (gLOB nil_sign) j.uj_val >]
let prvar ((id,a)) =
pP [< 'sTR"#" ; 'sTR(string_of_id id) ; 'sTR":" ;
term0 (gLOB nil_sign) a >]
let genprj f j = [< (f (gLOB nil_sign)j.uj_val);
'sTR " : ";
(f (gLOB nil_sign)j.uj_type);
'sTR " : ";
(f (gLOB nil_sign)j.uj_kind)>]
let prj j = pP (genprj term0 j)
let prsp sp = pP[< 'sTR(string_of_path sp) >]
let prgoal g = pP(prgl g)
let prsigmagoal g = pP(prgl (sig_it g))
let prgls gls = pP(pr_gls gls)
let prglls glls = pP(pr_glls glls)
let prctxt ctxt = pP(pr_ctxt ctxt)
let pproof p = pP(print_proof Evd.empty nil_sign p)
let prevd evd = pP(pr_decls evd)
let prevc evc = pP(pr_evc evc)
let prwc wc = pP(pr_evc wc)
let prclenv clenv = pP(pr_clenv clenv)
let p_uni u =
[< 'sTR(string_of_path u.u_sp) ;
'sTR "." ;
'iNT u.u_num >]
let print_uni u = (pP (p_uni u))
let pp_universes u = pP [< 'sTR"[" ; pr_universes u ; 'sTR"]" >]
|