From ed11f59ab67b0b6eb103d07386bf45ab2a8bede6 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 28 Mar 2000 16:30:04 +0000 Subject: 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 --- tactics/tactics.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'tactics/tactics.ml') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b8cfc3b45..0bc6860b2 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 -- cgit v1.2.3