aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml14
-rw-r--r--plugins/omega/coq_omega.ml10
-rw-r--r--plugins/quote/quote.ml4
-rw-r--r--plugins/xml/README15
-rw-r--r--proofs/logic.ml10
-rw-r--r--proofs/logic.mli3
-rw-r--r--proofs/proofview.ml2
-rw-r--r--proofs/proofview.mli2
-rw-r--r--tactics/eauto.ml44
-rw-r--r--tactics/rewrite.ml4
-rw-r--r--tactics/tactics.ml54
-rw-r--r--tactics/tactics.mli6
12 files changed, 76 insertions, 52 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index a21447fbb..470dc9d9c 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -580,7 +580,7 @@ let assume_tac hyps gls =
tclTHEN
(push_intro_tac
(fun id ->
- convert_hyp (id,None,st.st_it)) st.st_label))
+ Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label))
hyps tclIDTAC gls
let assume_hyps_or_theses hyps gls =
@@ -590,7 +590,7 @@ let assume_hyps_or_theses hyps gls =
tclTHEN
(push_intro_tac
(fun id ->
- convert_hyp (id,None,c)) nam)
+ Proofview.V82.of_tactic (convert_hyp (id,None,c))) nam)
| Hprop {st_label=nam;st_it=Thesis (tk)} ->
tclTHEN
(push_intro_tac
@@ -602,7 +602,7 @@ let assume_st hyps gls =
(fun st ->
tclTHEN
(push_intro_tac
- (fun id -> convert_hyp (id,None,st.st_it)) st.st_label))
+ (fun id -> Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label))
hyps tclIDTAC gls
let assume_st_letin hyps gls =
@@ -611,7 +611,7 @@ let assume_st_letin hyps gls =
tclTHEN
(push_intro_tac
(fun id ->
- convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label))
+ Proofview.V82.of_tactic (convert_hyp (id,Some (fst st.st_it),snd st.st_it))) st.st_label))
hyps tclIDTAC gls
(* suffices *)
@@ -705,7 +705,7 @@ let rec consider_match may_intro introduced available expected gls =
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))
+ tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it)))
begin
match st.st_label with
Anonymous ->
@@ -774,11 +774,11 @@ let cast_tac id_or_thesis typ gls =
match id_or_thesis with
This id ->
let (_,body,_) = pf_get_hyp gls id in
- convert_hyp (id,body,typ) gls
+ Proofview.V82.of_tactic (convert_hyp (id,body,typ)) gls
| Thesis (For _ ) ->
error "\"thesis for ...\" is not applicable here."
| Thesis Plain ->
- convert_concl typ DEFAULTcast gls
+ Proofview.V82.of_tactic (convert_concl typ DEFAULTcast) gls
(* per cases *)
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index f8fd71ae2..847fda8cd 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -566,7 +566,7 @@ let abstract_path typ path t =
let focused_simpl path gl =
let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
- convert_concl_no_check newc DEFAULTcast gl
+ Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl
let focused_simpl path = focused_simpl path
@@ -1806,15 +1806,15 @@ let destructure_hyps =
match destructurate_type (pf_nf typ) with
| Kapp(Nat,_) ->
(Tacticals.New.tclTHEN
- (Proofview.V82.tactic (convert_hyp_no_check
+ (convert_hyp_no_check
(i,body,
- (mkApp (Lazy.force coq_neq, [| t1;t2|])))))
+ (mkApp (Lazy.force coq_neq, [| t1;t2|]))))
(loop lit))
| Kapp(Z,_) ->
(Tacticals.New.tclTHEN
- (Proofview.V82.tactic (convert_hyp_no_check
+ (convert_hyp_no_check
(i,body,
- (mkApp (Lazy.force coq_Zne, [| t1;t2|])))))
+ (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))
(loop lit))
| _ -> loop lit
end
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index ed7f18001..64166a0de 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -457,8 +457,8 @@ let quote f lid =
| _ -> assert false
in
match ivs.variable_lhs with
- | None -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast)
- | Some _ -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast)
+ | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast
+ | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast
end
let gen_quote cont c f lid =
diff --git a/plugins/xml/README b/plugins/xml/README
deleted file mode 100644
index e3bcdaf05..000000000
--- a/plugins/xml/README
+++ /dev/null
@@ -1,15 +0,0 @@
-The xml export plugin for Coq has been discontinued for lack of users:
-it was most certainly broken while imposing a non-negligible cost on
-Coq development. Its purpose was to give export Coq's kernel objects
-in xml form for treatment by external tools.
-
-If you are looking for such a tool, you may want to look at commit
-7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9 responsible for the deletion
-of this plugin (for instance, git checkout
-7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9^ including the "^", will lead
-you to the last commit before the xml plugin was deleted).
-
-Bear in mind, however, that the plugin was not working properly at the
-time. You may want instead to write to the original author of the
-plugin, Claudio Sacerdoti-Coen at sacerdot@cs.unibo.it. He has a
-stable version of the plugin for an old version of Coq.
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5de7b901d..2d302510e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -492,18 +492,18 @@ and mk_casegoals sigma goal goalacc p c =
(acc'',lbrty,conclty,sigma,p',c')
-let convert_hyp sign sigma (id,b,bt as d) =
+let convert_hyp check sign sigma (id,b,bt as d) =
let env = Global.env() in
let reorder = ref [] in
let sign' =
apply_to_hyp sign id
(fun _ (_,c,ct) _ ->
let env = Global.env_of_context sign in
- if !check && not (is_conv env sigma bt ct) then
+ if check && not (is_conv env sigma bt ct) then
error ("Incorrect change of the type of "^(Id.to_string id)^".");
- if !check && not (Option.equal (is_conv env sigma) b c) then
+ if check && not (Option.equal (is_conv env sigma) b c) then
error ("Incorrect change of the body of "^(Id.to_string id)^".");
- if !check then reorder := check_decl_position env sign d;
+ if check then reorder := check_decl_position env sign d;
d) in
reorder_val_context env sign' !reorder
@@ -665,7 +665,7 @@ let prim_refiner r sigma goal =
([sg], sigma)
| Convert_hyp (id,copt,ty) ->
- let (gl,ev,sigma) = mk_goal (convert_hyp sign sigma (id,copt,ty)) cl in
+ let (gl,ev,sigma) = mk_goal (convert_hyp !check sign sigma (id,copt,ty)) cl in
let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
([gl], sigma)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index da54ef0a8..7714b8658 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -51,3 +51,6 @@ type refiner_error =
exception RefinerError of refiner_error
val catchable_exception : exn -> bool
+
+val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
+ Context.named_declaration -> Environ.named_context_val
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 9f8458ba7..8fe924e0f 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -877,6 +877,8 @@ module Goal = struct
let hyps { env=env } = Environ.named_context env
let concl { concl=concl } = concl
+ let raw_concl { concl=concl } = concl
+
let nf_enter_t = Goal.nf_enter begin fun env sigma concl self ->
{env=env;sigma=sigma;concl=concl;self=self}
end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 0eae9b605..ebaa63267 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -403,6 +403,8 @@ module Goal : sig
val env : 'a t -> Environ.env
val sigma : 'a t -> Evd.evar_map
+ val raw_concl : 'a t -> Term.constr
+
(* [nf_enter t] execute the goal-dependent tactic [t] in each goal
independently. In particular [t] need not backtrack the same way in
each goal. *)
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 334e0c22a..eb9ffd425 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -563,7 +563,7 @@ let autounfold_one db cl gl =
if did then
match cl with
| Some hyp -> change_in_hyp None (fun env sigma -> sigma, c') hyp gl
- | None -> convert_concl_no_check c' DEFAULTcast gl
+ | None -> Proofview.V82.of_tactic (convert_concl_no_check c' DEFAULTcast) gl
else tclFAIL 0 (str "Nothing to unfold") gl
(* Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *)
@@ -611,7 +611,7 @@ END
TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> [ Proofview.V82.tactic (convert_concl_no_check x DEFAULTcast) ]
+| ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ]
END
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 63885318c..0207b9b0f 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1543,7 +1543,7 @@ let cl_rewrite_clause_newtac ?abs strat clause =
| Some id, (undef, Some p, newt) ->
assert_replacing id newt (new_refine (undef, p))
| Some id, (undef, None, newt) ->
- Proofview.V82.tactic (Tacmach.convert_hyp_no_check (id, None, newt))
+ convert_hyp_no_check (id, None, newt)
| None, (undef, Some p, newt) ->
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -1555,7 +1555,7 @@ let cl_rewrite_clause_newtac ?abs strat clause =
Proofview.Refine.refine make
end
| None, (undef, None, newt) ->
- Proofview.V82.tactic (Tacmach.convert_concl_no_check newt DEFAULTcast)
+ convert_concl_no_check newt DEFAULTcast
in
Proofview.Goal.nf_enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 68aac55c8..391affd11 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -118,8 +118,38 @@ let _ =
let introduction = Tacmach.introduction
let refine = Tacmach.refine
-let convert_concl = Tacmach.convert_concl
-let convert_hyp = Tacmach.convert_hyp
+
+let convert_concl ?(unsafe=false) ty k =
+ Proofview.Goal.nf_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let conclty = Proofview.Goal.raw_concl gl in
+ let sigma =
+ if not unsafe then begin
+ ignore (Typing.type_of env sigma ty);
+ let sigma,b = Reductionops.infer_conv env sigma ty conclty in
+ if not b then error "Not convertible.";
+ sigma
+ end else sigma in
+ Tacticals.New.tclTHEN
+ (Proofview.V82.tclEVARS sigma)
+ (Proofview.Refine.refine (fun h ->
+ let (h,x) = Proofview.Refine.new_evar h env ty in
+ (h, if k == DEFAULTcast then x else mkCast(x,k,conclty))))
+ end
+
+let convert_hyp ?(unsafe=false) d =
+ Proofview.Goal.nf_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let ty = Proofview.Goal.raw_concl gl in
+ let sign = convert_hyp (not unsafe) (named_context_val env) sigma d in
+ let env = reset_with_named_context sign env in
+ Proofview.Refine.refine (fun h -> Proofview.Refine.new_evar h env ty)
+ end
+
+let convert_concl_no_check = convert_concl ~unsafe:true
+let convert_hyp_no_check = convert_hyp ~unsafe:true
let convert_gen pb x y =
Proofview.Goal.enter begin fun gl ->
@@ -390,11 +420,11 @@ let bind_red_expr_occurrences occs nbcl redexp =
certain hypothesis *)
let reduct_in_concl (redfun,sty) gl =
- convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl
+ Proofview.V82.of_tactic (convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty) gl
let reduct_in_hyp redfun (id,where) gl =
- convert_hyp_no_check
- (pf_reduce_decl redfun where (pf_get_hyp gl id) gl) gl
+ Proofview.V82.of_tactic (convert_hyp_no_check
+ (pf_reduce_decl redfun where (pf_get_hyp gl id) gl)) gl
let revert_cast (redfun,kind as r) =
if kind == DEFAULTcast then (redfun,REVERTcast) else r
@@ -413,7 +443,7 @@ let tclWITHEVARS f k gl =
let e_reduct_in_concl (redfun,sty) gl =
tclWITHEVARS
(fun env sigma -> redfun env sigma (pf_concl gl))
- (fun c -> convert_concl_no_check c sty) gl
+ (fun c -> Proofview.V82.of_tactic (convert_concl_no_check c sty)) gl
let e_pf_reduce_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env sigma =
match c with
@@ -430,7 +460,7 @@ let e_pf_reduce_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env
let e_reduct_in_hyp redfun (id,where) gl =
tclWITHEVARS
(e_pf_reduce_decl redfun where (pf_get_hyp gl id))
- convert_hyp_no_check gl
+ (fun s -> Proofview.V82.of_tactic (convert_hyp_no_check s)) gl
type change_arg = env -> evar_map -> evar_map * constr
@@ -1690,7 +1720,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in
(Tacticals.New.tclTHENLIST
[Proofview.V82.tclEVARS sigma;
- Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast);
+ convert_concl_no_check redcl DEFAULTcast;
intros; apply_tac])
end
@@ -2098,9 +2128,9 @@ let letin_tac_gen with_eq abs ty =
let (sigma,newcl,eq_tac) = eq_tac gl in
Tacticals.New.tclTHENLIST
[ Proofview.V82.tclEVARS sigma;
- Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
+ convert_concl_no_check newcl DEFAULTcast;
intro_gen (NamingMustBe (dloc,id)) (decode_hyp lastlhyp) true false;
- Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls);
+ Tacticals.New.tclMAP convert_hyp_no_check depdecls;
eq_tac ]))
end
@@ -3894,7 +3924,7 @@ let symmetry_red allowred =
match with_eqn with
| Some eq_data,_,_ ->
Tacticals.New.tclTHEN
- (Proofview.V82.tactic (convert_concl_no_check concl DEFAULTcast))
+ (convert_concl_no_check concl DEFAULTcast)
(Tacticals.New.pf_constr_of_global eq_data.sym apply)
| None,eq,eq_kind -> prove_symmetry eq eq_kind
end
@@ -3986,7 +4016,7 @@ let transitivity_red allowred t =
match with_eqn with
| Some eq_data,_,_ ->
Tacticals.New.tclTHEN
- (Proofview.V82.tactic (convert_concl_no_check concl DEFAULTcast))
+ (convert_concl_no_check concl DEFAULTcast)
(match t with
| None -> Tacticals.New.pf_constr_of_global eq_data.trans eapply
| Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t]))
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6ecb48101..c2beefdfb 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -32,8 +32,10 @@ val is_quantified_hypothesis : Id.t -> goal sigma -> bool
val introduction : Id.t -> tactic
val refine : constr -> tactic
-val convert_concl : constr -> cast_kind -> tactic
-val convert_hyp : named_declaration -> tactic
+val convert_concl : ?unsafe:bool -> types -> cast_kind -> unit Proofview.tactic
+val convert_hyp : ?unsafe:bool -> named_declaration -> unit Proofview.tactic
+val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
+val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
val thin : Id.t list -> tactic
val mutual_fix :
Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 04:16:30 +0000