diff options
Diffstat (limited to 'contrib/interface/showproof_ct.ml')
| -rw-r--r-- | contrib/interface/showproof_ct.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/contrib/interface/showproof_ct.ml b/contrib/interface/showproof_ct.ml index ee901c5e..dd7f455d 100644 --- a/contrib/interface/showproof_ct.ml +++ b/contrib/interface/showproof_ct.ml @@ -3,7 +3,6 @@ Vers Ctcoq *) -open Esyntax open Metasyntax open Printer open Pp @@ -131,12 +130,12 @@ let rec sp_print x = | "\n" -> fnl () | "Retour chariot pour Show proof" -> fnl () |_ -> str s) - | CT_text_formula f -> prterm (Hashtbl.find ct_FORMULA_constr f) + | CT_text_formula f -> pr_lconstr (Hashtbl.find ct_FORMULA_constr f) | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "to_prove"); CT_text_path (CT_signed_int_list p); CT_coerce_ID_to_TEXT (CT_ident "goal"); g] -> - let p=(List.map (fun y -> match y with + let _p=(List.map (fun y -> match y with (CT_coerce_INT_to_SIGNED_INT (CT_int x)) -> x | _ -> raise (Failure "sp_print")) p) in @@ -149,7 +148,7 @@ let rec sp_print x = CT_text_path (CT_signed_int_list p); CT_coerce_ID_to_TEXT (CT_ident hyp); g] -> - let p=(List.map (fun y -> match y with + let _p=(List.map (fun y -> match y with (CT_coerce_INT_to_SIGNED_INT (CT_int x)) -> x | _ -> raise (Failure "sp_print")) p) in @@ -159,7 +158,7 @@ let rec sp_print x = CT_text_path (CT_signed_int_list p); CT_coerce_ID_to_TEXT (CT_ident hyp); g] -> - let p=(List.map (fun y -> match y with + let _p=(List.map (fun y -> match y with (CT_coerce_INT_to_SIGNED_INT (CT_int x)) -> x | _ -> raise (Failure "sp_print")) p) in |