diff options
| -rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/logic.mli | 1 | ||||
| -rw-r--r-- | proofs/refiner.ml | 5 | ||||
| -rw-r--r-- | proofs/refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 51 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 40 | ||||
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 4 |
9 files changed, 71 insertions, 38 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 09879d585..3f3b66dee 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -32,8 +32,6 @@ let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it type w_tactic = named_context sigma -> named_context sigma -let local_Constraints gs = refiner Change_evars gs - let startWalk gls = let evc = project_with_focus gls in (evc, diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index b0dd5e4f4..55c7282c2 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -30,8 +30,6 @@ val rc_of_glsigma : goal sigma -> wc dependent goal *) type w_tactic = wc -> wc -val local_Constraints : tactic - val startWalk : goal sigma -> wc * (wc -> tactic) val extract_decl : evar -> w_tactic diff --git a/proofs/logic.mli b/proofs/logic.mli index dfe40228f..7d449c71d 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -21,6 +21,7 @@ open Proof_type argument; works by side-effect *) val without_check : tactic -> tactic +val with_check : tactic -> tactic (* [without_check] respectively means:\\ [Intro]: no check that the name does not exist\\ diff --git a/proofs/refiner.ml b/proofs/refiner.ml index a6edd9a3a..41043eac0 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -202,7 +202,10 @@ let refiner = function assert (List.length spfl = 1); List.hd spfl)))) -let norm_evar_tac gl = refiner Change_evars gl + +let local_Constraints gl = refiner Change_evars gl + +let norm_evar_tac = local_Constraints (* let vernac_tactic (s,args) = diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 34f8fb665..2fa0b178c 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -50,6 +50,8 @@ val frontier : transformation_tactic val list_pf : proof_tree -> goal list val unTAC : tactic -> goal sigma -> proof_tree sigma +val local_Constraints : tactic + (*s Tacticals. *) (* [tclIDTAC] is the identity tactic *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index c140aec93..6b53f6c98 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -168,52 +168,67 @@ let change_constraints_pftreestate = change_constraints_pftreestate let refiner = refiner (* This does not check that the variable name is not here *) -let unsafe_introduction id = - without_check (refiner (Prim (Intro id))) +let introduction_no_check id = + refiner (Prim (Intro id)) -let introduction id gl = - refiner (Prim (Intro id)) gl - -let intro_replacing whereid gl = +(* This does not check that the dependencies are correct *) +let intro_replacing_no_check whereid gl = refiner (Prim (Intro_replacing whereid)) gl -let internal_cut id t gl = +let internal_cut_no_check id t gl = refiner (Prim (Cut (true,id,t))) gl -let internal_cut_rev id t gl = +let internal_cut_rev_no_check id t gl = refiner (Prim (Cut (false,id,t))) gl -let refine c gl = +let refine_no_check c gl = refiner (Prim (Refine c)) gl -let convert_concl c gl = +let convert_concl_no_check c gl = refiner (Prim (Convert_concl c)) gl -let convert_hyp d gl = +let convert_hyp_no_check d gl = refiner (Prim (Convert_hyp d)) gl -let thin ids gl = +(* This does not check dependencies *) +let thin_no_check ids gl = if ids = [] then tclIDTAC gl else refiner (Prim (Thin ids)) gl -let thin_body ids gl = +(* This does not check dependencies *) +let thin_body_no_check ids gl = if ids = [] then tclIDTAC gl else refiner (Prim (ThinBody ids)) gl -let move_hyp with_dep id1 id2 gl = +let move_hyp_no_check with_dep id1 id2 gl = refiner (Prim (Move (with_dep,id1,id2))) gl -let rename_hyp id1 id2 gl = +let rename_hyp_no_check id1 id2 gl = refiner (Prim (Rename (id1,id2))) gl let mutual_fix f n others gl = - refiner (Prim (FixRule (f,n,others))) gl + with_check (refiner (Prim (FixRule (f,n,others)))) gl let mutual_cofix f others gl = - refiner (Prim (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 (rename_bound_var (Global.env()) ids cl) gls + convert_concl_no_check (rename_bound_var (Global.env()) ids cl) gls + + +(* Versions with consistency checks *) + +let introduction id = with_check (introduction_no_check id) +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_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) +let move_hyp b id id' = with_check (move_hyp_no_check b id id') +let rename_hyp id id' = with_check (rename_hyp_no_check id id') (* Pretty-printers *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index ec849662f..5ea42b380 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -122,23 +122,39 @@ val vernac_tactic : string * tactic_arg list -> tactic *) (*s The most primitive tactics. *) -val refiner : rule -> tactic -val introduction : identifier -> tactic -val intro_replacing : identifier -> tactic -val internal_cut : identifier -> types -> tactic -val internal_cut_rev : identifier -> types -> tactic -val refine : constr -> tactic -val convert_concl : types -> tactic -val convert_hyp : named_declaration -> tactic -val thin : identifier list -> tactic -val thin_body : identifier list -> tactic -val move_hyp : bool -> identifier -> identifier -> tactic -val rename_hyp : identifier -> identifier -> tactic +val refiner : rule -> tactic +val introduction_no_check : identifier -> tactic +val intro_replacing_no_check : identifier -> tactic +val internal_cut_no_check : identifier -> types -> tactic +val internal_cut_rev_no_check : identifier -> types -> tactic +val refine_no_check : constr -> tactic +val convert_concl_no_check : types -> tactic +val convert_hyp_no_check : named_declaration -> tactic +val thin_no_check : identifier list -> tactic +val thin_body_no_check : identifier list -> tactic +val move_hyp_no_check : bool -> identifier -> identifier -> tactic +val rename_hyp_no_check : identifier -> identifier -> tactic val mutual_fix : identifier -> int -> (identifier * int * constr) list -> tactic val mutual_cofix : identifier -> (identifier * constr) list -> tactic val rename_bound_var_goal : tactic +(*s The most primitive tactics with consistency and type checking *) + +val introduction : identifier -> tactic +val intro_replacing : identifier -> tactic +val internal_cut : identifier -> types -> tactic +val internal_cut_rev : identifier -> types -> tactic +val refine : constr -> tactic +val convert_concl : constr -> tactic +val convert_hyp : named_declaration -> tactic +val thin : identifier list -> tactic +val convert_concl : types -> tactic +val convert_hyp : named_declaration -> tactic +val thin : identifier list -> tactic +val thin_body : identifier list -> tactic +val move_hyp : bool -> identifier -> identifier -> tactic +val rename_hyp : identifier -> identifier -> tactic (*s Tactics handling a list of goals. *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 9c153b15e..684329419 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -650,7 +650,7 @@ and my_find_search db_list local_db hdc concl = match t with | Res_pf (term,cl) -> unify_resolve (term,cl) | ERes_pf (_,c) -> (fun gl -> error "eres_pf") - | Give_exact c -> exact_no_check c + | Give_exact c -> exact_check c | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_resolve (term,cl)) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 896218c80..5667796fe 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -31,8 +31,8 @@ open Rawterm let e_give_exact c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in if occur_existential t1 or occur_existential t2 then - tclTHEN (unify t1) (exact_no_check c) gl - else exact_no_check c gl + tclTHEN (unify t1) (exact_check c) gl + else exact_check c gl let assumption id = e_give_exact (mkVar id) |