aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-23 13:55:20 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-23 13:55:20 +0000
commit72e450d7ef0f01f2f92ce0089885f071d75cc74d (patch)
tree6fbc5c8005bfe158aa423c1b94f812f22450b20b /proofs
parent71df2a928fb9367a632a6869306626e3a5c7a971 (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.ml6
-rw-r--r--proofs/logic.ml24
-rw-r--r--proofs/tacmach.ml2
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 >]