From e824d429363262a9ff9db117282fe15289b5ab59 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 5 Oct 2014 15:15:58 +0200 Subject: A version of convert_concl and convert_hyp in new proof engine. Not very optimized though (if we apply convert_hyp on any hyp, a new evar will be generated for every different hyp...). --- plugins/decl_mode/decl_proof_instr.ml | 14 +++++++------- plugins/omega/coq_omega.ml | 10 +++++----- plugins/quote/quote.ml | 4 ++-- plugins/xml/README | 15 --------------- 4 files changed, 14 insertions(+), 29 deletions(-) delete mode 100644 plugins/xml/README (limited to 'plugins') 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. -- cgit v1.2.3