diff options
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/Bintree.v | 10 | ||||
| -rw-r--r-- | plugins/rtauto/Rtauto.v | 239 | ||||
| -rw-r--r-- | plugins/rtauto/g_rtauto.ml4 | 13 | ||||
| -rw-r--r-- | plugins/rtauto/proof_search.ml | 29 | ||||
| -rw-r--r-- | plugins/rtauto/proof_search.mli | 14 | ||||
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 72 | ||||
| -rw-r--r-- | plugins/rtauto/refl_tauto.mli | 23 | ||||
| -rw-r--r-- | plugins/rtauto/vo.itarget | 2 |
8 files changed, 205 insertions, 197 deletions
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 36460187..600e8993 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Export List. diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index 0dc6e31b..06cdf76b 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -1,15 +1,17 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Export List. Require Export Bintree. -Require Import Bool. +Require Import Bool BinPos. Declare ML Module "rtauto_plugin". @@ -96,8 +98,6 @@ match F with | F_push H hyps0 F0 => interp_ctx hyps0 F0 ([[H]] -> G) end. -Require Export BinPos. - Ltac wipe := intros;simpl;constructor. Lemma compose0 : @@ -255,122 +255,115 @@ Theorem interp_proof: forall p hyps F gl, check_proof hyps gl p = true -> interp_ctx hyps F [[gl]]. -induction p;intros hyps F gl. - -(* cas Axiom *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f nth_f e;rewrite <- (form_eq_refl e). -apply project with p;trivial. - -(* Cas Arrow_Intro *) -Focus 1. -destruct gl;clean. -simpl;intros. -change (interp_ctx (hyps\gl1) (F_push gl1 hyps F) [[gl2]]). -apply IHp;try constructor;trivial. - -(* Cas Arrow_Elim *) -Focus 1. -simpl check_proof;case_eq (get p hyps);clean. -intros f ef;case_eq (get p0 hyps);clean. -intros f0 ef0;destruct f0;clean. -case_eq (form_eq f f0_1);clean. -simpl;intros e check_p1. -generalize (project F ef) (project F ef0) -(IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1); -clear check_p1 IHp p p0 p1 ef ef0. -simpl. -apply compose3. -rewrite (form_eq_refl e). -auto. - -(* cas Arrow_Destruct *) -Focus 1. -simpl;case_eq (get p1 hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -case_eq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2);clean. -intros check_p1 check_p2. -generalize (project F ef) -(IHp1 (hyps \ f1_2 =>> f2 \ f1_1) -(F_push f1_1 (hyps \ f1_2 =>> f2) - (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1) -(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2). -simpl;apply compose3;auto. - -(* Cas False_Elim *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -intros _; generalize (project F ef). -apply compose1;apply False_ind. - -(* Cas And_Intro *) -Focus 1. -simpl;destruct gl;clean. -case_eq (check_proof hyps gl1 p1);clean. -intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2). -apply compose2 ;simpl;auto. - -(* cas And_Elim *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -intro check_p;generalize (project F ef) -(IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p). -simpl;apply compose2;intros [h1 h2];auto. - -(* cas And_Destruct *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -intro H;generalize (project F ef) -(IHp (hyps \ f1_1 =>> f1_2 =>> f2) -(F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H);clear H;simpl. -apply compose2;auto. - -(* cas Or_Intro_left *) -Focus 1. -destruct gl;clean. -intro Hp;generalize (IHp hyps F gl1 Hp). -apply compose1;simpl;auto. - -(* cas Or_Intro_right *) -Focus 1. -destruct gl;clean. -intro Hp;generalize (IHp hyps F gl2 Hp). -apply compose1;simpl;auto. - -(* cas Or_elim *) -Focus 1. -simpl;case_eq (get p1 hyps);clean. -intros f ef;destruct f;clean. -case_eq (check_proof (hyps \ f1) gl p2);clean. -intros check_p1 check_p2;generalize (project F ef) -(IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1) -(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2); -simpl;apply compose3;simpl;intro h;destruct h;auto. - -(* cas Or_Destruct *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -intro check_p0;generalize (project F ef) -(IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2) -(F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) - (F_push (f1_1 =>> f2) hyps F)) gl check_p0);simpl. -apply compose2;auto. - -(* cas Cut *) -Focus 1. -simpl;case_eq (check_proof hyps f p1);clean. -intros check_p1 check_p2; -generalize (IHp1 hyps F f check_p1) -(IHp2 (hyps\f) (F_push f hyps F) gl check_p2); -simpl; apply compose2;auto. +induction p; intros hyps F gl. + +- (* Axiom *) + simpl;case_eq (get p hyps);clean. + intros f nth_f e;rewrite <- (form_eq_refl e). + apply project with p;trivial. + +- (* Arrow_Intro *) + destruct gl; clean. + simpl; intros. + change (interp_ctx (hyps\gl1) (F_push gl1 hyps F) [[gl2]]). + apply IHp; try constructor; trivial. + +- (* Arrow_Elim *) + simpl check_proof; case_eq (get p hyps); clean. + intros f ef; case_eq (get p0 hyps); clean. + intros f0 ef0; destruct f0; clean. + case_eq (form_eq f f0_1); clean. + simpl; intros e check_p1. + generalize (project F ef) (project F ef0) + (IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1); + clear check_p1 IHp p p0 p1 ef ef0. + simpl. + apply compose3. + rewrite (form_eq_refl e). + auto. + +- (* Arrow_Destruct *) + simpl; case_eq (get p1 hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + case_eq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2); clean. + intros check_p1 check_p2. + generalize (project F ef) + (IHp1 (hyps \ f1_2 =>> f2 \ f1_1) + (F_push f1_1 (hyps \ f1_2 =>> f2) + (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1) + (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2). + simpl; apply compose3; auto. + +- (* False_Elim *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + intros _; generalize (project F ef). + apply compose1; apply False_ind. + +- (* And_Intro *) + simpl; destruct gl; clean. + case_eq (check_proof hyps gl1 p1); clean. + intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2). + apply compose2 ; simpl; auto. + +- (* And_Elim *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + intro check_p; + generalize (project F ef) + (IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p). + simpl; apply compose2; intros [h1 h2]; auto. + +- (* And_Destruct*) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + intro H; + generalize (project F ef) + (IHp (hyps \ f1_1 =>> f1_2 =>> f2) + (F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H); + clear H; simpl. + apply compose2; auto. + +- (* Or_Intro_left *) + destruct gl; clean. + intro Hp; generalize (IHp hyps F gl1 Hp). + apply compose1; simpl; auto. + +- (* Or_Intro_right *) + destruct gl; clean. + intro Hp; generalize (IHp hyps F gl2 Hp). + apply compose1; simpl; auto. + +- (* Or_elim *) + simpl; case_eq (get p1 hyps); clean. + intros f ef; destruct f; clean. + case_eq (check_proof (hyps \ f1) gl p2); clean. + intros check_p1 check_p2; + generalize (project F ef) + (IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1) + (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2); + simpl; apply compose3; simpl; intro h; destruct h; auto. + +- (* Or_Destruct *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + intro check_p0; + generalize (project F ef) + (IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2) + (F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) + (F_push (f1_1 =>> f2) hyps F)) gl check_p0); + simpl. + apply compose2; auto. + +- (* Cut *) + simpl; case_eq (check_proof hyps f p1); clean. + intros check_p1 check_p2; + generalize (IHp1 hyps F f check_p1) + (IHp2 (hyps\f) (F_push f hyps F) gl check_p2); + simpl; apply compose2; auto. Qed. Theorem Reflect: forall gl prf, if check_proof empty gl prf then [[gl]] else True. diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index d27b0483..aa675763 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -1,12 +1,15 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) + +open Ltac_plugin DECLARE PLUGIN "rtauto_plugin" diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 8b926111..3de59239 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors @@ -46,8 +48,7 @@ let reset_info () = let pruning = ref true let opt_pruning= - {optsync=true; - optdepr=false; + {optdepr=false; optname="Rtauto Pruning"; optkey=["Rtauto";"Pruning"]; optread=(fun () -> !pruning); @@ -146,7 +147,7 @@ let add_step s sub = | SI_Or_r,[p] -> I_Or_r p | SE_Or i,[p1;p2] -> E_Or(i,p1,p2) | SD_Or i,[p] -> D_Or(i,p) - | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity") + | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity.") type 'a with_deps = {dep_it:'a; @@ -168,7 +169,7 @@ type state = let project = function Complete prf -> prf - | Incomplete (_,_) -> anomaly (Pp.str "not a successful state") + | Incomplete (_,_) -> anomaly (Pp.str "not a successful state.") let pop n prf = let nprf= @@ -362,7 +363,7 @@ let search_norev seq= (Arrow(f2,f3))) f1; add_hyp (embed nseq) f3]):: !goals - | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen") in + | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen.") in Int.Map.iter add_one seq.norev_hyps; List.rev !goals @@ -387,7 +388,7 @@ let search_in_rev_hyps seq= | Arrow (Disjunct (f1,f2),f0) -> [make_step (SD_Or(i)), [add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]] - | _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen") + | _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen.") with Not_found -> search_norev seq @@ -465,7 +466,7 @@ let branching = function | _::next -> s_info.nd_branching<-s_info.nd_branching+List.length next in List.map (append stack) successors - | Complete prf -> anomaly (Pp.str "already succeeded") + | Complete prf -> anomaly (Pp.str "already succeeded.") open Pp @@ -505,12 +506,12 @@ let pp_mapint map = pp_form obj ++ str " => " ++ pp_list (fun (i,f) -> pp_form f) l ++ cut ()) ) map; - str "{ " ++ vb 0 ++ (!pp) ++ str " }" ++ close () + str "{ " ++ hv 0 (!pp ++ str " }") let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2 let pp_gl gl= cut () ++ - str "{ " ++ vb 0 ++ + str "{ " ++ hv 0 ( begin match gl.abs with None -> str "" @@ -520,7 +521,7 @@ let pp_gl gl= cut () ++ str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++ str "arrows=" ++ pp_mapint gl.right ++ cut () ++ str "cnx =" ++ pp_list pp_connect gl.cnx ++ cut () ++ - str "goal =" ++ pp_form gl.gl ++ str " }" ++ close () + str "goal =" ++ pp_form gl.gl ++ str " }") let pp = function diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli index 31f8e7b5..607cdc95 100644 --- a/plugins/rtauto/proof_search.mli +++ b/plugins/rtauto/proof_search.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) type form= @@ -38,9 +40,9 @@ val branching: state -> state list val success: state -> bool -val pp: state -> Pp.std_ppcmds +val pp: state -> Pp.t -val pr_form : form -> Pp.std_ppcmds +val pr_form : form -> Pp.t val reset_info : unit -> unit diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 4ed90795..946b6dff 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -1,16 +1,21 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) + module Search = Explore.Make(Proof_search) +open Ltac_plugin open CErrors open Util open Term +open Constr open Tacmach open Proof_search open Context.Named.Declaration @@ -21,28 +26,28 @@ let step_count = ref 0 let node_count = ref 0 -let logic_constant = - Coqlib.gen_constant "refl_tauto" ["Init";"Logic"] +let logic_constant s = Universes.constr_of_global @@ + Coqlib.coq_reference "refl_tauto" ["Init";"Logic"] s let li_False = lazy (destInd (logic_constant "False")) -let li_and = lazy (destInd (logic_constant "and")) -let li_or = lazy (destInd (logic_constant "or")) +let li_and = lazy (destInd (logic_constant "and")) +let li_or = lazy (destInd (logic_constant "or")) -let pos_constant = - Coqlib.gen_constant "refl_tauto" ["Numbers";"BinNums"] +let pos_constant s = Universes.constr_of_global @@ + Coqlib.coq_reference "refl_tauto" ["Numbers";"BinNums"] s let l_xI = lazy (pos_constant "xI") let l_xO = lazy (pos_constant "xO") let l_xH = lazy (pos_constant "xH") -let store_constant = - Coqlib.gen_constant "refl_tauto" ["rtauto";"Bintree"] +let store_constant s = Universes.constr_of_global @@ + Coqlib.coq_reference "refl_tauto" ["rtauto";"Bintree"] s let l_empty = lazy (store_constant "empty") let l_push = lazy (store_constant "push") -let constant= - Coqlib.gen_constant "refl_tauto" ["rtauto";"Rtauto"] +let constant s = Universes.constr_of_global @@ + Coqlib.coq_reference "refl_tauto" ["rtauto";"Rtauto"] s let l_Reflect = lazy (constant "Reflect") @@ -66,22 +71,21 @@ let l_E_Or = lazy (constant "E_Or") let l_D_Or = lazy (constant "D_Or") -let special_whd gl= - let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in - (fun t -> CClosure.whd_val infos (CClosure.inject t)) +let special_whd gl c = + Reductionops.clos_whd_flags CClosure.all (pf_env gl) (Tacmach.project gl) c -let special_nf gl= - let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in - (fun t -> CClosure.norm_val infos (CClosure.inject t)) +let special_nf gl c = + Reductionops.clos_norm_flags CClosure.betaiotazeta (pf_env gl) (Tacmach.project gl) c type atom_env= {mutable next:int; mutable env:(constr*int) list} let make_atom atom_env term= + let term = EConstr.Unsafe.to_constr term in try let (_,i)= - List.find (fun (t,_)-> eq_constr term t) atom_env.env + List.find (fun (t,_)-> Constr.equal term t) atom_env.env in Atom i with Not_found -> let i=atom_env.next in @@ -90,13 +94,16 @@ let make_atom atom_env term= Atom i let rec make_form atom_env gls term = + let open EConstr in + let open Vars in let normalize=special_nf gls in let cciterm=special_whd gls term in - match kind_of_term cciterm with + let sigma = Tacmach.project gls in + match EConstr.kind sigma cciterm with Prod(_,a,b) -> - if not (Termops.dependent (mkRel 1) b) && + if noccurn sigma 1 b && Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) a == InProp + (pf_env gls) sigma a == InProp then let fa=make_form atom_env gls a in let fb=make_form atom_env gls b in @@ -113,7 +120,7 @@ let rec make_form atom_env gls term = | App(hd,argv) when Int.equal (Array.length argv) 2 -> begin try - let ind, _ = destInd hd in + let ind, _ = destInd sigma hd in if Names.eq_ind ind (fst (Lazy.force li_and)) then let fa=make_form atom_env gls argv.(0) in let fb=make_form atom_env gls argv.(1) in @@ -134,7 +141,7 @@ let rec make_hyps atom_env gls lenv = function | LocalAssum (id,typ)::rest -> let hrec= make_hyps atom_env gls (typ::lenv) rest in - if List.exists (Termops.dependent (mkVar id)) lenv || + if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id c) lenv || (Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) typ != InProp) then @@ -233,8 +240,7 @@ open Goptions let verbose = ref false let opt_verbose= - {optsync=true; - optdepr=false; + {optdepr=false; optname="Rtauto Verbose"; optkey=["Rtauto";"Verbose"]; optread=(fun () -> !verbose); @@ -245,8 +251,7 @@ let _ = declare_bool_option opt_verbose let check = ref false let opt_check= - {optsync=true; - optdepr=false; + {optdepr=false; optname="Rtauto Check"; optkey=["Rtauto";"Check"]; optread=(fun () -> !check); @@ -263,7 +268,7 @@ let rtauto_tac gls= let _= if Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) gl != InProp - then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in + then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in let glf=make_form gamma gls gl in let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in let formula= @@ -282,7 +287,7 @@ let rtauto_tac gls= let prf = try project (search_fun (init_state [] formula)) with Not_found -> - errorlabstrm "rtauto" (Pp.str "rtauto couldn't find any proof") in + user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in let search_end_time = System.get_time () in let _ = if !verbose then begin @@ -298,7 +303,7 @@ let rtauto_tac gls= build_form formula; build_proof [] 0 prf|]) in let term= - applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in + applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in let build_end_time=System.get_time () in let _ = if !verbose then begin @@ -312,6 +317,7 @@ let rtauto_tac gls= str "Giving proof term to Coq ... ") end in let tac_start_time = System.get_time () in + let term = EConstr.of_constr term in let result= if !check then Proofview.V82.of_tactic (Tactics.exact_check term) gls diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index 9a14ac6c..a91dd666 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -1,24 +1,27 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* raises Not_found if no proof is found *) + type atom_env= {mutable next:int; - mutable env:(Term.constr*int) list} + mutable env:(Constr.t*int) list} val make_form : atom_env -> - Proof_type.goal Tacmach.sigma -> Term.types -> Proof_search.form + Goal.goal Evd.sigma -> EConstr.types -> Proof_search.form val make_hyps : atom_env -> - Proof_type.goal Tacmach.sigma -> - Term.types list -> - Context.Named.t -> + Goal.goal Evd.sigma -> + EConstr.types list -> + EConstr.named_context -> (Names.Id.t * Proof_search.form) list -val rtauto_tac : Proof_type.tactic +val rtauto_tac : Tacmach.tactic diff --git a/plugins/rtauto/vo.itarget b/plugins/rtauto/vo.itarget deleted file mode 100644 index 4c9364ad..00000000 --- a/plugins/rtauto/vo.itarget +++ /dev/null @@ -1,2 +0,0 @@ -Bintree.vo -Rtauto.vo |