diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-23 13:55:20 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-23 13:55:20 +0000 |
commit | 72e450d7ef0f01f2f92ce0089885f071d75cc74d (patch) | |
tree | 6fbc5c8005bfe158aa423c1b94f812f22450b20b /proofs | |
parent | 71df2a928fb9367a632a6869306626e3a5c7a971 (diff) |
print_id, print_sp -> pr_id, pr_sp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@923 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/clenv.ml | 6 | ||||
-rw-r--r-- | proofs/logic.ml | 24 | ||||
-rw-r--r-- | proofs/tacmach.ml | 2 |
3 files changed, 16 insertions, 16 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index daef42298..1332e0ecd 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -850,7 +850,7 @@ let clenv_lookup_name clenv id = match intmap_inv clenv.namenv id with | [] -> errorlabstrm "clenv_lookup_name" - [< 'sTR"No such bound variable "; print_id id >] + [< 'sTR"No such bound variable "; pr_id id >] | [n] -> n | _ -> @@ -869,7 +869,7 @@ let clenv_match_args s clause = | Dep s -> if List.mem_assoc b t then errorlabstrm "clenv_match_args" - [< 'sTR "The variable "; print_id s; + [< 'sTR "The variable "; pr_id s; 'sTR " occurs more than once in binding" >] else clenv_lookup_name clause s @@ -1027,7 +1027,7 @@ let pr_clenv clenv = let pr_name mv = try let id = Intmap.find mv clenv.namenv in - [< 'sTR"[" ; print_id id ; 'sTR"]" >] + [< 'sTR"[" ; pr_id id ; 'sTR"]" >] with Not_found -> [< >] in let pr_meta_binding = function diff --git a/proofs/logic.ml b/proofs/logic.ml index 0e7b5dc53..8021f336e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -548,36 +548,36 @@ open Printer let pr_prim_rule = function | {name=Intro;newids=[id]} -> - [< 'sTR"Intro " ; print_id id >] + [< 'sTR"Intro " ; pr_id id >] | {name=Intro_after;newids=[id]} -> - [< 'sTR"intro after " ; print_id id >] + [< 'sTR"intro after " ; pr_id id >] | {name=Intro_replacing;newids=[id]} -> - [< 'sTR"intro replacing " ; print_id id >] + [< 'sTR"intro replacing " ; pr_id id >] | {name=Fix;newids=[f];params=[Num(_,n)]} -> - [< 'sTR"Fix "; print_id f; 'sTR"/"; 'iNT n>] + [< 'sTR"Fix "; pr_id f; 'sTR"/"; 'iNT n>] | {name=Fix;newids=(f::lf);params=(Num(_,n))::ln;terms=lar} -> let rec print_mut = function (f::lf),((Num(_,n))::ln),(ar::lar) -> - [< print_id f; 'sTR"/"; 'iNT n; 'sTR" : "; prterm ar; + [< pr_id f; 'sTR"/"; 'iNT n; 'sTR" : "; prterm ar; print_mut (lf,ln,lar)>] | _ -> [<>] in - [< 'sTR"Fix "; print_id f; 'sTR"/"; 'iNT n; + [< 'sTR"Fix "; pr_id f; 'sTR"/"; 'iNT n; 'sTR" with "; print_mut (lf,ln,lar) >] | {name=Cofix;newids=[f];terms=[]} -> - [< 'sTR"Cofix "; print_id f >] + [< 'sTR"Cofix "; pr_id f >] | {name=Cofix;newids=(f::lf);terms=lar} -> let rec print_mut = function (f::lf),(ar::lar) -> - [< print_id f; 'sTR" : "; prterm ar; print_mut (lf,lar)>] + [< pr_id f; 'sTR" : "; prterm ar; print_mut (lf,lar)>] | _ -> [<>] in - [< 'sTR"Cofix "; print_id f; 'sTR" with "; print_mut (lf,lar) >] + [< 'sTR"Cofix "; pr_id f; 'sTR" with "; print_mut (lf,lar) >] | {name=Refine;terms=[c]} -> [< 'sTR(if occur_meta c then "Refine " else "Exact ") ; prterm c >] @@ -586,13 +586,13 @@ let pr_prim_rule = function [< 'sTR"Change " ; prterm c >] | {name=Convert_hyp;hypspecs=[id];terms=[c]} -> - [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; print_id id >] + [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; pr_id id >] | {name=Thin;hypspecs=ids} -> - [< 'sTR"Clear " ; prlist_with_sep pr_spc print_id ids >] + [< 'sTR"Clear " ; prlist_with_sep pr_spc pr_id ids >] | {name=Move withdep;hypspecs=[id1;id2]} -> [< 'sTR (if withdep then "Dependent " else ""); - 'sTR"Move " ; print_id id1; 'sTR " after "; print_id id2 >] + 'sTR"Move " ; pr_id id1; 'sTR " after "; pr_id id2 >] | _ -> anomaly "pr_prim_rule: Unrecognized primitive rule" diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 272fe6eae..575b18930 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -513,7 +513,7 @@ let pr_com sigma goal com = (Astterm.interp_constr sigma (Evarutil.evar_env goal) com)) let pr_one_binding sigma goal = function - | (Dep id,com) -> [< print_id id ; 'sTR":=" ; pr_com sigma goal com >] + | (Dep id,com) -> [< pr_id id ; 'sTR":=" ; pr_com sigma goal com >] | (NoDep n,com) -> [< 'iNT n ; 'sTR":=" ; pr_com sigma goal com >] | (Com,com) -> [< pr_com sigma goal com >] |