Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf_,}interp_constr*

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@357 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 24 insertions, 24 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 137486bb48..a8b8ba97ec 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -246,8 +246,8 @@ let start_proof_with_type na str env concl =
 let start_proof na str concl_com =
   let sigma = Evd.empty in
   let env = Global.env() in
-  let concl = type_of_com env concl_com in
-  start_proof_with_type na str env concl.body
+  let concl = interp_type sigma env concl_com in
+  start_proof_with_type na str env concl
 
 let start_proof_constr na str concl =
   let sigma = Evd.empty in
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 5a7c105947..7209361109 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -69,13 +69,13 @@ let hnf_type_of gls =
 let pf_check_type gls c1 c2 =
   let casted = mkCast c1 c2 in pf_type_of gls casted
 
-let pf_constr_of_com gls c =
+let pf_interp_constr gls c =
   let evc = project gls in 
-  Astterm.constr_of_com evc (sig_it gls).evar_env c
+  Astterm.interp_constr evc (sig_it gls).evar_env c
 
-let pf_constr_of_com_sort gls c =
+let pf_interp_type gls c =
   let evc = project gls in 
-  Astterm.constr_of_com_sort evc (sig_it gls).evar_env c
+  Astterm.interp_type evc (sig_it gls).evar_env c
 
 let pf_global gls id = Declare.construct_reference (sig_it gls).evar_env CCI id
 let pf_parse_const gls = compose (pf_global gls) id_of_string
@@ -282,26 +282,26 @@ let overwriting_tactic = Refiner.overwriting_add_tactic
 
 type ('a,'b) parse_combinator = ('a -> tactic) -> ('b -> tactic)
 
-let tactic_com tac t x = tac (pf_constr_of_com x t) x
+let tactic_com tac t x = tac (pf_interp_constr x t) x
       
-let tactic_com_sort tac t x = tac (pf_constr_of_com_sort x t) x
+let tactic_com_sort tac t x = tac (pf_interp_type x t) x
       
 let tactic_com_list tac tl x =
-  let translate = pf_constr_of_com x in 
+  let translate = pf_interp_constr x in 
   tac (List.map translate tl) x
     
 let tactic_bind_list tac tl x =
-  let translate = pf_constr_of_com x in 
+  let translate = pf_interp_constr x in 
   tac (List.map (fun (b,c)->(b,translate c)) tl) x
 
 let tactic_com_bind_list tac (c,tl) x =
-  let translate = pf_constr_of_com x in 
+  let translate = pf_interp_constr x in 
   tac (translate c,List.map (fun (b,c')->(b,translate c')) tl) x
 
 let tactic_com_bind_list_list tac args gl =
   let translate (c,tl) = 
-    (pf_constr_of_com gl c,
-     List.map (fun (b,c')->(b,pf_constr_of_com gl c')) tl) in 
+    (pf_interp_constr gl c,
+     List.map (fun (b,c')->(b,pf_interp_constr gl c')) tl) in 
   tac (List.map translate args) gl
 
 
@@ -319,31 +319,31 @@ let overwrite_hidden_tactic s tac  =
   (fun args -> vernac_tactic(s,args))
 
 let tactic_com = 
-  fun tac t x -> tac (pf_constr_of_com x t) x
+  fun tac t x -> tac (pf_interp_constr x t) x
       
 let tactic_com_sort = 
-  fun tac t x -> tac (pf_constr_of_com_sort x t) x
+  fun tac t x -> tac (pf_interp_type x t) x
       
 let tactic_com_list =    
   fun tac tl x -> 
-    let translate = pf_constr_of_com x in 
+    let translate = pf_interp_constr x in 
     tac (List.map translate tl) x
 
 let tactic_bind_list =
   fun tac tl x -> 
-    let translate = pf_constr_of_com x in 
+    let translate = pf_interp_constr x in 
     tac (List.map (fun (b,c)->(b,translate c)) tl) x
 
 let tactic_com_bind_list =
   fun tac (c,tl) x -> 
-    let translate = pf_constr_of_com x in 
+    let translate = pf_interp_constr x in 
     tac (translate c,List.map (fun (b,c')->(b,translate c')) tl) x
 
 let tactic_com_bind_list_list =
   fun tac args gl -> 
     let translate (c,tl) = 
-      (pf_constr_of_com gl c,
-       List.map (fun (b,c')->(b,pf_constr_of_com gl c')) tl)
+      (pf_interp_constr gl c,
+       List.map (fun (b,c')->(b,pf_interp_constr gl c')) tl)
     in 
     tac (List.map translate args) gl
 
@@ -374,7 +374,7 @@ let overwrite_hidden_constr_comarg_tactic s tac =
   let tacfun = function 
     | [Constr c] -> tac c
     | [Command com] -> 
-        (fun gls -> tac (pf_constr_of_com gls com) gls)
+        (fun gls -> tac (pf_interp_constr gls com) gls)
     | _ -> 
 	anomaly 
 	  "overwrite_hidden_constr_comarg_tactic : neither CONSTR nor COMMAND"
@@ -475,7 +475,7 @@ open Printer
 let pr_com sigma goal com =
   prterm (rename_bound_var 
             (ids_of_sign (var_context goal.evar_env)) 
-            (Astterm.constr_of_com sigma goal.evar_env com))
+            (Astterm.interp_constr sigma goal.evar_env com))
 
 let pr_one_binding sigma goal = function
   | (Dep id,com)  -> [< print_id id ; 'sTR":=" ; pr_com sigma goal com >]
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index dff9fe0b2e..9a946e7620 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -41,8 +41,8 @@ val pf_check_type         : goal sigma -> constr -> constr -> constr
 val pf_execute            : goal sigma -> constr -> unsafe_judgment
 val hnf_type_of           : goal sigma -> constr -> constr
 
-val pf_constr_of_com      : goal sigma -> Coqast.t -> constr
-val pf_constr_of_com_sort : goal sigma -> Coqast.t -> constr
+val pf_interp_constr      : goal sigma -> Coqast.t -> constr
+val pf_interp_type : goal sigma -> Coqast.t -> constr
 
 val pf_get_hyp             : goal sigma -> identifier -> constr