diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
| commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
| tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /contrib/interface/showproof_ct.ml | |
| parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) | |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
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 |