diff options
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 50 |
1 files changed, 22 insertions, 28 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 0e3a49b0..b426f75d 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacmach.ml,v 1.61.2.1 2004/07/16 19:30:50 herbelin Exp $ *) +(* $Id: tacmach.ml 7682 2005-12-21 15:06:11Z herbelin $ *) open Util open Names @@ -14,11 +14,11 @@ open Nameops open Sign open Term open Termops -open Instantiate open Environ open Reductionops open Evd open Typing +open Redexpr open Tacred open Proof_trees open Proof_type @@ -32,7 +32,7 @@ let re_sig it gc = { it = it; sigma = gc } (* Operations for handling terms under a local typing context *) (**************************************************************) -type 'a sigma = 'a Proof_type.sigma;; +type 'a sigma = 'a Evd.sigma;; type validation = Proof_type.validation;; type tactic = Proof_type.tactic;; @@ -40,10 +40,10 @@ let unpackage = Refiner.unpackage let repackage = Refiner.repackage let apply_sig_tac = Refiner.apply_sig_tac -let sig_it = Refiner.sig_it -let project = Refiner.sig_sig -let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps -let pf_hyps gls = (sig_it gls).evar_hyps +let sig_it = Refiner.sig_it +let project = Refiner.project +let pf_env = Refiner.pf_env +let pf_hyps = Refiner.pf_hyps let pf_concl gls = (sig_it gls).evar_concl let pf_hyps_types gls = @@ -79,10 +79,6 @@ let pf_interp_constr gls c = let evc = project gls in Constrintern.interp_constr evc (pf_env gls) c -let pf_interp_openconstr gls c = - let evc = project gls in - Constrintern.interp_openconstr evc (pf_env gls) c - let pf_interp_type gls c = let evc = project gls in Constrintern.interp_type evc (pf_env gls) c @@ -91,12 +87,8 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id let pf_parse_const gls = compose (pf_global gls) id_of_string -let pf_execute gls = - let evc = project gls in - Typing.unsafe_machine (pf_env gls) evc - -let pf_reduction_of_redexp gls re c = - reduction_of_redexp re (pf_env gls) (project gls) c +let pf_reduction_of_red_expr gls re c = + (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c let pf_apply f gls = f (pf_env gls) (project gls) let pf_reduce = pf_apply @@ -119,7 +111,8 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls) -let pf_check_type gls c1 c2 = ignore (pf_type_of gls (mkCast (c1, c2))) +let pf_check_type gls c1 c2 = + ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2))) (************************************) (* Tactics handling a list of goals *) @@ -194,8 +187,8 @@ let internal_cut_rev_no_check id t gl = let refine_no_check c gl = refiner (Prim (Refine c)) gl -let convert_concl_no_check c gl = - refiner (Prim (Convert_concl c)) gl +let convert_concl_no_check c sty gl = + refiner (Prim (Convert_concl (c,sty))) gl let convert_hyp_no_check d gl = refiner (Prim (Convert_hyp d)) gl @@ -221,9 +214,11 @@ let mutual_cofix f others gl = with_check (refiner (Prim (Cofix (f,others)))) gl let rename_bound_var_goal gls = - let { evar_hyps = sign; evar_concl = cl } as gl = sig_it gls in - let ids = ids_of_named_context sign in - convert_concl_no_check (rename_bound_var (Global.env()) ids cl) gls + let { evar_hyps = sign; evar_concl = cl } = sig_it gls in + let ids = ids_of_named_context (named_context_of_val sign) in + convert_concl_no_check + (rename_bound_var (Global.env()) ids cl) DEFAULTcast gls + (* Versions with consistency checks *) @@ -233,7 +228,7 @@ let intro_replacing id = with_check (intro_replacing_no_check id) let internal_cut d t = with_check (internal_cut_no_check d t) let internal_cut_rev d t = with_check (internal_cut_rev_no_check d t) let refine c = with_check (refine_no_check c) -let convert_concl d = with_check (convert_concl_no_check d) +let convert_concl d sty = with_check (convert_concl_no_check d sty) let convert_hyp d = with_check (convert_hyp_no_check d) let thin l = with_check (thin_no_check l) let thin_body c = with_check (thin_body_no_check c) @@ -243,7 +238,6 @@ let rename_hyp id id' = with_check (rename_hyp_no_check id id') (* Pretty-printers *) open Pp -open Printer open Tacexpr open Rawterm @@ -252,9 +246,9 @@ let rec pr_list f = function | a::l1 -> (f a) ++ pr_list f l1 let pr_gls gls = - hov 0 (pr_decls (sig_sig gls) ++ fnl () ++ pr_seq (sig_it gls)) + hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) let pr_glls glls = - hov 0 (pr_decls (sig_sig glls) ++ fnl () ++ - prlist_with_sep pr_fnl pr_seq (sig_it glls)) + hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++ + prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) |