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

4 files changed, 19 insertions, 19 deletions

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