diff options
| author | Hugo Herbelin | 2014-10-17 15:14:54 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-17 15:14:54 +0200 |
| commit | cfff8f8a32708ea0c8e72178424db0b40665fe37 (patch) | |
| tree | fe126ebb99be8e307df8a0a0f7837f51619a0eb8 /printing/printer.ml | |
| parent | bc8a5357889396f07d005a84bd3c50e9a25c1ddb (diff) | |
Experimental printing of the signature of open evars in Check.
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index cba33929b9..33bd5041e8 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -432,14 +432,15 @@ let pr_evar sigma (evk, evi) = hov 0 (pr_existential_key sigma evk ++ str " : " ++ pegl) (* Print an enumerated list of existential variables *) -let rec pr_evars_int sigma i = function +let rec pr_evars_int_hd head sigma i = function | [] -> mt () | (evk,evi)::rest -> - (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++ - pr_evar sigma (evk,evi))) ++ - (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int sigma (i+1) rest) + (hov 0 (head i ++ pr_evar sigma (evk,evi))) ++ + (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd head sigma (i+1) rest) -let pr_evars_int sigma i evs = pr_evars_int sigma i (Evar.Map.bindings evs) +let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ int i ++ str " =" ++ spc ()) sigma i (Evar.Map.bindings evs) + +let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs) let default_pr_subgoal n sigma = let rec prrec p = function |