summaryrefslogtreecommitdiff
path: root/tactics/decl_proof_instr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/decl_proof_instr.ml')
-rw-r--r--tactics/decl_proof_instr.ml67
1 files changed, 35 insertions, 32 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 895b97fe..5356868a 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: decl_proof_instr.ml 11072 2008-06-08 16:13:37Z herbelin $ *)
+(* $Id: decl_proof_instr.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Util
open Pp
@@ -106,6 +106,9 @@ let clean_tmp gls =
in
clean_all (tmp_ids gls) gls
+let assert_postpone id t =
+ assert_as true (dummy_loc, Genarg.IntroIdentifier id) t
+
(* start a proof *)
let start_proof_tac gls=
@@ -188,7 +191,7 @@ let close_tactic_mode pts =
let pts1=
try goto_current_focus pts
with Not_found ->
- error "\"return\" cannot be used outside of Declarative Proof Mode" in
+ error "\"return\" cannot be used outside of Declarative Proof Mode." in
let pts2 = daimon_subtree pts1 in
let pts3 = mark_as_done pts2 in
goto_current_focus pts3
@@ -207,18 +210,18 @@ let close_block bt pts =
B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
daimon_subtree (goto_current_focus pts)
| _, Claim::_ ->
- error "\"end claim\" expected"
+ error "\"end claim\" expected."
| _, Focus_claim::_ ->
- error "\"end focus\" expected"
+ error "\"end focus\" expected."
| _, [] ->
- error "\"end proof\" expected"
+ error "\"end proof\" expected."
| _, (Per (et,_,_,_)::_|Suppose_case::Per (et,_,_,_)::_) ->
begin
match et with
- ET_Case_analysis -> error "\"end cases\" expected"
- | ET_Induction -> error "\"end induction\" expected"
+ ET_Case_analysis -> error "\"end cases\" expected."
+ | ET_Induction -> error "\"end induction\" expected."
end
- | _,_ -> anomaly "lonely suppose on stack"
+ | _,_ -> anomaly "Lonely suppose on stack."
(* utility for suppose / suppose it is *)
@@ -284,10 +287,10 @@ let justification tac gls=
(tclSOLVE [tclTHEN tac assumption])
(fun gls ->
if get_strictness () then
- error "insufficient justification"
+ error "Insufficient justification."
else
begin
- msg_warning (str "insufficient justification");
+ msg_warning (str "Insufficient justification.");
daimon_tac gls
end) gls
@@ -475,7 +478,7 @@ let thus_tac c ctyp submetas gls =
try
find_subsubgoal c ctyp 0 submetas gls
with Not_found ->
- error "I could not relate this statement to the thesis" in
+ error "I could not relate this statement to the thesis." in
if list = [] then
exact_check proof gls
else
@@ -490,7 +493,7 @@ let anon_id_base = id_of_string "__"
let mk_stat_or_thesis info gls = function
This c -> c
| Thesis (For _ ) ->
- error "\"thesis for ...\" is not applicable here"
+ error "\"thesis for ...\" is not applicable here."
| Thesis Plain -> pf_concl gls
let just_tac _then cut info gls0 =
@@ -524,7 +527,7 @@ let instr_cut mkstat _thus _then cut gls0 =
if _thus then
thus_tac (mkVar c_id) c_stat [] gls
else tclIDTAC gls in
- tclTHENS (internal_cut c_id c_stat)
+ tclTHENS (assert_postpone c_id c_stat)
[tclTHEN tcl_erase_info (just_tac _then cut info);
thus_tac] gls0
@@ -542,12 +545,12 @@ let decompose_eq id gls =
then (args.(0),
args.(1),
args.(2))
- else error "previous step is not an equality"
- | _ -> error "previous step is not an equality"
+ else error "Previous step is not an equality."
+ | _ -> error "Previous step is not an equality."
let instr_rew _thus rew_side cut gls0 =
let last_id =
- try get_last (pf_env gls0) with _ -> error "no previous equality" in
+ try get_last (pf_env gls0) with _ -> error "No previous equality." in
let typ,lhs,rhs = decompose_eq last_id gls0 in
let items_tac gls =
match cut.cut_by with
@@ -572,14 +575,14 @@ let instr_rew _thus rew_side cut gls0 =
match rew_side with
Lhs ->
let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in
- tclTHENS (internal_cut c_id new_eq)
+ tclTHENS (assert_postpone c_id new_eq)
[tclTHEN tcl_erase_info
(tclTHENS (transitivity lhs)
[just_tac;exact_check (mkVar last_id)]);
thus_tac new_eq] gls0
| Rhs ->
let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in
- tclTHENS (internal_cut c_id new_eq)
+ tclTHENS (assert_postpone c_id new_eq)
[tclTHEN tcl_erase_info
(tclTHENS (transitivity rhs)
[exact_check (mkVar last_id);just_tac]);
@@ -600,7 +603,7 @@ let instr_claim _thus st gls0 =
else tclIDTAC gls in
let ninfo1 = {pm_stack=
(if _thus then Focus_claim else Claim)::info.pm_stack} in
- tclTHENS (internal_cut id st.st_it)
+ tclTHENS (assert_postpone id st.st_it)
[tcl_change_info ninfo1;
thus_tac] gls0
@@ -691,7 +694,7 @@ let instr_suffices _then cut gls0 =
let c_term = applist (mkVar c_id,List.map mkMeta metas) in
let thus_tac gls=
thus_tac c_term c_head c_ctx gls in
- tclTHENS (internal_cut c_id c_stat)
+ tclTHENS (assert_postpone c_id c_stat)
[tclTHENLIST
[ assume_tac ctx;
tcl_erase_info;
@@ -730,7 +733,7 @@ let rec consider_match may_intro introduced available expected gls =
match available,expected with
[],[] ->
tclIDTAC gls
- | _,[] -> error "last statements do not match a complete hypothesis"
+ | _,[] -> error "Last statements do not match a complete hypothesis."
(* should tell which ones *)
| [],hyps ->
if may_intro then
@@ -740,11 +743,11 @@ let rec consider_match may_intro introduced available expected gls =
(intro_mustbe_force id)
(consider_match true [] [id] hyps)
(fun _ ->
- error "not enough sub-hypotheses to match statements")
+ error "Not enough sub-hypotheses to match statements.")
gls
end
else
- error "not enough sub-hypotheses to match statements"
+ error "Not enough sub-hypotheses to match statements."
(* should tell which ones *)
| id::rest_ids,(Hvar st | Hprop st)::rest ->
tclIFTHENELSE (convert_hyp (id,None,st.st_it))
@@ -761,7 +764,7 @@ let rec consider_match may_intro introduced available expected gls =
(fun gls ->
let nhyps =
try conjunction_arity id gls with
- Not_found -> error "matching hypothesis not found" in
+ Not_found -> error "Matching hypothesis not found." in
tclTHENLIST
[general_case_analysis false (mkVar id,NoBindings);
intron_then nhyps []
@@ -777,7 +780,7 @@ let consider_tac c hyps gls =
| _ ->
let id = pf_get_new_id (id_of_string "_tmp") gls in
tclTHEN
- (forward None (Genarg.IntroIdentifier id) c)
+ (forward None (dummy_loc, Genarg.IntroIdentifier id) c)
(consider_match false [] [id] hyps) gls
@@ -818,7 +821,7 @@ let cast_tac id_or_thesis typ gls =
let (_,body,_) = pf_get_hyp gls id in
convert_hyp (id,body,typ) gls
| Thesis (For _ ) ->
- error "\"thesis for ...\" is not applicable here"
+ error "\"thesis for ...\" is not applicable here."
| Thesis Plain ->
convert_concl typ DEFAULTcast gls
@@ -884,7 +887,7 @@ let build_per_info etype casee gls =
try
destInd hd
with _ ->
- error "Case analysis must be done on an inductive object" in
+ error "Case analysis must be done on an inductive object." in
let mind,oind = Global.lookup_inductive ind in
let nparams,index =
match etype with
@@ -955,7 +958,7 @@ let suppose_tac hyps gls0 =
let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
let old_clauses,stack = register_nodep_subcase id info.pm_stack in
let ninfo2 = {pm_stack=stack} in
- tclTHENS (internal_cut id clause)
+ tclTHENS (assert_postpone id clause)
[tclTHENLIST [tcl_change_info ninfo1;
assume_tac hyps;
clear old_clauses];
@@ -1042,7 +1045,7 @@ let rec add_branch ((id,_) as cpl) pats tree=
| Split_patt (_,ind0,_) ->
if (ind <> ind0) then error
(* this can happen with coercions *)
- "Case pattern belongs to wrong inductive type";
+ "Case pattern belongs to wrong inductive type.";
let mapi i ati bri =
if i = pred cnum then
let nargs =
@@ -1083,12 +1086,12 @@ let thesis_for obj typ per_info env=
let _ = if ind <> per_info.per_ind then
errorlabstrm "thesis_for"
((Printer.pr_constr_env env obj) ++ spc () ++
- str "cannot give an induction hypothesis (wrong inductive type)") in
+ str"cannot give an induction hypothesis (wrong inductive type).") in
let params,args = list_chop per_info.per_nparams all_args in
let _ = if not (List.for_all2 eq_constr params per_info.per_params) then
errorlabstrm "thesis_for"
((Printer.pr_constr_env env obj) ++ spc () ++
- str "cannot give an induction hypothesis (wrong parameters)") in
+ str "cannot give an induction hypothesis (wrong parameters).") in
let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
compose_prod rc (whd_beta hd2)
@@ -1161,7 +1164,7 @@ let case_tac params pat_info hyps gls0 =
register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info
pat_info.pat_pat ek in
let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in
- tclTHENS (internal_cut id clause)
+ tclTHENS (assert_postpone id clause)
[tclTHENLIST
[tcl_change_info ninfo1;
assume_st (params@pat_info.pat_vars);
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-01 08:43:27 +0000