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

8 files changed, 55 insertions, 43 deletions

diff --git a/dev/changements.txt b/dev/changements.txt
index f247062e37..6293de2960 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -80,6 +80,18 @@ Changements dans les fonctions :
           whd_betadeltat      -> whd_betaevar
           whd_betadeltatiota  -> whd_betaiotaevar
 
+        Astterm
+          constr_of_com_casted -> interp_casted_constr
+          constr_of_com_sort   -> interp_type
+          constr_of_com        -> interp_constr
+          rawconstr_of_com     -> interp_rawconstr
+          type_of_com          -> typed_type_of_com
+
+        Tacmach
+          pf_constr_of_com_sort -> pf_interp_type
+          pf_constr_of_com      -> pf_interp_constr
+
+
 Changements dans les inductifs
 ------------------------------
 Nouveaux types "constructor" et "inductive" dans Term
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
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 15e9069dda..97222bd359 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -331,7 +331,7 @@ let _ =
     "HintResolve"
     (function 
        | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_CONSTR c] ->
-	   let c1 = Astterm.constr_of_com Evd.empty (Global.env()) c in
+	   let c1 = Astterm.interp_constr Evd.empty (Global.env()) c in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function VARG_IDENTIFIER i -> string_of_id i
 		      	 | _ -> bad_vernac_args "HintResolve") l in
@@ -343,7 +343,7 @@ let _ =
     "HintImmediate"
     (function 
        | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_CONSTR c] ->
-	   let c1 = Astterm.constr_of_com Evd.empty (Global.env()) c in
+	   let c1 = Astterm.interp_constr Evd.empty (Global.env()) c in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function VARG_IDENTIFIER i -> string_of_id i
 			 | _ -> bad_vernac_args "HintImmediate") l in
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 2505f3b0a3..69c4104d9f 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -99,7 +99,7 @@ let decompose_or c gls =
 let dyn_decompose args gl = 
   match args with 
     | [Clause ids; Command c] -> 
-        decompose_these (pf_constr_of_com gl c) ids gl
+        decompose_these (pf_interp_constr gl c) ids gl
     | [Clause ids; Constr c]  -> 
         decompose_these c ids  gl
     | l -> bad_tactic_args "DecomposeThese" l gl
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b57be4b1a9..10bf2e53b6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -119,7 +119,7 @@ let replace c2 c1 gl =
 let dyn_replace args gl = 
   match args with 
     | [(Command c1);(Command c2)] -> 
-       	replace (pf_constr_of_com gl c1) (pf_constr_of_com gl c2) gl
+       	replace (pf_interp_constr gl c1) (pf_interp_constr gl c2) gl
     | [(Constr c1);(Constr c2)] -> 
        	replace c1 c2 gl
     | _ -> assert false
@@ -1441,7 +1441,7 @@ let rewrite_in lR com id gls =
      let _ = lookup_var id (pf_env gls) in () 
    with Not_found -> 
      errorlabstrm "rewrite_in" [< 'sTR"No such hypothesis : " ;print_id id >]);
-  let c = pf_constr_of_com gls com in
+  let c = pf_interp_constr gls com in
   let eqn = pf_type_of gls c in
   try
     let _ = find_eq_data_decompose eqn in
@@ -1470,7 +1470,7 @@ let substConcl_LR_tac =
     hide_tactic "SubstConcl_LR"
       (function 
 	 | [Command eqn] -> 
-	     (fun gls ->  substConcl_LR (pf_constr_of_com gls eqn)  gls)
+	     (fun gls ->  substConcl_LR (pf_interp_constr gls eqn)  gls)
 	 | _ -> assert false)
   in 
   fun eqn  -> gentac [Command eqn] 
@@ -1524,7 +1524,7 @@ let substConcl_RL_tac =
     hide_tactic "SubstConcl_RL"
       (function 
 	 | [Command eqn] -> 
-	     (fun gls ->  substConcl_RL (pf_constr_of_com gls eqn)  gls)
+	     (fun gls ->  substConcl_RL (pf_interp_constr gls eqn)  gls)
 	 | _ -> assert false)
   in 
   fun eqn  -> gentac [Command eqn] 
@@ -1619,7 +1619,7 @@ let _ =
      | [] -> lrl
      | (VARG_VARGLIST [VARG_CONSTR rule; VARG_STRING ort])::a 
 	 when ort="LR" or ort="RL" ->
-           lrules_arg (lrl@[(Astterm.constr_of_com Evd.empty
+           lrules_arg (lrl@[(Astterm.interp_constr Evd.empty
 			      (Global.env()) rule,ort="LR")]) a
      | _ -> bad_vernac_args "HintRewrite"
    and lbases_arg lbs = function
@@ -1710,7 +1710,7 @@ let explicit_hint_base gl = function
 	| lbs -> lbs
       end 
   | Explicit lbs -> 
-      List.map (fun (ast,b) -> (pf_constr_of_com gl ast, b)) lbs 
+      List.map (fun (ast,b) -> (pf_interp_constr gl ast, b)) lbs 
 
 (*AutoRewrite cannot be expressed with a combination of tacticals (due to the
   options). So, we make it in a primitive way*)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b8cfc3b45a..0bc6860b28 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -110,7 +110,7 @@ let dyn_mutual_fix argsl gl =
 	  | _  -> bad_tactic_args "mutual_fix" argsl
 	in
 	let (lid,ln,lar) = decomp [] [] [] lfix in
-	mutual_fix (id::lid) (n::ln) (List.map (pf_constr_of_com gl) lar) gl
+	mutual_fix (id::lid) (n::ln) (List.map (pf_interp_constr gl) lar) gl
     | l -> bad_tactic_args "mutual_fix" l 
 
 let mutual_cofix = Tacmach.mutual_cofix
@@ -133,7 +133,7 @@ let dyn_mutual_cofix argsl gl =
 	  |  _ -> bad_tactic_args "mutual_cofix" argsl
 	in
 	let (lid,lar) = decomp [] [] lcofix in
-        mutual_cofix (id::lid) (List.map (pf_constr_of_com gl) lar) gl
+        mutual_cofix (id::lid) (List.map (pf_interp_constr gl) lar) gl
    | l -> bad_tactic_args "mutual_cofix" l 
 
 
@@ -213,7 +213,7 @@ let pattern_option l = reduct_option (pattern_occs l)
 let dyn_change = function
   | [Command (com); Clause cl] ->
       (fun goal -> 
-         let c = Astterm.constr_of_com_sort (project goal) (pf_env goal) com in
+         let c = Astterm.interp_type (project goal) (pf_env goal) com in
          in_combinator (change_in_concl c) (change_in_hyp c) cl goal)
   | l -> bad_tactic_args "change" l
 
@@ -693,7 +693,7 @@ let letin_tac with_eq name c occ_ccl occhypl gl =
 
 let dyn_lettac args gl = match args with
   | [Identifier id; Command com; Letpatterns (o,l)] -> 
-      letin_tac true (Name id) (pf_constr_of_com gl com) o l gl
+      letin_tac true (Name id) (pf_interp_constr gl com) o l gl
   | [Identifier id; Constr c; Letpatterns (o,l)]    ->
       letin_tac true (Name id) c o l gl
   | l -> bad_tactic_args "letin" l
@@ -723,7 +723,7 @@ let dyn_exact cc gl = match cc with
   | [Command com] ->
       let evc = (project gl) in
       let concl = (pf_concl gl) in
-      let c = Astterm.constr_of_com_casted evc (pf_env gl) com concl in
+      let c = Astterm.interp_casted_constr evc (pf_env gl) com concl in
       refine c gl 
   | l -> bad_tactic_args "exact" l 
 
@@ -803,12 +803,12 @@ let dyn_new_hyp argsl gl =
     | [Integer n; Command com; Bindings binds]  ->
 	tactic_bind_list 
           (new_hyp (Some n) 
-             (pf_constr_of_com gl com)) 
+             (pf_interp_constr gl com)) 
           binds gl
     | [Command com; Bindings binds] ->  
 	tactic_bind_list 
           (new_hyp None 
-             (pf_constr_of_com gl com))
+             (pf_interp_constr gl com))
           binds gl
     | [Integer n; Constr c; Cbindings binds] ->  
         new_hyp (Some n) c binds gl
@@ -1502,7 +1502,7 @@ let instantiate_pf_com n com pfts =
     with Failure _ -> 
       error "not so many uninstantiated existential variables"
   in 
-  let c = Astterm.constr_of_com sigma evd.evar_env com in     
+  let c = Astterm.interp_constr sigma evd.evar_env com in     
   let wc' = w_Define sp c wc in
   let newgc = ts_mk (w_Underlying wc') in
   change_constraints_pftreestate newgc pfts
@@ -1522,7 +1522,7 @@ let contradiction_on_hyp id gl =
 
 (* Absurd *)
 let absurd c gls =
-  let falseterm = pf_constr_of_com_sort gls (Ast.nvar "False") in
+  let falseterm = pf_interp_type gls (Ast.nvar "False") in
   (tclTHENS
      (tclTHEN (elim_type falseterm) (cut c)) 
      ([(tclTHENS
@@ -1541,7 +1541,7 @@ let dyn_absurd = function
   | l             -> bad_tactic_args "absurd" l
 
 let contradiction gls = 
-  let falseterm = pf_constr_of_com_sort gls (Ast.nvar "False") in 
+  let falseterm = pf_interp_type gls (Ast.nvar "False") in 
   tclTHENLIST [ intros; elim_type falseterm; assumption ] gls
 
 let dyn_contradiction = function