diff options
39 files changed, 757 insertions, 653 deletions
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index bb193ebb55..fad6472911 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -25,7 +25,7 @@ echo $TRAVIS_PULL_REQUEST echo $TRAVIS_BRANCH echo $TRAVIS_COMMIT -if [ $TRAVIS_PULL_REQUEST == "461" ] || [ $TRAVIS_BRANCH == "stm+remove_compat_parsing" ]; then - mathcomp_CI_BRANCH=no_camlp4_compat - mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git +if [ $TRAVIS_PULL_REQUEST == "568" ] || [ $TRAVIS_BRANCH == "remove-tactic-compat" ]; then + fiat_parsers_CI_BRANCH=fix-ml + fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat.git fi diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 7f915b7819..8ea1638c99 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -51,6 +51,15 @@ In Constrexpr_ops: interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones were preserving the original sharing of the type. +** Tactic API ** + +- pf_constr_of_global now returns a tactic instead of taking a continuation. + Thus it only generates one instance of the global reference, and it is the + caller's responsibility to perform a focus on the goal. + +- The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase + was very specific. Use tclPROGRESS instead. + ** Ltac API ** Many Ltac specific API has been moved in its own ltac/ folder. Amongst other diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 2d9dec095a..00b31cccee 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -239,21 +239,43 @@ let build_projection intype (cstr:pconstructor) special default gls= (* generate an adhoc tactic following the proof tree *) -let _M =mkMeta - let app_global f args k = - Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) - -let new_app_global f args k = - Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) - -let new_refine c = Proofview.V82.tactic (refine c) -let refine c = refine c + Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> k (mkApp (fc, args)) + +let rec gen_holes env sigma t n accu = + let open Sigma in + if Int.equal n 0 then (sigma, List.rev accu) + else match EConstr.kind sigma t with + | Prod (_, u, t) -> + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma u in + let sigma = Sigma.to_evar_map sigma in + let t = EConstr.Vars.subst1 ev t in + gen_holes env sigma t (pred n) (ev :: accu) + | _ -> assert false + +let app_global_with_holes f args n = + Proofview.Goal.enter { enter = begin fun gl -> + Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + Refine.refine { Sigma.run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in + let t = Tacmach.New.pf_get_type_of gl fc in + let t = Termops.prod_applist sigma t (Array.to_list args) in + let ans = mkApp (fc, args) in + let (sigma, holes) = gen_holes env sigma t n [] in + let ans = applist (ans, holes) in + let evdref = ref sigma in + let () = Typing.e_check env evdref ans concl in + Sigma.Unsafe.of_pair (ans, !evdref) + end } + end } let assert_before n c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> let evm, _ = Tacmach.New.pf_apply type_of gl c in - Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c) + Sigma.Unsafe.of_pair (assert_before n c, evm) end } let refresh_type env evm ty = @@ -281,18 +303,18 @@ let rec proof_tac p : unit Proofview.tactic = let l=constr_of_term p.p_lhs and r=constr_of_term p.p_rhs in refresh_universes (type_of l) (fun typ -> - new_app_global _sym_eq [|typ;r;l;c|] exact_check) + app_global _sym_eq [|typ;r;l;c|] exact_check) | Refl t -> let lr = constr_of_term t in refresh_universes (type_of lr) (fun typ -> - new_app_global _refl_equal [|typ;constr_of_term t|] exact_check) + app_global _refl_equal [|typ;constr_of_term t|] exact_check) | Trans (p1,p2)-> let t1 = constr_of_term p1.p_lhs and t2 = constr_of_term p1.p_rhs and t3 = constr_of_term p2.p_rhs in refresh_universes (type_of t2) (fun typ -> - let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in - Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)]) + let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in + Tacticals.New.tclTHENS prf [(proof_tac p1);(proof_tac p2)]) | Congr (p1,p2)-> let tf1=constr_of_term p1.p_lhs and tx1=constr_of_term p2.p_lhs @@ -303,18 +325,18 @@ let rec proof_tac p : unit Proofview.tactic = refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx -> let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in - let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in - let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in + let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in + let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in let prf = - app_global _trans_eq + app_global_with_holes _trans_eq [|typfx; mkApp(tf1,[|tx1|]); mkApp(tf2,[|tx1|]); - mkApp(tf2,[|tx2|]);_M 2;_M 3|] in - Tacticals.New.tclTHENS (Proofview.V82.tactic (prf refine)) - [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma1 refine)) (proof_tac p1); + mkApp(tf2,[|tx2|])|] 2 in + Tacticals.New.tclTHENS prf + [Tacticals.New.tclTHEN lemma1 (proof_tac p1); Tacticals.New.tclFIRST - [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2); + [Tacticals.New.tclTHEN lemma2 (proof_tac p2); reflexivity; Tacticals.New.tclZEROMSG (Pp.str @@ -330,8 +352,8 @@ let rec proof_tac p : unit Proofview.tactic = build_projection intype cstr special default gl in let injt= - app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in - Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf))) + app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in + Tacticals.New.tclTHEN injt (proof_tac prf))) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end } @@ -341,27 +363,29 @@ let refute_tac c t1 t2 p = let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in let false_t=mkApp (c,[|mkVar hid|]) in let k intype = - let neweq= new_app_global _eq [|intype;tt1;tt2|] in + let neweq= app_global _eq [|intype;tt1;tt2|] in Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k end } -let refine_exact_check c gl = - let evm, _ = pf_apply type_of gl c in - Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl +let refine_exact_check c = + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let evm, _ = Tacmach.New.pf_apply type_of gl c in + Sigma.Unsafe.of_pair (exact_check c, evm) + end } let convert_to_goal_tac c t1 t2 p = Proofview.Goal.enter { enter = begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let k sort = - let neweq= new_app_global _eq [|sort;tt1;tt2|] in + let neweq= app_global _eq [|sort;tt1;tt2|] in let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in let identity=mkLambda (Name x,sort,mkRel 1) in - let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in + let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) - [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] + [proof_tac p; endt refine_exact_check] in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k end } @@ -392,27 +416,25 @@ let discriminate_tac (cstr,u as cstru) p = let pred = mkLambda(Name xid,outtype,mkRel 1) in let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in let proj = build_projection intype cstru trivial concl gl in - let injt=app_global _f_equal + let injt = app_global _f_equal [|intype;outtype;proj;t1;t2;mkVar hid|] in let endt k = injt (fun injt -> app_global _eq_rect [|outtype;trivial;pred;identity;concl;injt|] k) in - let neweq=new_app_global _eq [|intype;t1;t2|] in + let neweq = app_global _eq [|intype;t1;t2|] in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) - [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]) + [proof_tac p; endt refine_exact_check]) end } (* wrap everything *) -let build_term_to_complete uf meta pac = +let build_term_to_complete uf pac = let cinfo = get_constructor_info uf pac.cnode in - let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in - let dummy_args = List.rev (List.init pac.arity meta) in - let all_args = List.rev_append real_args dummy_args in + let real_args = List.rev_map (fun i -> constr_of_term (term uf i)) pac.args in let (kn, u) = cinfo.ci_constr in - applist (mkConstructU (kn, EInstance.make u), all_args) + (applist (mkConstructU (kn, EInstance.make u), real_args), pac.arity) let cc_tactic depth additionnal_terms = Proofview.Goal.enter { enter = begin fun gl -> @@ -434,16 +456,17 @@ let cc_tactic depth additionnal_terms = let cstr=(get_constructor_info uf ipac.cnode).ci_constr in discriminate_tac cstr p | Incomplete -> + let open Glob_term in let env = Proofview.Goal.env gl in - let metacnt = ref 0 in - let newmeta _ = incr metacnt; _M !metacnt in - let terms_to_complete = - List.map - (build_term_to_complete uf newmeta) - (epsilons uf) in + let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in + let hole = GHole (Loc.ghost, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in + let pr_missing (c, missing) = + let c = Detyping.detype ~lax:true false [] env sigma c in + let holes = List.init missing (fun _ -> hole) in + Printer.pr_glob_constr_env env (GApp (Loc.ghost, c, holes)) + in Feedback.msg_info - (Pp.str "Goal is solvable by congruence but \ - some arguments are missing."); + (Pp.str "Goal is solvable by congruence but some arguments are missing."); Feedback.msg_info (Pp.str " Try " ++ hov 8 @@ -451,7 +474,7 @@ let cc_tactic depth additionnal_terms = str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(") - (Termops.print_constr_env env sigma) + pr_missing terms_to_complete ++ str ")\"," end ++ @@ -472,13 +495,13 @@ let cc_tactic depth additionnal_terms = convert_to_hyp_tac ida ta idb tb p end } -let cc_fail gls = - user_err ~hdr:"Congruence" (Pp.str "congruence failed.") +let cc_fail = + Tacticals.New.tclZEROMSG (Pp.str "congruence failed.") let congruence_tac depth l = Tacticals.New.tclORELSE (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l)) - (Proofview.V82.tactic cc_fail) + cc_fail (* Beware: reflexivity = constructor 1 = apply refl_equal might be slow now, let's rather do something equivalent @@ -492,16 +515,15 @@ let congruence_tac depth l = *) let mk_eq f c1 c2 k = - Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> - Proofview.Goal.enter { enter = begin fun gl -> + Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> let open Tacmach.New in let evm, ty = pf_apply type_of gl c1 in let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in let term = mkApp (fc, [| ty; c1; c2 |]) in let evm, _ = type_of (pf_env gl) evm term in - Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) - (k term) - end }) + Sigma.Unsafe.of_pair (k term, evm) + end } let f_equal = Proofview.Goal.enter { enter = begin fun gl -> @@ -511,7 +533,7 @@ let f_equal = try (* type_of can raise an exception *) Tacticals.New.tclTHENS (mk_eq _eq c1 c2 Tactics.cut) - [Proofview.tclUNIT ();Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)] + [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)] with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index de6eb982ee..5099d847b0 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -14,7 +14,7 @@ val proof_tac: Ccproof.proof -> unit Proofview.tactic val cc_tactic : int -> constr list -> unit Proofview.tactic -val cc_fail : tactic +val cc_fail : unit Proofview.tactic val congruence_tac : int -> constr list -> unit Proofview.tactic diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 7773f6a2fd..ade94e98e3 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -9,6 +9,7 @@ open Hipattern open Names open Term +open EConstr open Vars open Termops open Tacmach @@ -44,28 +45,27 @@ let rec nb_prod_after n c= 1+(nb_prod_after 0 b) | _ -> 0 -let construct_nhyps ind gls = +let construct_nhyps env ind = let nparams = (fst (Global.lookup_inductive (fst ind))).mind_nparams in - let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in + let constr_types = Inductiveops.arities_of_constructors env ind in let hyp = nb_prod_after nparams in Array.map hyp constr_types (* indhyps builds the array of arrays of constructor hyps for (ind largs)*) -let ind_hyps nevar ind largs gls= - let types= Inductiveops.arities_of_constructors (pf_env gls) ind in +let ind_hyps env sigma nevar ind largs = + let types= Inductiveops.arities_of_constructors env ind in let myhyps t = - let t1=Term.prod_applist t largs in - let t2=snd (decompose_prod_n_assum nevar t1) in - fst (decompose_prod_assum t2) in + let t = EConstr.of_constr t in + let t1=Termops.prod_applist sigma t largs in + let t2=snd (decompose_prod_n_assum sigma nevar t1) in + fst (decompose_prod_assum sigma t2) in Array.map myhyps types -let special_nf gl= - let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in - (fun t -> CClosure.norm_val infos (CClosure.inject t)) +let special_nf env sigma t = + Reductionops.clos_norm_flags !red_flags env sigma t -let special_whd gl= - let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in - (fun t -> CClosure.whd_val infos (CClosure.inject t)) +let special_whd env sigma t = + Reductionops.clos_whd_flags !red_flags env sigma t type kind_of_formula= Arrow of constr*constr @@ -78,20 +78,19 @@ type kind_of_formula= let pop t = Vars.lift (-1) t -let kind_of_formula gl term = - let normalize=special_nf gl in - let cciterm=special_whd gl term in - match match_with_imp_term (project gl) (EConstr.of_constr cciterm) with - Some (a,b)-> Arrow(EConstr.Unsafe.to_constr a,(pop (EConstr.Unsafe.to_constr b))) +let kind_of_formula env sigma term = + let normalize = special_nf env sigma in + let cciterm = special_whd env sigma term in + match match_with_imp_term sigma cciterm with + Some (a,b)-> Arrow (a, pop b) |_-> - match match_with_forall_term (project gl) (EConstr.of_constr cciterm) with - Some (_,a,b)-> Forall(EConstr.Unsafe.to_constr a,EConstr.Unsafe.to_constr b) + match match_with_forall_term sigma cciterm with + Some (_,a,b)-> Forall (a, b) |_-> - match match_with_nodep_ind (project gl) (EConstr.of_constr cciterm) with + match match_with_nodep_ind sigma cciterm with Some (i,l,n)-> - let l = List.map EConstr.Unsafe.to_constr l in - let ind,u=EConstr.destInd (project gl) i in - let u = EConstr.EInstance.kind (project gl) u in + let ind,u=EConstr.destInd sigma i in + let u = EConstr.EInstance.kind sigma u in let (mib,mip) = Global.lookup_inductive ind in let nconstr=Array.length mip.mind_consnames in if Int.equal nconstr 0 then @@ -100,7 +99,7 @@ let kind_of_formula gl term = let has_realargs=(n>0) in let is_trivial= let is_constant c = - Int.equal (nb_prod (project gl) (EConstr.of_constr c)) mib.mind_nparams in + Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in Array.exists is_constant mip.mind_nf_lc in if Inductiveops.mis_is_recursive (ind,mib,mip) || (has_realargs && not is_trivial) @@ -112,11 +111,11 @@ let kind_of_formula gl term = else Or((ind,u),l,is_trivial) | _ -> - match match_with_sigma_type (project gl) (EConstr.of_constr cciterm) with + match match_with_sigma_type sigma cciterm with Some (i,l)-> - let (ind, u) = EConstr.destInd (project gl) i in - let u = EConstr.EInstance.kind (project gl) u in - Exists((ind, u), List.map EConstr.Unsafe.to_constr l) + let (ind, u) = EConstr.destInd sigma i in + let u = EConstr.EInstance.kind sigma u in + Exists((ind, u), l) |_-> Atom (normalize cciterm) type atoms = {positive:constr list;negative:constr list} @@ -127,29 +126,29 @@ let no_atoms = (false,{positive=[];negative=[]}) let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *) -let build_atoms gl metagen side cciterm = +let build_atoms env sigma metagen side cciterm = let trivial =ref false and positive=ref [] and negative=ref [] in - let normalize=special_nf gl in - let rec build_rec env polarity cciterm= - match kind_of_formula gl cciterm with + let normalize=special_nf env sigma in + let rec build_rec subst polarity cciterm= + match kind_of_formula env sigma cciterm with False(_,_)->if not polarity then trivial:=true | Arrow (a,b)-> - build_rec env (not polarity) a; - build_rec env polarity b + build_rec subst (not polarity) a; + build_rec subst polarity b | And(i,l,b) | Or(i,l,b)-> if b then begin - let unsigned=normalize (substnl env 0 cciterm) in + let unsigned=normalize (substnl subst 0 cciterm) in if polarity then positive:= unsigned :: !positive else negative:= unsigned :: !negative end; - let v = ind_hyps 0 i l gl in + let v = ind_hyps env sigma 0 i l in let g i _ decl = - build_rec env polarity (lift i (RelDecl.get_type decl)) in + build_rec subst polarity (lift i (RelDecl.get_type decl)) in let f l = List.fold_left_i g (1-(List.length l)) () l in if polarity && (* we have a constant constructor *) @@ -158,16 +157,16 @@ let build_atoms gl metagen side cciterm = Array.iter f v | Exists(i,l)-> let var=mkMeta (metagen true) in - let v =(ind_hyps 1 i l gl).(0) in + let v =(ind_hyps env sigma 1 i l).(0) in let g i _ decl = - build_rec (var::env) polarity (lift i (RelDecl.get_type decl)) in + build_rec (var::subst) polarity (lift i (RelDecl.get_type decl)) in List.fold_left_i g (2-(List.length l)) () v | Forall(_,b)-> let var=mkMeta (metagen true) in - build_rec (var::env) polarity b + build_rec (var::subst) polarity b | Atom t-> - let unsigned=substnl env 0 t in - if not (isMeta unsigned) then (* discarding wildcard atoms *) + let unsigned=substnl subst 0 t in + if not (isMeta sigma unsigned) then (* discarding wildcard atoms *) if polarity then positive:= unsigned :: !positive else @@ -177,9 +176,9 @@ let build_atoms gl metagen side cciterm = Concl -> build_rec [] true cciterm | Hyp -> build_rec [] false cciterm | Hint -> - let rels,head=decompose_prod cciterm in - let env=List.rev_map (fun _->mkMeta (metagen true)) rels in - build_rec env false head;trivial:=false (* special for hints *) + let rels,head=decompose_prod sigma cciterm in + let subst=List.rev_map (fun _->mkMeta (metagen true)) rels in + build_rec subst false head;trivial:=false (* special for hints *) end; (!trivial, {positive= !positive; @@ -215,32 +214,32 @@ type t={id:global_reference; pat:(left_pattern,right_pattern) sum; atoms:atoms} -let build_formula side nam typ gl metagen= - let normalize = special_nf gl in +let build_formula env sigma side nam typ metagen= + let normalize = special_nf env sigma in try let m=meta_succ(metagen false) in let trivial,atoms= if !qflag then - build_atoms gl metagen side typ + build_atoms env sigma metagen side typ else no_atoms in let pattern= match side with Concl -> let pat= - match kind_of_formula gl typ with + match kind_of_formula env sigma typ with False(_,_) -> Rfalse | Atom a -> raise (Is_atom a) | And(_,_,_) -> Rand | Or(_,_,_) -> Ror | Exists (i,l) -> - let d = RelDecl.get_type (List.last (ind_hyps 0 i l gl).(0)) in + let d = RelDecl.get_type (List.last (ind_hyps env sigma 0 i l).(0)) in Rexists(m,d,trivial) | Forall (_,a) -> Rforall | Arrow (a,b) -> Rarrow in Right pat | _ -> let pat= - match kind_of_formula gl typ with + match kind_of_formula env sigma typ with False(i,_) -> Lfalse | Atom a -> raise (Is_atom a) | And(i,_,b) -> @@ -257,7 +256,7 @@ let build_formula side nam typ gl metagen= | Arrow (a,b) -> let nfa=normalize a in LA (nfa, - match kind_of_formula gl a with + match kind_of_formula env sigma a with False(i,l)-> LLfalse(i,l) | Atom t-> LLatom | And(i,l,_)-> LLand(i,l) diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 5db8ff59ad..3f438c04a0 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -7,6 +7,7 @@ (************************************************************************) open Term +open EConstr open Globnames val qflag : bool ref @@ -23,10 +24,10 @@ type ('a,'b) sum = Left of 'a | Right of 'b type counter = bool -> metavariable -val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array +val construct_nhyps : Environ.env -> pinductive -> int array -val ind_hyps : int -> pinductive -> constr list -> - Proof_type.goal Tacmach.sigma -> Context.Rel.t array +val ind_hyps : Environ.env -> Evd.evar_map -> int -> pinductive -> + constr list -> EConstr.rel_context array type atoms = {positive:constr list;negative:constr list} @@ -34,7 +35,7 @@ type side = Hyp | Concl | Hint val dummy_id: global_reference -val build_atoms : Proof_type.goal Tacmach.sigma -> counter -> +val build_atoms : Environ.env -> Evd.evar_map -> counter -> side -> constr -> bool * atoms type right_pattern = @@ -69,6 +70,6 @@ type t={id: global_reference; (*exception Is_atom of constr*) -val build_formula : side -> global_reference -> types -> - Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum +val build_formula : Environ.env -> Evd.evar_map -> side -> global_reference -> types -> + counter -> (t,types) sum diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 3c03193196..8ef6a09d0e 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -13,7 +13,9 @@ open Formula open Sequent open Ground open Goptions -open Tacticals +open Tacmach.New +open Tacticals.New +open Proofview.Notations open Tacinterp open Libnames open Stdarg @@ -81,21 +83,29 @@ END let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") -let gen_ground_tac flag taco ids bases gl= +let gen_ground_tac flag taco ids bases = let backup= !qflag in - try + Proofview.tclOR begin + Proofview.Goal.enter { enter = begin fun gl -> qflag:=flag; let solver= match taco with Some tac-> tac | None-> snd (default_solver ()) in - let startseq gl= + let startseq k = + Proofview.Goal.s_enter { s_enter = begin fun gl -> let seq=empty_seq !ground_depth in - let seq,gl = extend_with_ref_list ids seq gl in - extend_with_auto_hints bases seq gl in - let result=ground_tac (Proofview.V82.of_tactic solver) startseq gl in - qflag:=backup;result - with reraise -> qflag:=backup;raise reraise + let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in + let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in + Sigma.Unsafe.of_pair (k seq, sigma) + end } + in + let result=ground_tac solver startseq in + qflag := backup; + result + end } + end + (fun (e, info) -> qflag := backup; Proofview.tclZERO ~info e) (* special for compatibility with Intuition @@ -144,18 +154,15 @@ END TACTIC EXTEND firstorder [ "firstorder" tactic_opt(t) firstorder_using(l) ] -> - [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l []) ] + [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l [] ] | [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> - [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l) ] + [ gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l ] | [ "firstorder" tactic_opt(t) firstorder_using(l) "with" ne_preident_list(l') ] -> - [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l l') ] + [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l l' ] END TACTIC EXTEND gintuition [ "gintuition" tactic_opt(t) ] -> - [ Proofview.V82.tactic (gen_ground_tac false (Option.map (tactic_of_value ist) t) [] []) ] + [ gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] ] END - -open Proofview.Notations -open Cc_plugin diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index d6cd7e2a08..ab1dd07c11 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -12,8 +12,9 @@ open Sequent open Rules open Instances open Term -open Tacmach -open Tacticals +open Tacmach.New +open Tacticals.New +open Proofview.Notations let update_flags ()= let predref=ref Names.Cpred.empty in @@ -29,18 +30,24 @@ let update_flags ()= CClosure.betaiotazeta (Names.Id.Pred.full,Names.Cpred.complement !predref) -let ground_tac solver startseq gl= +let ground_tac solver startseq = + Proofview.Goal.enter { enter = begin fun gl -> update_flags (); - let rec toptac skipped seq gl= - if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 - then Feedback.msg_debug (Printer.pr_goal gl); + let rec toptac skipped seq = + Proofview.Goal.enter { enter = begin fun gl -> + let () = + if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 + then + let gl = { Evd.it = Proofview.Goal.goal (Proofview.Goal.assume gl); sigma = project gl } in + Feedback.msg_debug (Printer.pr_goal gl) + in tclORELSE (axiom_tac seq.gl seq) begin try - let (hd,seq1)=take_formula seq - and re_add s=re_add_formula_list skipped s in + let (hd,seq1)=take_formula (project gl) seq + and re_add s=re_add_formula_list (project gl) skipped s in let continue=toptac [] - and backtrack gl=toptac (hd::skipped) seq1 gl in + and backtrack =toptac (hd::skipped) seq1 in match hd.pat with Right rpat-> begin @@ -60,7 +67,7 @@ let ground_tac solver startseq gl= or_tac backtrack continue (re_add seq1) | Rfalse->backtrack | Rexists(i,dom,triv)-> - let (lfp,seq2)=collect_quantified seq in + let (lfp,seq2)=collect_quantified (project gl) seq in let backtrack2=toptac (lfp@skipped) seq2 in if !qflag && seq.depth>0 then quantified_tac lfp backtrack2 @@ -80,7 +87,7 @@ let ground_tac solver startseq gl= left_or_tac ind backtrack hd.id continue (re_add seq1) | Lforall (_,_,_)-> - let (lfp,seq2)=collect_quantified seq in + let (lfp,seq2)=collect_quantified (project gl) seq in let backtrack2=toptac (lfp@skipped) seq2 in if !qflag && seq.depth>0 then quantified_tac lfp backtrack2 @@ -119,7 +126,8 @@ let ground_tac solver startseq gl= ll_atom_tac typ la_tac hd.id continue (re_add seq1) end with Heap.EmptyHeap->solver - end gl in - let seq, gl' = startseq gl in - wrap (List.length (pf_hyps gl)) true (toptac []) seq gl' - + end + end } in + let n = List.length (Proofview.Goal.hyps gl) in + startseq (fun seq -> wrap n true (toptac []) seq) + end } diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli index b5669463cd..4fd1e38a27 100644 --- a/plugins/firstorder/ground.mli +++ b/plugins/firstorder/ground.mli @@ -6,6 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -val ground_tac: Tacmach.tactic -> - (Proof_type.goal Tacmach.sigma -> Sequent.t * Proof_type.goal Tacmach.sigma) -> Tacmach.tactic +val ground_tac: unit Proofview.tactic -> + ((Sequent.t -> unit Proofview.tactic) -> unit Proofview.tactic) -> unit Proofview.tactic diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 9dc2a51a61..62f811546d 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -11,10 +11,12 @@ open Rules open CErrors open Util open Term +open EConstr open Vars -open Tacmach +open Tacmach.New open Tactics -open Tacticals +open Tacticals.New +open Proofview.Notations open Termops open Reductionops open Formula @@ -25,11 +27,12 @@ open Sigma.Notations open Context.Rel.Declaration let compare_instance inst1 inst2= + let cmp c1 c2 = OrderedConstr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in match inst1,inst2 with Phantom(d1),Phantom(d2)-> - (OrderedConstr.compare d1 d2) + (cmp d1 d2) | Real((m1,c1),n1),Real((m2,c2),n2)-> - ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2 + ((-) =? (-) ==? cmp) m2 m1 n1 n2 c1 c2 | Phantom(_),Real((m,_),_)-> if Int.equal m 0 then -1 else 1 | Real((m,_),_),Phantom(_)-> if Int.equal m 0 then 1 else -1 @@ -56,12 +59,12 @@ let make_simple_atoms seq= | None->[] in {negative=seq.latoms;positive=ratoms} -let do_sequent setref triv id seq i dom atoms= +let do_sequent sigma setref triv id seq i dom atoms= let flag=ref true in let phref=ref triv in let do_atoms a1 a2 = let do_pair t1 t2 = - match unif_atoms i dom t1 t2 with + match unif_atoms sigma i dom t1 t2 with None->() | Some (Phantom _) ->phref:=true | Some c ->flag:=false;setref:=IS.add (c,id) !setref in @@ -71,26 +74,26 @@ let do_sequent setref triv id seq i dom atoms= do_atoms atoms (make_simple_atoms seq); !flag && !phref -let match_one_quantified_hyp setref seq lf= +let match_one_quantified_hyp sigma setref seq lf= match lf.pat with Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))-> - if do_sequent setref triv lf.id seq i dom lf.atoms then + if do_sequent sigma setref triv lf.id seq i dom lf.atoms then setref:=IS.add ((Phantom dom),lf.id) !setref | _ -> anomaly (Pp.str "can't happen") -let give_instances lf seq= +let give_instances sigma lf seq= let setref=ref IS.empty in - List.iter (match_one_quantified_hyp setref seq) lf; + List.iter (match_one_quantified_hyp sigma setref seq) lf; IS.elements !setref (* collector for the engine *) -let rec collect_quantified seq= +let rec collect_quantified sigma seq= try - let hd,seq1=take_formula seq in + let hd,seq1=take_formula sigma seq in (match hd.pat with Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) -> - let (q,seq2)=collect_quantified seq1 in + let (q,seq2)=collect_quantified sigma seq1 in ((hd::q),seq2) | _->[],seq) with Heap.EmptyHeap -> [],seq @@ -99,60 +102,61 @@ let rec collect_quantified seq= let dummy_bvid=Id.of_string "x" -let mk_open_instance id idc gl m t= - let env=pf_env gl in - let evmap=Refiner.project gl in +let mk_open_instance env evmap id idc m t = let var_id= if id==dummy_id then dummy_bvid else - let typ=pf_unsafe_type_of gl idc in + let typ=Typing.unsafe_type_of env evmap idc in (* since we know we will get a product, reduction is not too expensive *) - let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap typ)) in + let (nam,_,_)=destProd evmap (whd_all env evmap typ) in match nam with Name id -> id | Anonymous -> dummy_bvid in let revt=substl (List.init m (fun i->mkRel (m-i))) t in let rec aux n avoid env evmap decls = if Int.equal n 0 then evmap, decls else - let nid=(fresh_id avoid var_id gl) in + let nid=(fresh_id_in_env avoid var_id env) in let evmap = Sigma.Unsafe.of_evar_map evmap in let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in let evmap = Sigma.to_evar_map evmap in let decl = LocalAssum (Name nid, c) in aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in let evmap, decls = aux m [] env evmap [] in - evmap, decls, revt + (evmap, decls, revt) (* tactics *) let left_instance_tac (inst,id) continue seq= let open EConstr in + Proofview.Goal.enter { enter = begin fun gl -> + let sigma = project gl in match inst with Phantom dom-> - if lookup (id,None) seq then + if lookup sigma (id,None) seq then tclFAIL 0 (Pp.str "already done") else - tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom))) + tclTHENS (cut dom) [tclTHENLIST - [Proofview.V82.of_tactic introf; - pf_constr_of_global id (fun idc -> - (fun gls-> Proofview.V82.of_tactic (generalize - [mkApp(idc, - [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls)); - Proofview.V82.of_tactic introf; + [introf; + (pf_constr_of_global id >>= fun idc -> + Proofview.Goal.enter { enter = begin fun gl -> + let id0 = List.nth (pf_ids_of_hyps gl) 0 in + generalize [mkApp(idc, [|mkVar id0|])] + end }); + introf; tclSOLVE [wrap 1 false continue (deepen (record (id,None) seq))]]; - tclTRY (Proofview.V82.of_tactic assumption)] - | Real((m,t) as c,_)-> - if lookup (id,Some c) seq then + tclTRY assumption] + | Real((m,t),_)-> + let c = (m, EConstr.to_constr sigma t) in + if lookup sigma (id,Some c) seq then tclFAIL 0 (Pp.str "already done") else let special_generalize= if m>0 then - pf_constr_of_global id (fun idc -> - fun gl-> - let evmap,rc,ot = mk_open_instance id idc gl m t in - let ot = EConstr.of_constr ot in + (pf_constr_of_global id >>= fun idc -> + Proofview.Goal.s_enter { s_enter = begin fun gl-> + let (evmap, rc, ot) = mk_open_instance (pf_env gl) (project gl) id idc m t in let gt= it_mkLambda_or_LetIn (mkApp(idc,[|ot|])) rc in @@ -160,34 +164,38 @@ let left_instance_tac (inst,id) continue seq= try Typing.type_of (pf_env gl) evmap gt with e when CErrors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in - tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl) + Sigma.Unsafe.of_pair (generalize [gt], evmap) + end }) else - let t = EConstr.of_constr t in - pf_constr_of_global id (fun idc -> - Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])])) + pf_constr_of_global id >>= fun idc -> generalize [mkApp(idc,[|t|])] in tclTHENLIST [special_generalize; - Proofview.V82.of_tactic introf; + introf; tclSOLVE [wrap 1 false continue (deepen (record (id,Some c) seq))]] + end } let right_instance_tac inst continue seq= + let open EConstr in + Proofview.Goal.enter { enter = begin fun gl -> match inst with Phantom dom -> - tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom))) + tclTHENS (cut dom) [tclTHENLIST - [Proofview.V82.of_tactic introf; - (fun gls-> - Proofview.V82.of_tactic (split (ImplicitBindings - [EConstr.mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls); + [introf; + Proofview.Goal.enter { enter = begin fun gl -> + let id0 = List.nth (pf_ids_of_hyps gl) 0 in + split (ImplicitBindings [mkVar id0]) + end }; tclSOLVE [wrap 0 true continue (deepen seq)]]; - tclTRY (Proofview.V82.of_tactic assumption)] + tclTRY assumption] | Real ((0,t),_) -> - (tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr t]))) + (tclTHEN (split (ImplicitBindings [t])) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") + end } let instance_tac inst= if (snd inst)==dummy_id then @@ -195,10 +203,10 @@ let instance_tac inst= else left_instance_tac inst -let quantified_tac lf backtrack continue seq gl= - let insts=give_instances lf seq in +let quantified_tac lf backtrack continue seq = + Proofview.Goal.enter { enter = begin fun gl -> + let insts=give_instances (project gl) lf seq in tclORELSE (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts)) - backtrack gl - - + backtrack + end } diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index ce711f3f97..47550f314e 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -9,9 +9,9 @@ open Globnames open Rules -val collect_quantified : Sequent.t -> Formula.t list * Sequent.t +val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.t list * Sequent.t -val give_instances : Formula.t list -> Sequent.t -> +val give_instances : Evd.evar_map -> Formula.t list -> Sequent.t -> (Unify.instance * global_reference) list val quantified_tac : Formula.t list -> seqtac with_backtracking diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index a60fd4d8f1..e0d2c38a73 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -10,10 +10,12 @@ open CErrors open Util open Names open Term +open EConstr open Vars -open Tacmach +open Tacmach.New open Tactics -open Tacticals +open Tacticals.New +open Proofview.Notations open Termops open Formula open Sequent @@ -22,148 +24,165 @@ open Locus module NamedDecl = Context.Named.Declaration +type tactic = unit Proofview.tactic + type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic type lseqtac= global_reference -> seqtac type 'a with_backtracking = tactic -> 'a -let wrap n b continue seq gls= +let wrap n b continue seq = + Proofview.Goal.nf_enter { enter = begin fun gls -> Control.check_for_interrupt (); - let nc=pf_hyps gls in + let nc = Proofview.Goal.hyps gls in let env=pf_env gls in + let sigma = project gls in let rec aux i nc ctx= if i<=0 then seq else match nc with []->anomaly (Pp.str "Not the expected number of hyps") | nd::q-> let id = NamedDecl.get_id nd in - if occur_var env (project gls) id (pf_concl gls) || - List.exists (occur_var_in_decl env (project gls) id) ctx then + if occur_var env sigma id (pf_concl gls) || + List.exists (occur_var_in_decl env sigma id) ctx then (aux (i-1) q (nd::ctx)) else - add_formula Hyp (VarRef id) (EConstr.Unsafe.to_constr (NamedDecl.get_type nd)) (aux (i-1) q (nd::ctx)) gls in + add_formula env sigma Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) in let seq1=aux n nc [] in let seq2=if b then - add_formula Concl dummy_id (EConstr.Unsafe.to_constr (pf_concl gls)) seq1 gls else seq1 in - continue seq2 gls + add_formula env sigma Concl dummy_id (pf_concl gls) seq1 else seq1 in + continue seq2 + end } let basename_of_global=function VarRef id->id | _->assert false let clear_global=function - VarRef id-> Proofview.V82.of_tactic (clear [id]) + VarRef id-> clear [id] | _->tclIDTAC (* connection rules *) -let axiom_tac t seq= - try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c)) - with Not_found->tclFAIL 0 (Pp.str "No axiom link") +let axiom_tac t seq = + Proofview.Goal.enter { enter = begin fun gl -> + try + pf_constr_of_global (find_left (project gl) t seq) >>= fun c -> + exact_no_check c + with Not_found -> tclFAIL 0 (Pp.str "No axiom link") + end } -let ll_atom_tac a backtrack id continue seq= +let ll_atom_tac a backtrack id continue seq = let open EConstr in tclIFTHENELSE - (try - tclTHENLIST - [pf_constr_of_global (find_left a seq) (fun left -> - pf_constr_of_global id (fun id -> - Proofview.V82.of_tactic (generalize [(mkApp(id, [|left|]))]))); + (tclTHENLIST + [(Proofview.tclEVARMAP >>= fun sigma -> + let gr = + try Proofview.tclUNIT (find_left sigma a seq) + with Not_found -> tclFAIL 0 (Pp.str "No link") + in + gr >>= fun gr -> + pf_constr_of_global gr >>= fun left -> + pf_constr_of_global id >>= fun id -> + generalize [(mkApp(id, [|left|]))]); clear_global id; - Proofview.V82.of_tactic intro] - with Not_found->tclFAIL 0 (Pp.str "No link")) + intro]) (wrap 1 false continue seq) backtrack (* right connectives rules *) let and_tac backtrack continue seq= - tclIFTHENELSE (Proofview.V82.of_tactic simplest_split) (wrap 0 true continue seq) backtrack + tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack let or_tac backtrack continue seq= tclORELSE - (Proofview.V82.of_tactic (any_constructor false (Some (Proofview.V82.tactic (tclCOMPLETE (wrap 0 true continue seq)))))) + (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq)))) backtrack let arrow_tac backtrack continue seq= - tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 1 true continue seq) + tclIFTHENELSE intro (wrap 1 true continue seq) (tclORELSE - (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 1 true continue seq))) + (tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq))) backtrack) (* left connectives rules *) -let left_and_tac ind backtrack id continue seq gls= - let n=(construct_nhyps ind gls).(0) in +let left_and_tac ind backtrack id continue seq = + Proofview.Goal.enter { enter = begin fun gl -> + let n=(construct_nhyps (pf_env gl) ind).(0) in tclIFTHENELSE (tclTHENLIST - [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim); + [(pf_constr_of_global id >>= simplest_elim); clear_global id; - tclDO n (Proofview.V82.of_tactic intro)]) + tclDO n intro]) (wrap n false continue seq) - backtrack gls + backtrack + end } -let left_or_tac ind backtrack id continue seq gls= - let v=construct_nhyps ind gls in +let left_or_tac ind backtrack id continue seq = + Proofview.Goal.enter { enter = begin fun gl -> + let v=construct_nhyps (pf_env gl) ind in let f n= tclTHENLIST [clear_global id; - tclDO n (Proofview.V82.of_tactic intro); + tclDO n intro; wrap n false continue seq] in tclIFTHENSVELSE - (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)) + (pf_constr_of_global id >>= simplest_elim) (Array.map f v) - backtrack gls + backtrack + end } let left_false_tac id= - Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim) + Tacticals.New.pf_constr_of_global id >>= simplest_elim (* left arrow connective rules *) (* We use this function for false, and, or, exists *) -let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl= - let rcs=ind_hyps 0 indu largs gl in +let ll_ind_tac (ind,u as indu) largs backtrack id continue seq = + Proofview.Goal.enter { enter = begin fun gl -> + let rcs=ind_hyps (pf_env gl) (project gl) 0 indu largs in let vargs=Array.of_list largs in (* construire le terme H->B, le generaliser etc *) let myterm idc i= let rc=rcs.(i) in let p=List.length rc in + let u = EInstance.make u in let cstr=mkApp ((mkConstructU ((ind,(i+1)),u)),vargs) in let vars=Array.init p (fun j->mkRel (p-j)) in let capply=mkApp ((lift p cstr),vars) in let head=mkApp ((lift p idc),[|capply|]) in - EConstr.of_constr (it_mkLambda_or_LetIn head rc) in + EConstr.it_mkLambda_or_LetIn head rc in let lp=Array.length rcs in - let newhyps idc =List.init lp (myterm (EConstr.Unsafe.to_constr idc)) in + let newhyps idc =List.init lp (myterm idc) in tclIFTHENELSE (tclTHENLIST - [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc))); + [(pf_constr_of_global id >>= fun idc -> generalize (newhyps idc)); clear_global id; - tclDO lp (Proofview.V82.of_tactic intro)]) - (wrap lp false continue seq) backtrack gl + tclDO lp intro]) + (wrap lp false continue seq) backtrack + end } let ll_arrow_tac a b c backtrack id continue seq= let open EConstr in let open Vars in - let a = EConstr.of_constr a in - let b = EConstr.of_constr b in - let c = EConstr.of_constr c in let cc=mkProd(Anonymous,a,(lift 1 b)) in let d idc = mkLambda (Anonymous,b, mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in tclORELSE - (tclTHENS (Proofview.V82.of_tactic (cut c)) + (tclTHENS (cut c) [tclTHENLIST - [Proofview.V82.of_tactic introf; + [introf; clear_global id; wrap 1 false continue seq]; - tclTHENS (Proofview.V82.of_tactic (cut cc)) - [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c)); + tclTHENS (cut cc) + [(pf_constr_of_global id >>= fun c -> exact_no_check c); tclTHENLIST - [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc])); + [(pf_constr_of_global id >>= fun idc -> generalize [d idc]); clear_global id; - Proofview.V82.of_tactic introf; - Proofview.V82.of_tactic introf; + introf; + introf; tclCOMPLETE (wrap 2 true continue seq)]]]) backtrack @@ -171,38 +190,40 @@ let ll_arrow_tac a b c backtrack id continue seq= let forall_tac backtrack continue seq= tclORELSE - (tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 0 true continue seq) + (tclIFTHENELSE intro (wrap 0 true continue seq) (tclORELSE - (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 0 true continue seq))) + (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq))) backtrack)) (if !qflag then tclFAIL 0 (Pp.str "reversible in 1st order mode") else backtrack) -let left_exists_tac ind backtrack id continue seq gls= - let n=(construct_nhyps ind gls).(0) in +let left_exists_tac ind backtrack id continue seq = + Proofview.Goal.enter { enter = begin fun gl -> + let n=(construct_nhyps (pf_env gl) ind).(0) in tclIFTHENELSE - (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)) + (Tacticals.New.pf_constr_of_global id >>= simplest_elim) (tclTHENLIST [clear_global id; - tclDO n (Proofview.V82.of_tactic intro); + tclDO n intro; (wrap (n-1) false continue seq)]) backtrack - gls + end } let ll_forall_tac prod backtrack id continue seq= tclORELSE - (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr prod))) + (tclTHENS (cut prod) [tclTHENLIST - [Proofview.V82.of_tactic intro; - pf_constr_of_global id (fun idc -> - (fun gls-> + [intro; + (pf_constr_of_global id >>= fun idc -> + Proofview.Goal.enter { enter = begin fun gls-> let open EConstr in - let id0=pf_nth_hyp_id gls 1 in + let id0 = List.nth (pf_ids_of_hyps gls) 0 in let term=mkApp(idc,[|mkVar(id0)|]) in - tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls)); + tclTHEN (generalize [term]) (clear [id0]) + end }); clear_global id; - Proofview.V82.of_tactic intro; + intro; tclCOMPLETE (wrap 1 false continue (deepen seq))]; tclCOMPLETE (wrap 0 true continue (deepen seq))]) backtrack @@ -214,12 +235,13 @@ let ll_forall_tac prod backtrack id continue seq= let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str let defined_connectives=lazy - [AllOccurrences,EvalConstRef (fst (destConst (constant "not"))); - AllOccurrences,EvalConstRef (fst (destConst (constant "iff")))] + [AllOccurrences,EvalConstRef (fst (Term.destConst (constant "not"))); + AllOccurrences,EvalConstRef (fst (Term.destConst (constant "iff")))] let normalize_evaluables= - onAllHypsAndConcl - (function - None-> Proofview.V82.of_tactic (unfold_in_concl (Lazy.force defined_connectives)) - | Some id -> - Proofview.V82.of_tactic (unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))) + Proofview.Goal.enter { enter = begin fun gl -> + unfold_in_concl (Lazy.force defined_connectives) <*> + tclMAP + (fun id -> unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)) + (pf_ids_of_hyps gl) + end } diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index 381b7cd87c..80a7ae2c25 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -7,10 +7,13 @@ (************************************************************************) open Term +open EConstr open Tacmach open Names open Globnames +type tactic = unit Proofview.tactic + type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic type lseqtac= global_reference -> seqtac diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index fb0c22c2b7..59b842c825 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -7,6 +7,7 @@ (************************************************************************) open Term +open EConstr open CErrors open Util open Formula @@ -57,11 +58,11 @@ end module OrderedConstr= struct - type t=constr + type t=Constr.t let compare=constr_ord end -type h_item = global_reference * (int*constr) option +type h_item = global_reference * (int*Constr.t) option module Hitem= struct @@ -81,13 +82,15 @@ module CM=Map.Make(OrderedConstr) module History=Set.Make(Hitem) -let cm_add typ nam cm= +let cm_add sigma typ nam cm= + let typ = EConstr.to_constr sigma typ in try let l=CM.find typ cm in CM.add typ (nam::l) cm with Not_found->CM.add typ [nam] cm -let cm_remove typ nam cm= +let cm_remove sigma typ nam cm= + let typ = EConstr.to_constr sigma typ in try let l=CM.find typ cm in let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in @@ -112,19 +115,19 @@ let deepen seq={seq with depth=seq.depth-1} let record item seq={seq with history=History.add item seq.history} -let lookup item seq= +let lookup sigma item seq= History.mem item seq.history || match item with (_,None)->false - | (id,Some ((m,t) as c))-> + | (id,Some (m, t))-> let p (id2,o)= match o with None -> false - | Some ((m2,t2) as c2)-> Globnames.eq_gr id id2 && m2>m && more_general c2 c in + | Some (m2, t2)-> Globnames.eq_gr id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in History.exists p seq.history -let add_formula side nam t seq gl= - match build_formula side nam t gl seq.cnt with +let add_formula env sigma side nam t seq = + match build_formula env sigma side nam t seq.cnt with Left f-> begin match side with @@ -136,7 +139,7 @@ let add_formula side nam t seq gl= | _ -> {seq with redexes=HP.add f seq.redexes; - context=cm_add f.constr nam seq.context} + context=cm_add sigma f.constr nam seq.context} end | Right t-> match side with @@ -144,18 +147,18 @@ let add_formula side nam t seq gl= {seq with gl=t;glatom=Some t} | _ -> {seq with - context=cm_add t nam seq.context; + context=cm_add sigma t nam seq.context; latoms=t::seq.latoms} -let re_add_formula_list lf seq= +let re_add_formula_list sigma lf seq= let do_one f cm= if f.id == dummy_id then cm - else cm_add f.constr f.id cm in + else cm_add sigma f.constr f.id cm in {seq with redexes=List.fold_right HP.add lf seq.redexes; context=List.fold_right do_one lf seq.context} -let find_left t seq=List.hd (CM.find t seq.context) +let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr sigma t) seq.context) (*let rev_left seq= try @@ -164,7 +167,7 @@ let find_left t seq=List.hd (CM.find t seq.context) with Heap.EmptyHeap -> false *) -let rec take_formula seq= +let rec take_formula sigma seq= let hd=HP.maximum seq.redexes and hp=HP.remove seq.redexes in if hd.id == dummy_id then @@ -172,11 +175,11 @@ let rec take_formula seq= if seq.gl==hd.constr then hd,nseq else - take_formula nseq (* discarding deprecated goal *) + take_formula sigma nseq (* discarding deprecated goal *) else hd,{seq with redexes=hp; - context=cm_remove hd.constr hd.id seq.context} + context=cm_remove sigma hd.constr hd.id seq.context} let empty_seq depth= {redexes=HP.empty; @@ -196,18 +199,17 @@ let expand_constructor_hints = | gr -> [gr]) -let extend_with_ref_list l seq gl = +let extend_with_ref_list env sigma l seq = let l = expand_constructor_hints l in - let f gr (seq,gl) = - let gl, c = pf_eapply Evd.fresh_global gl gr in - let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in - let typ = EConstr.Unsafe.to_constr typ in - (add_formula Hyp gr typ seq gl,gl) in - List.fold_right f l (seq,gl) + let f gr (seq, sigma) = + let sigma, c = Evd.fresh_global env sigma gr in + let sigma, typ= Typing.type_of env sigma (EConstr.of_constr c) in + (add_formula env sigma Hyp gr typ seq, sigma) in + List.fold_right f l (seq, sigma) open Hints -let extend_with_auto_hints l seq gl= +let extend_with_auto_hints env sigma l seq = let seqref=ref seq in let f p_a_t = match repr_hint p_a_t.code with @@ -215,10 +217,9 @@ let extend_with_auto_hints l seq gl= | Res_pf_THEN_trivial_fail (c,_) -> let (c, _, _) = c in (try - let (gr, _) = Termops.global_of_constr (project gl) c in - let typ=(pf_unsafe_type_of gl c) in - let typ = EConstr.Unsafe.to_constr typ in - seqref:=add_formula Hint gr typ !seqref gl + let (gr, _) = Termops.global_of_constr sigma c in + let typ=(Typing.unsafe_type_of env sigma c) in + seqref:=add_formula env sigma Hint gr typ !seqref with Not_found->()) | _-> () in let g _ _ l = List.iter f l in @@ -230,7 +231,7 @@ let extend_with_auto_hints l seq gl= error ("Firstorder: "^dbname^" : No such Hint database") in Hint_db.iter g hdb in List.iter h l; - !seqref, gl (*FIXME: forgetting about universes*) + !seqref, sigma (*FIXME: forgetting about universes*) let print_cmap map= let print_entry c l s= diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 06c9251e7b..18d68f54f9 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -7,22 +7,23 @@ (************************************************************************) open Term +open EConstr open Formula open Tacmach open Globnames -module OrderedConstr: Set.OrderedType with type t=constr +module OrderedConstr: Set.OrderedType with type t=Constr.t -module CM: CSig.MapS with type key=constr +module CM: CSig.MapS with type key=Constr.t -type h_item = global_reference * (int*constr) option +type h_item = global_reference * (int*Constr.t) option module History: Set.S with type elt = h_item -val cm_add : constr -> global_reference -> global_reference list CM.t -> +val cm_add : Evd.evar_map -> constr -> global_reference -> global_reference list CM.t -> global_reference list CM.t -val cm_remove : constr -> global_reference -> global_reference list CM.t -> +val cm_remove : Evd.evar_map -> constr -> global_reference -> global_reference list CM.t -> global_reference list CM.t module HP: Heap.S with type elt=Formula.t @@ -40,23 +41,22 @@ val deepen: t -> t val record: h_item -> t -> t -val lookup: h_item -> t -> bool +val lookup: Evd.evar_map -> h_item -> t -> bool -val add_formula : side -> global_reference -> constr -> t -> - Proof_type.goal sigma -> t +val add_formula : Environ.env -> Evd.evar_map -> side -> global_reference -> constr -> t -> t -val re_add_formula_list : Formula.t list -> t -> t +val re_add_formula_list : Evd.evar_map -> Formula.t list -> t -> t -val find_left : constr -> t -> global_reference +val find_left : Evd.evar_map -> constr -> t -> global_reference -val take_formula : t -> Formula.t * t +val take_formula : Evd.evar_map -> t -> Formula.t * t val empty_seq : int -> t -val extend_with_ref_list : global_reference list -> - t -> Proof_type.goal sigma -> t * Proof_type.goal sigma +val extend_with_ref_list : Environ.env -> Evd.evar_map -> global_reference list -> + t -> t * Evd.evar_map -val extend_with_auto_hints : Hints.hint_db_name list -> - t -> Proof_type.goal sigma -> t * Proof_type.goal sigma +val extend_with_auto_hints : Environ.env -> Evd.evar_map -> Hints.hint_db_name list -> + t -> t * Evd.evar_map val print_cmap: global_reference list CM.t -> Pp.std_ppcmds diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 7cbfb8e7de..49bf07155f 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -8,6 +8,7 @@ open Util open Term +open EConstr open Vars open Termops open Reductionops @@ -21,13 +22,12 @@ exception UFAIL of constr*constr to the equation set. Raises UFAIL with a pair of terms *) -let strip_outer_cast t = - EConstr.Unsafe.to_constr (strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *) - let pop t = Vars.lift (-1) t +let subst_meta subst t = + let subst = List.map (fun (m, c) -> (m, EConstr.Unsafe.to_constr c)) subst in + EConstr.of_constr (subst_meta subst (EConstr.Unsafe.to_constr t)) -let unif t1 t2= - let evd = Evd.empty in (** FIXME *) +let unif evd t1 t2= let bige=Queue.create () and sigma=ref [] in let bind i t= @@ -35,7 +35,7 @@ let unif t1 t2= (List.map (function (n,tn)->(n,subst_meta [i,t] tn)) !sigma) in let rec head_reduce t= (* forbids non-sigma-normal meta in head position*) - match kind_of_term t with + match EConstr.kind evd t with Meta i-> (try head_reduce (Int.List.assoc i !sigma) @@ -44,25 +44,25 @@ let unif t1 t2= Queue.add (t1,t2) bige; try while true do let t1,t2=Queue.take bige in - let nt1=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t1))) - and nt2=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t2))) in - match (kind_of_term nt1),(kind_of_term nt2) with + let nt1=head_reduce (whd_betaiotazeta evd t1) + and nt2=head_reduce (whd_betaiotazeta evd t2) in + match (EConstr.kind evd nt1),(EConstr.kind evd nt2) with Meta i,Meta j-> if not (Int.equal i j) then if i<j then bind j nt1 else bind i nt2 | Meta i,_ -> let t=subst_meta !sigma nt2 in - if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) && - not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then + if Int.Set.is_empty (free_rels evd t) && + not (occur_term evd (EConstr.mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) | _,Meta i -> let t=subst_meta !sigma nt1 in - if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) && - not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then + if Int.Set.is_empty (free_rels evd t) && + not (occur_term evd (EConstr.mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) - | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige - | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige + | Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige + | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> Queue.add (a,c) bige;Queue.add (pop b,pop d) bige | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> @@ -84,19 +84,19 @@ let unif t1 t2= for i=0 to l-1 do Queue.add (va.(i),vb.(i)) bige done - | _->if not (eq_constr_nounivs nt1 nt2) then raise (UFAIL (nt1,nt2)) + | _->if not (eq_constr_nounivs evd nt1 nt2) then raise (UFAIL (nt1,nt2)) done; assert false (* this place is unreachable but needed for the sake of typing *) with Queue.Empty-> !sigma -let value i t= +let value evd i t= let add x y= if x<0 then y else if y<0 then x else x+y in let rec vaux term= - if isMeta term && Int.equal (destMeta term) i then 0 else + if isMeta evd term && Int.equal (destMeta evd term) i then 0 else let f v t=add v (vaux t) in - let vr=fold_constr f (-1) term in + let vr=EConstr.fold evd f (-1) term in if vr<0 then -1 else vr+1 in vaux t @@ -104,11 +104,11 @@ type instance= Real of (int*constr)*int | Phantom of constr -let mk_rel_inst t= +let mk_rel_inst evd t= let new_rel=ref 1 in let rel_env=ref [] in let rec renum_rec d t= - match kind_of_term t with + match EConstr.kind evd t with Meta n-> (try mkRel (d+(Int.List.assoc n !rel_env)) @@ -117,15 +117,15 @@ let mk_rel_inst t= incr new_rel; rel_env:=(n,m) :: !rel_env; mkRel (m+d)) - | _ -> map_constr_with_binders succ renum_rec d t + | _ -> EConstr.map_with_binders evd succ renum_rec d t in let nt=renum_rec 0 t in (!new_rel - 1,nt) -let unif_atoms i dom t1 t2= +let unif_atoms evd i dom t1 t2= try - let t=Int.List.assoc i (unif t1 t2) in - if isMeta t then Some (Phantom dom) - else Some (Real(mk_rel_inst t,value i t1)) + let t=Int.List.assoc i (unif evd t1 t2) in + if isMeta evd t then Some (Phantom dom) + else Some (Real(mk_rel_inst evd t,value evd i t1)) with UFAIL(_,_) ->None | Not_found ->Some (Phantom dom) @@ -134,11 +134,11 @@ let renum_metas_from k n t= (* requires n = max (free_rels t) *) let l=List.init n (fun i->mkMeta (k+i)) in substl l t -let more_general (m1,t1) (m2,t2)= +let more_general evd (m1,t1) (m2,t2)= let mt1=renum_metas_from 0 m1 t1 and mt2=renum_metas_from m1 m2 t2 in try - let sigma=unif mt1 mt2 in - let p (n,t)= n<m1 || isMeta t in + let sigma=unif evd mt1 mt2 in + let p (n,t)= n<m1 || isMeta evd t in List.for_all p sigma with UFAIL(_,_)->false diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli index 4fe9ad38d8..c9cca9bd8d 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -7,15 +7,16 @@ (************************************************************************) open Term +open EConstr exception UFAIL of constr*constr -val unif : constr -> constr -> (int*constr) list +val unif : Evd.evar_map -> constr -> constr -> (int*constr) list type instance= Real of (int*constr)*int (* nb trous*terme*valeur heuristique *) | Phantom of constr (* domaine de quantification *) -val unif_atoms : metavariable -> constr -> constr -> constr -> instance option +val unif_atoms : Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option -val more_general : (int*constr) -> (int*constr) -> bool +val more_general : Evd.evar_map -> (int*constr) -> (int*constr) -> bool diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index e11cbc279a..25d8f8c832 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -617,9 +617,9 @@ let rec fourier () = [Tacticals.New.tclORELSE (* TODO : Ring.polynom []*) (Proofview.tclUNIT ()) (Proofview.tclUNIT ()); - Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) (fun symeq -> + Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) >>= fun symeq -> (Tacticals.New.tclTHEN (apply symeq) - (apply (get coq_Rinv_1))))] + (apply (get coq_Rinv_1)))] ) ])); diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 40f30c7943..ff5e7d5ff2 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -85,7 +85,7 @@ TACTIC EXTEND not_evar END TACTIC EXTEND is_ground - [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ] + [ "is_ground" constr(ty) ] -> [ is_ground ty ] END TACTIC EXTEND autoapply diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index c50100bf55..fdcaedab3a 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -19,6 +19,7 @@ open Geninterp open Extraargs open Tacmach open Tacticals +open Proofview.Notations open Rewrite open Stdarg open Pcoq.Vernac_ @@ -123,15 +124,19 @@ TACTIC EXTEND rewrite_strat END let clsubstitute o c = + Proofview.Goal.enter { enter = begin fun gl -> let is_tac id = match fst (fst (snd c)) with GVar (_, id') when Id.equal id' id -> true | _ -> false in - Tacticals.onAllHypsAndConcl + let hyps = Tacmach.New.pf_ids_of_hyps gl in + Tacticals.New.tclMAP (fun cl -> match cl with - | Some id when is_tac id -> tclIDTAC - | _ -> Proofview.V82.of_tactic (cl_rewrite_clause c o AllOccurrences cl)) + | Some id when is_tac id -> Tacticals.New.tclIDTAC + | _ -> cl_rewrite_clause c o AllOccurrences cl) + (None :: List.map (fun id -> Some id) hyps) + end } TACTIC EXTEND substitute -| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ Proofview.V82.tactic (clsubstitute o c) ] +| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ] END diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index b84be4600c..12a1566e20 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2197,7 +2197,8 @@ let setoid_transitivity c = (transitivity_red true c) let setoid_symmetry_in id = - Proofview.V82.tactic (fun gl -> + let open Tacmach.New in + Proofview.Goal.enter { enter = begin fun gl -> let sigma = project gl in let ctype = pf_unsafe_type_of gl (mkVar id) in let binders,concl = decompose_prod_assum sigma ctype in @@ -2211,11 +2212,10 @@ let setoid_symmetry_in id = let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in let new_hyp' = mkApp (he, [| c2 ; c1 |]) in let new_hyp = it_mkProd_or_LetIn new_hyp' binders in - Proofview.V82.of_tactic (tclTHENLAST (Tactics.assert_after_replacing id new_hyp) (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ])) - gl) + end } let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 4b87e6e2ed..eb26c5431d 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -901,16 +901,13 @@ struct coq_Qeq, Mc.OpEq ] - let has_typ gl t1 typ = - let ty = Retyping.get_type_of (Tacmach.pf_env gl) (Tacmach.project gl) t1 in - EConstr.eq_constr (Tacmach.project gl) ty typ - + type gl = { env : Environ.env; sigma : Evd.evar_map } let is_convertible gl t1 t2 = - Reductionops.is_conv (Tacmach.pf_env gl) (Tacmach.project gl) t1 t2 + Reductionops.is_conv gl.env gl.sigma t1 t2 let parse_zop gl (op,args) = - let sigma = Tacmach.project gl in + let sigma = gl.sigma in match EConstr.kind sigma op with | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1)) | Ind((n,0),_) -> @@ -920,7 +917,7 @@ struct | _ -> failwith "parse_zop" let parse_rop gl (op,args) = - let sigma = Tacmach.project gl in + let sigma = gl.sigma in match EConstr.kind sigma op with | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1)) | Ind((n,0),_) -> @@ -930,7 +927,7 @@ struct | _ -> failwith "parse_zop" let parse_qop gl (op,args) = - (assoc_const (Tacmach.project gl) op qop_table, args.(0) , args.(1)) + (assoc_const gl.sigma op qop_table, args.(0) , args.(1)) let is_constant sigma t = (* This is an approx *) match EConstr.kind sigma t with @@ -1154,7 +1151,7 @@ struct rop_spec let parse_arith parse_op parse_expr env cstr gl = - let sigma = Tacmach.project gl in + let sigma = gl.sigma in if debug then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ()); match EConstr.kind sigma cstr with @@ -1199,7 +1196,7 @@ struct *) let parse_formula gl parse_atom env tg term = - let sigma = Tacmach.project gl in + let sigma = gl.sigma in let parse_atom env tg t = try @@ -1208,7 +1205,7 @@ struct with e when CErrors.noncritical e -> (X(t),env,tg) in let is_prop term = - let sort = Retyping.get_sort_of (Tacmach.pf_env gl) (Tacmach.project gl) term in + let sort = Retyping.get_sort_of gl.env gl.sigma term in Sorts.is_prop sort in let rec xparse_formula env tg term = @@ -1720,7 +1717,6 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* let vm = dump_varmap (spec.typ) (vm_of_list env) in (* todo : directly generate the proof term - or generalize before conversion? *) Proofview.Goal.nf_enter { enter = begin fun gl -> - let gl = Tacmach.New.of_old (fun x -> x) gl in Tacticals.New.tclTHENLIST [ Tactics.change_concl @@ -1730,7 +1726,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|])); ("__wit", cert, cert_typ) ] - (Tacmach.pf_concl gl)) + (Tacmach.New.pf_concl gl)) ] end } @@ -1967,11 +1963,13 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 Some (ids,ff',res') - (** * Parse the proof environment, and call micromega_tauto *) +let fresh_id avoid id gl = + Tactics.fresh_id_in_env avoid id (Proofview.Goal.env gl) + let micromega_gen parse_arith (negate:'cst atom -> 'cst mc_cnf) @@ -1979,17 +1977,17 @@ let micromega_gen unsat deduce spec dumpexpr prover tac = Proofview.Goal.nf_enter { enter = begin fun gl -> - let gl = Tacmach.New.of_old (fun x -> x) gl in - let sigma = Tacmach.project gl in - let concl = Tacmach.pf_concl gl in - let hyps = Tacmach.pf_hyps_types gl in + let sigma = Tacmach.New.project gl in + let concl = Tacmach.New.pf_concl gl in + let hyps = Tacmach.New.pf_hyps_types gl in try - let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in + let gl0 = { env = Tacmach.New.pf_env gl; sigma } in + let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in let env = Env.elements env in let spec = Lazy.force spec in let dumpexpr = Lazy.force dumpexpr in - match micromega_tauto negate normalise unsat deduce spec prover env hyps concl gl with + match micromega_tauto negate normalise unsat deduce spec prover env hyps concl gl0 with | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") | Some (ids,ff',res') -> let (arith_goal,props,vars,ff_arith) = make_goal_of_formula sigma dumpexpr ff' in @@ -1998,7 +1996,7 @@ let micromega_gen let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in let ipat_of_name id = Some (Loc.ghost, Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in - let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in + let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; @@ -2057,7 +2055,6 @@ let micromega_order_changer cert env ff = let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) (vm_of_list env) in Proofview.Goal.nf_enter { enter = begin fun gl -> - let gl = Tacmach.New.of_old (fun x -> x) gl in Tacticals.New.tclTHENLIST [ (Tactics.change_concl @@ -2069,7 +2066,7 @@ let micromega_order_changer cert env ff = [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t"), [|typ|])); ("__wit", cert, cert_typ) ] - (Tacmach.pf_concl gl))); + (Tacmach.New.pf_concl gl))); (* Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)*) ] end } @@ -2088,20 +2085,20 @@ let micromega_genr prover tac = dump_proof = dump_psatz coq_Q dump_q } in Proofview.Goal.nf_enter { enter = begin fun gl -> - let gl = Tacmach.New.of_old (fun x -> x) gl in - let sigma = Tacmach.project gl in - let concl = Tacmach.pf_concl gl in - let hyps = Tacmach.pf_hyps_types gl in + let sigma = Tacmach.New.project gl in + let concl = Tacmach.New.pf_concl gl in + let hyps = Tacmach.New.pf_hyps_types gl in try - let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in + let gl0 = { env = Tacmach.New.pf_env gl; sigma } in + let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in let env = Env.elements env in let spec = Lazy.force spec in let hyps' = List.map (fun (n,f) -> (n, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl in - match micromega_tauto negate normalise unsat deduce spec prover env hyps' concl' gl with + match micromega_tauto negate normalise unsat deduce spec prover env hyps' concl' gl0 with | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") | Some (ids,ff',res') -> let (ff,ids) = formula_hyps_concl @@ -2114,7 +2111,7 @@ let micromega_genr prover tac = let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in let ipat_of_name id = Some (Loc.ghost, Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in - let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in + let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 7780de7127..92b092ffe9 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -19,8 +19,8 @@ open Names open Nameops open Term open EConstr -open Tacticals -open Tacmach +open Tacticals.New +open Tacmach.New open Tactics open Logic open Libnames @@ -41,7 +41,9 @@ let elim_id id = Proofview.Goal.enter { enter = begin fun gl -> simplest_elim (Tacmach.New.pf_global id gl) end } -let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl +let resolve_id id = Proofview.Goal.enter { enter = begin fun gl -> + apply (Tacmach.New.pf_global id gl) +end } let timing timer_name f arg = f arg @@ -146,14 +148,14 @@ let intern_id,unintern_id,reset_intern_tables = Hashtbl.add table v idx; Hashtbl.add co_table idx v; v), (fun () -> cpt := 0; Hashtbl.clear table) -let mk_then = tclTHENLIST +let mk_then tacs = tclTHENLIST tacs let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) let generalize_tac t = generalize t let elim t = simplest_elim t -let exact t = Tacmach.refine t let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] +let pf_nf gl c = pf_apply Tacred.simpl gl c let rev_assoc k = let rec loop = function @@ -580,9 +582,12 @@ let abstract_path sigma typ path t = let abstract = context sigma (fun i t -> term_occur:= t; mkRel i) path t in mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur -let focused_simpl path gl = +let focused_simpl path = + let open Tacmach.New in + Proofview.Goal.nf_enter { enter = begin fun gl -> let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in - Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl + convert_concl_no_check newc DEFAULTcast + end } let focused_simpl path = focused_simpl path @@ -640,11 +645,19 @@ let decompile af = in loop af.body -let mkNewMeta () = mkMeta (Evarutil.new_meta()) +(** Backward compat to emulate the old Refine: normalize the goal conclusion *) +let new_hole env sigma c = + let c = Reductionops.nf_betaiota (Sigma.to_evar_map sigma) c in + Evarutil.new_evar env sigma c -let clever_rewrite_base_poly typ p result theorem gl = +let clever_rewrite_base_poly typ p result theorem = + let open Tacmach.New in + let open Sigma in + Proofview.Goal.nf_enter { enter = begin fun gl -> let full = pf_concl gl in + let env = pf_env gl in let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in + Refine.refine { run = begin fun sigma -> let t = applist (mkLambda @@ -657,13 +670,17 @@ let clever_rewrite_base_poly typ p result theorem gl = [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))), [abstracted]) in - exact (applist(t,[mkNewMeta()])) gl + let argt = mkApp (abstracted, [|result|]) in + let Sigma (hole, sigma, p) = new_hole env sigma argt in + Sigma (applist (t, [hole]), sigma, p) + end } + end } -let clever_rewrite_base p result theorem gl = - clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem gl +let clever_rewrite_base p result theorem = + clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem -let clever_rewrite_base_nat p result theorem gl = - clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem gl +let clever_rewrite_base_nat p result theorem = + clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem let clever_rewrite_gen p result (t,args) = let theorem = applist(t, args) in @@ -673,12 +690,29 @@ let clever_rewrite_gen_nat p result (t,args) = let theorem = applist(t, args) in clever_rewrite_base_nat p result theorem -let clever_rewrite p vpath t gl = +(** Solve using the term the term [t _] *) +let refine_app gl t = + let open Tacmach.New in + let open Sigma in + Refine.refine { run = begin fun sigma -> + let env = pf_env gl in + let ht = match EConstr.kind (Sigma.to_evar_map sigma) (pf_get_type_of gl t) with + | Prod (_, t, _) -> t + | _ -> assert false + in + let Sigma (hole, sigma, p) = new_hole env sigma ht in + Sigma (applist (t, [hole]), sigma, p) + end } + +let clever_rewrite p vpath t = + let open Tacmach.New in + Proofview.Goal.nf_enter { enter = begin fun gl -> let full = pf_concl gl in let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in let t' = applist(t, (vargs @ [abstracted])) in - exact (applist(t',[mkNewMeta()])) gl + refine_app gl t' + end } let rec shuffle p (t1,t2) = match t1,t2 with @@ -942,15 +976,15 @@ let rec transform sigma p t = transform sigma p (mkApp (Lazy.force coq_Zplus, [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in - Proofview.V82.of_tactic (unfold sp_Zminus) :: tac,t + unfold sp_Zminus :: tac,t | Kapp(Zsucc,[t1]) -> let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus, [| t1; mk_integer one |])) in - Proofview.V82.of_tactic (unfold sp_Zsucc) :: tac,t + unfold sp_Zsucc :: tac,t | Kapp(Zpred,[t1]) -> let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus, [| t1; mk_integer negone |])) in - Proofview.V82.of_tactic (unfold sp_Zpred) :: tac,t + unfold sp_Zpred :: tac,t | Kapp(Zmult,[t1;t2]) -> let tac1,t1' = transform sigma (P_APP 1 :: p) t1 and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in @@ -1068,7 +1102,7 @@ let replay_history tactic_normalisation = | HYP e :: l -> begin try - Tacticals.New.tclTHEN + tclTHEN (Id.List.assoc (hyp_of_tag e.id) tactic_normalisation) (loop l) with Not_found -> loop l end @@ -1080,16 +1114,16 @@ let replay_history tactic_normalisation = let k = if b then negone else one in let p_initial = [P_APP 1;P_TYPE] in let tac= shuffle_mult_right p_initial e1.body k e2.body in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ generalize_tac [mkApp (Lazy.force coq_OMEGA17, [| val_of eq1; val_of eq2; mk_integer k; mkVar id1; mkVar id2 |])]; - Proofview.V82.tactic (mk_then tac); + mk_then tac; (intros_using [aux]); - Proofview.V82.tactic (resolve_id aux); + resolve_id aux; reflexivity ] | CONTRADICTION (e1,e2) :: l -> @@ -1104,8 +1138,8 @@ let replay_history tactic_normalisation = Lazy.force coq_Gt; Lazy.force coq_Gt |]) in - Tacticals.New.tclTHENS - (Tacticals.New.tclTHENLIST [ + tclTHENS + (tclTHENLIST [ unfold sp_Zle; simpl_in_concl; intro; @@ -1118,7 +1152,7 @@ let replay_history tactic_normalisation = mkVar (hyp_of_tag e1.id); mkVar (hyp_of_tag e2.id) |]) in - Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (generalize_tac [theorem])) (mk_then tac))) (solve_le) + Proofview.tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) solve_le | DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> let id = hyp_of_tag e1.id in let eq1 = val_of(decompile e1) @@ -1128,10 +1162,10 @@ let replay_history tactic_normalisation = let rhs = mk_plus (mk_times eq2 kk) dd in let state_eg = mk_eq eq1 rhs in let tac = scalar_norm_add [P_APP 3] e2.body in - Tacticals.New.tclTHENS + tclTHENS (cut state_eg) - [ Tacticals.New.tclTHENS - (Tacticals.New.tclTHENLIST [ + [ tclTHENS + (tclTHENLIST [ (intros_using [aux]); (generalize_tac [mkApp (Lazy.force coq_OMEGA1, @@ -1139,9 +1173,9 @@ let replay_history tactic_normalisation = (clear [aux;id]); (intros_using [id]); (cut (mk_gt kk dd)) ]) - [ Tacticals.New.tclTHENS + [ tclTHENS (cut (mk_gt kk izero)) - [ Tacticals.New.tclTHENLIST [ + [ tclTHENLIST [ (intros_using [aux1; aux2]); (generalize_tac [mkApp (Lazy.force coq_Zmult_le_approx, @@ -1149,13 +1183,13 @@ let replay_history tactic_normalisation = (clear [aux1;aux2;id]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (unfold sp_Zgt); simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] + tclTHEN (mk_then tac) reflexivity ] | NOT_EXACT_DIVIDE (e1,k) :: l -> let c = floor_div e1.constant k in @@ -1166,10 +1200,10 @@ let replay_history tactic_normalisation = let kk = mk_integer k and dd = mk_integer d in let tac = scalar_norm_add [P_APP 2] e2.body in - Tacticals.New.tclTHENS + tclTHENS (cut (mk_gt dd izero)) - [ Tacticals.New.tclTHENS (cut (mk_gt kk dd)) - [Tacticals.New.tclTHENLIST [ + [ tclTHENS (cut (mk_gt kk dd)) + [tclTHENLIST [ (intros_using [aux2;aux1]); (generalize_tac [mkApp (Lazy.force coq_OMEGA4, @@ -1177,14 +1211,14 @@ let replay_history tactic_normalisation = (clear [aux1;aux2]); unfold sp_not; (intros_using [aux]); - Proofview.V82.tactic (resolve_id aux); - Proofview.V82.tactic (mk_then tac); + resolve_id aux; + mk_then tac; assumption ] ; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ] @@ -1197,9 +1231,9 @@ let replay_history tactic_normalisation = let state_eq = mk_eq eq1 (mk_times eq2 kk) in if e1.kind == DISE then let tac = scalar_norm [P_APP 3] e2.body in - Tacticals.New.tclTHENS + tclTHENS (cut state_eq) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux1]); (generalize_tac [mkApp (Lazy.force coq_OMEGA18, @@ -1207,14 +1241,14 @@ let replay_history tactic_normalisation = (clear [aux1;id]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] + tclTHEN (mk_then tac) reflexivity ] else let tac = scalar_norm [P_APP 3] e2.body in - Tacticals.New.tclTHENS (cut state_eq) + tclTHENS (cut state_eq) [ - Tacticals.New.tclTHENS + tclTHENS (cut (mk_gt kk izero)) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux2;aux1]); (generalize_tac [mkApp (Lazy.force coq_OMEGA3, @@ -1222,11 +1256,11 @@ let replay_history tactic_normalisation = (clear [aux1;aux2;id]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] + tclTHEN (mk_then tac) reflexivity ] | (MERGE_EQ(e3,e1,e2)) :: l -> let id = new_identifier () in tag_hypothesis id e3; @@ -1239,16 +1273,16 @@ let replay_history tactic_normalisation = (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: scalar_norm [P_APP 3] e1.body in - Tacticals.New.tclTHENS + tclTHENS (cut (mk_eq eq1 (mk_inv eq2))) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux]); (generalize_tac [mkApp (Lazy.force coq_OMEGA8, [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]); (clear [id1;id2;aux]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity] + tclTHEN (mk_then tac) reflexivity] | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l -> let id = new_identifier () @@ -1272,9 +1306,9 @@ let replay_history tactic_normalisation = [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: shuffle_mult_right p_initial orig.body m ({c= negone;v= v}::def.body) in - Tacticals.New.tclTHENS + tclTHENS (cut theorem) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux]); (elim_id aux); (clear [aux]); @@ -1282,11 +1316,11 @@ let replay_history tactic_normalisation = (generalize_tac [mkApp (Lazy.force coq_OMEGA9, [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]); - Proofview.V82.tactic (mk_then tac); + mk_then tac; (clear [aux]); (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHEN (exists_tac eq1) reflexivity ] + tclTHEN (exists_tac eq1) reflexivity ] | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> let id1 = new_identifier () and id2 = new_identifier () in @@ -1295,10 +1329,10 @@ let replay_history tactic_normalisation = let tac1 = norm_add [P_APP 2;P_TYPE] e.body in let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in let eq = val_of(decompile e) in - Tacticals.New.tclTHENS + tclTHENS (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id]))) - [Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac1); (intros_using [id1]); (loop act1) ]; - Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac2); (intros_using [id2]); (loop act2) ]] + [tclTHENLIST [ mk_then tac1; (intros_using [id1]); (loop act1) ]; + tclTHENLIST [ mk_then tac2; (intros_using [id2]); (loop act2) ]] | SUM(e3,(k1,e1),(k2,e2)) :: l -> let id = new_identifier () in tag_hypothesis id e3; @@ -1317,10 +1351,10 @@ let replay_history tactic_normalisation = let p_initial = if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in let tac = shuffle_mult_right p_initial e1.body k2 e2.body in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]); - Proofview.V82.tactic (mk_then tac); + mk_then tac; (intros_using [id]); (loop l) ] @@ -1329,10 +1363,10 @@ let replay_history tactic_normalisation = and kk2 = mk_integer k2 in let p_initial = [P_APP 2;P_TYPE] in let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in - Tacticals.New.tclTHENS (cut (mk_gt kk1 izero)) - [Tacticals.New.tclTHENS + tclTHENS (cut (mk_gt kk1 izero)) + [tclTHENS (cut (mk_gt kk2 izero)) - [Tacticals.New.tclTHENLIST [ + [tclTHENLIST [ (intros_using [aux2;aux1]); (generalize_tac [mkApp (Lazy.force coq_OMEGA7, [| @@ -1340,29 +1374,29 @@ let replay_history tactic_normalisation = mkVar aux1;mkVar aux2; mkVar id1;mkVar id2 |])]); (clear [aux1;aux2]); - Proofview.V82.tactic (mk_then tac); + mk_then tac; (intros_using [id]); (loop l) ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ]; - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ] ] | CONSTANT_NOT_NUL(e,k) :: l -> - Tacticals.New.tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl + tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl | CONSTANT_NUL(e) :: l -> - Tacticals.New.tclTHEN (Proofview.V82.tactic (resolve_id (hyp_of_tag e))) reflexivity + tclTHEN (resolve_id (hyp_of_tag e)) reflexivity | CONSTANT_NEG(e,k) :: l -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkVar (hyp_of_tag e)]); unfold sp_Zle; simpl_in_concl; unfold sp_not; (intros_using [aux]); - Proofview.V82.tactic (resolve_id aux); + resolve_id aux; reflexivity ] | _ -> Proofview.tclUNIT () @@ -1380,12 +1414,12 @@ let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) = let (tac,t') = normalize sigma p_initial t in let shift_left = tclTHEN - (Proofview.V82.of_tactic (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])) - (tclTRY (Proofview.V82.of_tactic (clear [id]))) + (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]) + (tclTRY (clear [id])) in if not (List.is_empty tac) then let id' = new_identifier () in - ((id',(Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (shift_left); Proofview.V82.tactic (mk_then tac); (intros_using [id']) ])) + ((id',(tclTHENLIST [ shift_left; mk_then tac; (intros_using [id']) ])) :: tactic, compile id' flag t' :: defs) else @@ -1430,7 +1464,7 @@ let destructure_omega gl tac_def (id,c) = let reintroduce id = (* [id] cannot be cleared if dependent: protect it by a try *) - Tacticals.New.tclTHEN (Tacticals.New.tclTRY (clear [id])) (intro_using id) + tclTHEN (tclTRY (clear [id])) (intro_using id) open Proofview.Notations @@ -1449,7 +1483,7 @@ let coq_omega = let id = new_identifier () in let i = new_id () in tag_hypothesis id i; - (Tacticals.New.tclTHENLIST [ + (tclTHENLIST [ (simplest_elim (applist (Lazy.force coq_intro_Z, [t]))); (intros_using [v; id]); (elim_id id); @@ -1460,7 +1494,7 @@ let coq_omega = body = [{v=intern_id v; c=one}]; constant = zero; id = i} :: sys else - (Tacticals.New.tclTHENLIST [ + (tclTHENLIST [ (simplest_elim (applist (Lazy.force coq_new_var, [t]))); (intros_using [v;th]); tac ]), @@ -1476,13 +1510,13 @@ let coq_omega = with UNSOLVABLE -> let _,path = depend [] [] (history ()) in if !display_action_flag then display_action display_var path; - (Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path)) + (tclTHEN prelude (replay_history tactic_normalisation path)) end else begin try let path = simplify_strong (new_id,new_var_num,display_var) system in if !display_action_flag then display_action display_var path; - Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path) - with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system") + tclTHEN prelude (replay_history tactic_normalisation path) + with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system") end end } @@ -1495,36 +1529,36 @@ let nat_inject = Proofview.tclEVARMAP >>= fun sigma -> try match destructurate_term sigma t with | Kapp(Plus,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2)) + tclTHENLIST [ + (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2)) ((Lazy.force coq_inj_plus),[t1;t2])); (explore (P_APP 1 :: p) t1); (explore (P_APP 2 :: p) t2) ] | Kapp(Mult,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2)) + tclTHENLIST [ + (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2)) ((Lazy.force coq_inj_mult),[t1;t2])); (explore (P_APP 1 :: p) t1); (explore (P_APP 2 :: p) t2) ] | Kapp(Minus,[t1;t2]) -> let id = new_identifier () in - Tacticals.New.tclTHENS - (Tacticals.New.tclTHEN + tclTHENS + (tclTHEN (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1]))) (intros_using [id])) [ - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (clever_rewrite_gen p + tclTHENLIST [ + (clever_rewrite_gen p (mk_minus (mk_inj t1) (mk_inj t2)) ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id])); (loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]); (explore (P_APP 1 :: p) t1); (explore (P_APP 2 :: p) t2) ]; - (Tacticals.New.tclTHEN - (Proofview.V82.tactic (clever_rewrite_gen p (mk_integer zero) - ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id]))) + (tclTHEN + (clever_rewrite_gen p (mk_integer zero) + ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id])) (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])])) ] | Kapp(S,[t']) -> @@ -1538,24 +1572,24 @@ let nat_inject = let rec loop p t : unit Proofview.tactic = try match destructurate_term sigma t with Kapp(S,[t]) -> - (Tacticals.New.tclTHEN - (Proofview.V82.tactic (clever_rewrite_gen p + (tclTHEN + (clever_rewrite_gen p (mkApp (Lazy.force coq_Zsucc, [| mk_inj t |])) - ((Lazy.force coq_inj_S),[t]))) + ((Lazy.force coq_inj_S),[t])) (loop (P_APP 1 :: p) t)) | _ -> explore p t with e when catchable_exception e -> explore p t in - if is_number t' then Proofview.V82.tactic (focused_simpl p) else loop p t + if is_number t' then focused_simpl p else loop p t | Kapp(Pred,[t]) -> let t_minus_one = mkApp (Lazy.force coq_minus, [| t; mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in - Tacticals.New.tclTHEN - (Proofview.V82.tactic (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one - ((Lazy.force coq_pred_of_minus),[t]))) + tclTHEN + (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one + ((Lazy.force coq_pred_of_minus),[t])) (explore p t_minus_one) - | Kapp(O,[]) -> Proofview.V82.tactic (focused_simpl p) + | Kapp(O,[]) -> focused_simpl p | _ -> Proofview.tclUNIT () with e when catchable_exception e -> Proofview.tclUNIT () @@ -1565,7 +1599,7 @@ let nat_inject = Proofview.tclEVARMAP >>= fun sigma -> begin try match destructurate_prop sigma t with Kapp(Le,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1574,7 +1608,7 @@ let nat_inject = (loop lit) ] | Kapp(Lt,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1583,7 +1617,7 @@ let nat_inject = (loop lit) ] | Kapp(Ge,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1592,7 +1626,7 @@ let nat_inject = (loop lit) ] | Kapp(Gt,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1601,7 +1635,7 @@ let nat_inject = (loop lit) ] | Kapp(Neq,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); @@ -1611,7 +1645,7 @@ let nat_inject = ] | Kapp(Eq,[typ;t1;t2]) -> if is_conv typ (Lazy.force coq_nat) then - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]); (explore [P_APP 2; P_TYPE] t1); @@ -1697,20 +1731,20 @@ let fresh_id avoid id gl = let onClearedName id tac = (* We cannot ensure that hyps can be cleared (because of dependencies), *) (* so renaming may be necessary *) - Tacticals.New.tclTHEN - (Tacticals.New.tclTRY (clear [id])) - (Proofview.Goal.enter { enter = begin fun gl -> + tclTHEN + (tclTRY (clear [id])) + (Proofview.Goal.nf_enter { enter = begin fun gl -> let id = fresh_id [] id gl in - Tacticals.New.tclTHEN (introduction id) (tac id) + tclTHEN (introduction id) (tac id) end }) let onClearedName2 id tac = - Tacticals.New.tclTHEN - (Tacticals.New.tclTRY (clear [id])) - (Proofview.Goal.enter { enter = begin fun gl -> + tclTHEN + (tclTRY (clear [id])) + (Proofview.Goal.nf_enter { enter = begin fun gl -> let id1 = fresh_id [] (add_suffix id "_left") gl in let id2 = fresh_id [] (add_suffix id "_right") gl in - Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] + tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] end }) let rec is_Prop sigma c = match EConstr.kind sigma c with @@ -1724,7 +1758,7 @@ let destructure_hyps = let decidability = decidability gl in let pf_nf = pf_nf gl in let rec loop = function - | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega) + | [] -> (tclTHEN nat_inject coq_omega) | decl::lit -> let i = NamedDecl.get_id decl in Proofview.tclEVARMAP >>= fun sigma -> @@ -1732,17 +1766,17 @@ let destructure_hyps = | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit | Kapp(Or,[t1;t2]) -> - (Tacticals.New.tclTHENS + (tclTHENS (elim_id i) [ onClearedName i (fun i -> (loop (LocalAssum (i,t1)::lit))); onClearedName i (fun i -> (loop (LocalAssum (i,t2)::lit))) ]) | Kapp(And,[t1;t2]) -> - Tacticals.New.tclTHEN + tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> loop (LocalAssum (i1,t1) :: LocalAssum (i2,t2) :: lit))) | Kapp(Iff,[t1;t2]) -> - Tacticals.New.tclTHEN + tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> loop (LocalAssum (i1,mkArrow t1 t2) :: LocalAssum (i2,mkArrow t2 t1) :: lit))) @@ -1752,7 +1786,7 @@ let destructure_hyps = if is_Prop sigma (type_of t2) then let d1 = decidability t1 in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_imp_simp, [| t1; t2; d1; mkVar i|])]); (onClearedName i (fun i -> @@ -1763,7 +1797,7 @@ let destructure_hyps = | Kapp(Not,[t]) -> begin match destructurate_prop sigma t with Kapp(Or,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); (onClearedName i (fun i -> @@ -1771,7 +1805,7 @@ let destructure_hyps = ] | Kapp(And,[t1;t2]) -> let d1 = decidability t1 in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_and, [| t1; t2; d1; mkVar i |])]); @@ -1781,7 +1815,7 @@ let destructure_hyps = | Kapp(Iff,[t1;t2]) -> let d1 = decidability t1 in let d2 = decidability t2 in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_iff, [| t1; t2; d1; d2; mkVar i |])]); @@ -1793,7 +1827,7 @@ let destructure_hyps = (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok. For t1, being decidable implies being Prop. *) let d1 = decidability t1 in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_imp, [| t1; t2; d1; mkVar i |])]); @@ -1802,7 +1836,7 @@ let destructure_hyps = ] | Kapp(Not,[t]) -> let d = decidability t in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit)))) @@ -1810,7 +1844,7 @@ let destructure_hyps = | Kapp(op,[t1;t2]) -> (try let thm = not_binop op in - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (generalize_tac [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]); (onClearedName i (fun _ -> loop lit)) @@ -1820,14 +1854,14 @@ let destructure_hyps = if !old_style_flag then begin match destructurate_type sigma (pf_nf typ) with | Kapp(Nat,_) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (simplest_elim (mkApp (Lazy.force coq_not_eq, [|t1;t2;mkVar i|]))); (onClearedName i (fun _ -> loop lit)) ] | Kapp(Z,_) -> - Tacticals.New.tclTHENLIST [ + tclTHENLIST [ (simplest_elim (mkApp (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|]))); @@ -1837,12 +1871,12 @@ let destructure_hyps = end else begin match destructurate_type sigma (pf_nf typ) with | Kapp(Nat,_) -> - (Tacticals.New.tclTHEN + (tclTHEN (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) decl)) (loop lit)) | Kapp(Z,_) -> - (Tacticals.New.tclTHEN + (tclTHEN (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) decl)) (loop lit)) @@ -1870,23 +1904,24 @@ let destructure_goal = Proofview.V82.wrap_exceptions prop >>= fun prop -> match prop with | Kapp(Not,[t]) -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (unfold sp_not) intro) + (tclTHEN + (tclTHEN (unfold sp_not) intro) destructure_hyps) - | Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b)) + | Kimp(a,b) -> (tclTHEN intro (loop b)) | Kapp(False,[]) -> destructure_hyps | _ -> let goal_tac = try let dec = decidability t in - Tacticals.New.tclTHEN - (Proofview.V82.tactic (Tacmach.refine - (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))) + tclTHEN + (Proofview.Goal.nf_enter { enter = begin fun gl -> + refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |])) + end }) intro with Undecidable -> Tactics.elim_type (Lazy.force coq_False) | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in - Tacticals.New.tclTHEN goal_tac destructure_hyps + tclTHEN goal_tac destructure_hyps in (loop concl) end } diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 5c68078d7d..8d7ae51fc0 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -285,7 +285,7 @@ module type Int = sig val mk : Bigint.bigint -> Term.constr val parse_term : Term.constr -> parse_term - val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel + val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel (* check whether t is built only with numbers and + * - *) val is_scalar : Term.constr -> bool end @@ -350,10 +350,12 @@ let parse_term t = | _ -> Tother with e when Logic.catchable_exception e -> Tother +let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c + let parse_rel gl t = try match destructurate t with | Kapp("eq",[typ;t1;t2]) - when destructurate (EConstr.Unsafe.to_constr (Tacmach.pf_nf gl (EConstr.of_constr typ))) = Kapp("Z",[]) -> Req (t1,t2) + when destructurate (EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr typ))) = Kapp("Z",[]) -> Req (t1,t2) | Kapp("Zne",[t1;t2]) -> Rne (t1,t2) | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2) | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2) diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index af50ea0fff..ee7ff451a9 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -168,7 +168,7 @@ module type Int = (* parsing a term (one level, except if a number is found) *) val parse_term : Term.constr -> parse_term (* parsing a relation expression, including = < <= >= > *) - val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel + val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel (* Is a particular term only made of numbers and + * - ? *) val is_scalar : Term.constr -> bool end diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 9a54ad7789..df7e5cb99e 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -38,7 +38,7 @@ let romega_tactic l = we'd better leave as little as possible in the conclusion, for an easier decidability argument. *) (Tactics.intros) - (Proofview.V82.tactic total_reflexive_omega_tactic)) + (total_reflexive_omega_tactic)) TACTIC EXTEND romega diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index cfe14b230c..a20589fb46 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -8,6 +8,7 @@ open Pp open Util +open Proofview.Notations open Const_omega module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -16,13 +17,12 @@ open OmegaSolver (* Especially useful debugging functions *) let debug = ref false -let show_goal gl = - if !debug then (); Tacticals.tclIDTAC gl +let show_goal = Tacticals.New.tclIDTAC let pp i = print_int i; print_newline (); flush stdout (* More readable than the prefix notation *) -let (>>) = Tacticals.tclTHEN +let (>>) = Tacticals.New.tclTHEN let mkApp = Term.mkApp @@ -739,7 +739,7 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = (* Destructuration des hypothèses et de la conclusion *) let reify_gl env gl = - let concl = Tacmach.pf_concl gl in + let concl = Tacmach.New.pf_concl gl in let concl = EConstr.Unsafe.to_constr concl in let t_concl = Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in @@ -760,7 +760,7 @@ let reify_gl env gl = | [] -> if !debug then print_env_reification env; [] in - let t_lhyps = loop (Tacmach.pf_hyps_types gl) in + let t_lhyps = loop (Tacmach.New.pf_hyps_types gl) in (id_concl,t_concl) :: t_lhyps let rec destructurate_pos_hyp orig list_equations list_depends = function @@ -1283,21 +1283,22 @@ let resolution env full_reified_goal systems_list = CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in let decompose_tactic = decompose_tree env context solution_tree in - Proofview.V82.of_tactic (Tactics.generalize - (l_generalize_arg @ List.map EConstr.mkVar (List.tl l_hyps))) >> - Proofview.V82.of_tactic (Tactics.change_concl reified) >> - Proofview.V82.of_tactic (Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|]))) >> + Tactics.generalize + (l_generalize_arg @ List.map EConstr.mkVar (List.tl l_hyps)) >> + Tactics.change_concl reified >> + Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> show_goal >> - Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >> + Tactics.normalise_vm_in_concl >> (*i Alternatives to the previous line: - Normalisation without VM: Tactics.normalise_in_concl - Skip the conversion check and rely directly on the QED: Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >> i*) - Proofview.V82.of_tactic (Tactics.apply (EConstr.of_constr (Lazy.force coq_I))) + Tactics.apply (EConstr.of_constr (Lazy.force coq_I)) -let total_reflexive_omega_tactic gl = +let total_reflexive_omega_tactic = + Proofview.Goal.nf_enter { enter = begin fun gl -> Coqlib.check_required_library ["Coq";"romega";"ROmega"]; rst_omega_eq (); rst_omega_var (); @@ -1306,9 +1307,9 @@ let total_reflexive_omega_tactic gl = let full_reified_goal = reify_gl env gl in let systems_list = destructurate_hyps full_reified_goal in if !debug then display_systems systems_list; - resolution env full_reified_goal systems_list gl + resolution env full_reified_goal systems_list with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system" - + end } (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*) diff --git a/proofs/goal.mli b/proofs/goal.mli index a2fa34c05e..ee2e736120 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -59,9 +59,6 @@ module V82 : sig second goal *) val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map - (* Principal part of the weak-progress tactical *) - val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool - (* Principal part of the progress tactical *) val progress : goal list Evd.sigma -> goal Evd.sigma -> bool diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 5c7659ac0e..bc12b3ba71 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -162,31 +162,11 @@ let tclMAP tacfun l = (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves the goal unchanged *) -let tclWEAK_PROGRESS tac ptree = - let rslt = tac ptree in - if Goal.V82.weak_progress rslt ptree then rslt - else user_err ~hdr:"Refiner.WEAK_PROGRESS" (str"Failed to progress.") - -(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves -the goal unchanged *) let tclPROGRESS tac ptree = let rslt = tac ptree in if Goal.V82.progress rslt ptree then rslt else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.") -(* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals, - one of them being identical to the original goal *) -let tclNOTSAMEGOAL (tac : tactic) goal = - let same_goal gls1 evd2 gl2 = - Goal.V82.same_goal gls1.sigma gls1.it evd2 gl2 - in - let rslt = tac goal in - let {it=gls;sigma=sigma} = rslt in - if List.exists (same_goal goal sigma) gls - then user_err ~hdr:"Refiner.tclNOTSAMEGOAL" - (str"Tactic generated a subgoal identical to the original goal.") - else rslt - (* Execute tac, show the names of new hypothesis names created by tac in the "as" format and then forget everything. From the logical point of view [tclSHOWHYPS tac] is therefore equivalent to idtac, diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 56f5facf89..e179589df2 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -119,10 +119,8 @@ val tclAT_LEAST_ONCE : tactic -> tactic val tclFAIL : int -> Pp.std_ppcmds -> tactic val tclFAIL_lazy : int -> Pp.std_ppcmds Lazy.t -> tactic val tclDO : int -> tactic -> tactic -val tclWEAK_PROGRESS : tactic -> tactic val tclPROGRESS : tactic -> tactic val tclSHOWHYPS : tactic -> tactic -val tclNOTSAMEGOAL : tactic -> tactic (** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, if it succeeds, applies [tac2] to the resulting subgoals, diff --git a/tactics/auto.ml b/tactics/auto.ml index 74cb7a364f..42230dff17 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -380,7 +380,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl = and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) = let tactic = function | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl) - | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf") + | ERes_pf _ -> Proofview.Goal.enter { enter = fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf") } | Give_exact (c, cl) -> exact poly (c, cl) | Res_pf_THEN_trivial_fail (c,cl) -> Tacticals.New.tclTHEN @@ -389,10 +389,11 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= with "debug auto" we don't display the details of inner trivial *) (trivial_fail_db (no_dbg ()) (not (Option.is_empty flags)) db_list local_db) | Unfold_nth c -> - Proofview.V82.tactic (fun gl -> - if exists_evaluable_reference (pf_env gl) c then - tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl - else tclFAIL 0 (str"Unbound reference") gl) + Proofview.Goal.enter { enter = begin fun gl -> + if exists_evaluable_reference (Tacmach.New.pf_env gl) c then + Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) + else Tacticals.New.tclFAIL 0 (str"Unbound reference") + end } | Extern tacast -> conclPattern concl p tacast in diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index df222eed80..54e4405d1c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -221,18 +221,22 @@ let auto_unif_flags freeze st = resolve_evars = false } -let e_give_exact flags poly (c,clenv) gl = +let e_give_exact flags poly (c,clenv) = + let open Tacmach.New in + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let sigma = project gl in let (c, _, _) = c in - let c, gl = + let c, sigma = if poly then let clenv', subst = Clenv.refresh_undefined_univs clenv in - let evd = evars_reset_evd ~with_conv_pbs:true gl.sigma clenv'.evd in + let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in let c = Vars.subst_univs_level_constr subst c in - c, {gl with sigma = evd} - else c, gl + c, evd + else c, sigma in - let t1 = pf_unsafe_type_of gl c in - Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl + let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in + Sigma.Unsafe.of_pair (Clenvtac.unify ~flags t1 <*> exact_no_check c, sigma) + end } let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) -> let clenv', c = connect_hint_clenv poly c clenv gls in @@ -455,15 +459,14 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co { enter = fun gl -> unify_resolve_refine poly flags gl (c,None,clenv) } in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else - Proofview.V82.tactic (e_give_exact flags poly (c,clenv)) + e_give_exact flags poly (c,clenv) | Res_pf_THEN_trivial_fail (term,cl) -> let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in let snd = if complete then Tacticals.New.tclIDTAC else e_trivial_fail_db only_classes db_list local_db secvars in Tacticals.New.tclTHEN fst snd | Unfold_nth c -> - let tac = Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c]) in - Proofview.V82.tactic (tclWEAK_PROGRESS tac) + Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c]) | Extern tacast -> conclPattern concl p tacast in let tac = run_hint t tac in @@ -1614,9 +1617,11 @@ let not_evar c = | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar") | _ -> Proofview.tclUNIT () -let is_ground c gl = - if Evarutil.is_ground_term (project gl) c then tclIDTAC gl - else tclFAIL 0 (str"Not ground") gl +let is_ground c = + let open Tacticals.New in + Proofview.tclEVARMAP >>= fun sigma -> + if Evarutil.is_ground_term sigma c then tclIDTAC + else tclFAIL 0 (str"Not ground") let autoapply c i = let open Proofview.Notations in diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index a38be5972f..738cc0feba 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -33,7 +33,7 @@ val head_of_constr : Id.t -> constr -> unit Proofview.tactic val not_evar : constr -> unit Proofview.tactic -val is_ground : constr -> tactic +val is_ground : constr -> unit Proofview.tactic val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic diff --git a/tactics/equality.ml b/tactics/equality.ml index 7ae7446c82..25c28cf4ac 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -97,9 +97,6 @@ let _ = (* Rewriting tactics *) -let tclNOTSAMEGOAL tac = - Proofview.V82.tactic (Tacticals.tclNOTSAMEGOAL (Proofview.V82.of_tactic tac)) - type dep_proof_flag = bool (* true = support rewriting dependent proofs *) type freeze_evars_flag = bool (* true = don't instantiate existing evars *) @@ -268,6 +265,25 @@ let rewrite_elim with_evars frzevars cls c e = general_elim_clause with_evars flags cls c e end } +let tclNOTSAMEGOAL tac = + let goal gl = Proofview.Goal.goal (Proofview.Goal.assume gl) in + Proofview.Goal.nf_enter { enter = begin fun gl -> + let sigma = project gl in + let ev = goal gl in + tac >>= fun () -> + Proofview.Goal.goals >>= fun gls -> + let check accu gl' = + gl' >>= fun gl' -> + let accu = accu || Goal.V82.same_goal sigma ev (project gl') (goal gl') in + Proofview.tclUNIT accu + in + Proofview.Monad.List.fold_left check false gls >>= fun has_same -> + if has_same then + tclZEROMSG (str"Tactic generated a subgoal identical to the original goal.") + else + Proofview.tclUNIT () + end } + (* Ad hoc asymmetric general_elim_clause *) let general_elim_clause with_evars frzevars cls rew elim = let open Pretype_errors in @@ -642,8 +658,8 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = | Some evd -> let e = build_coq_eq () in let sym = build_coq_eq_sym () in - Tacticals.New.pf_constr_of_global sym (fun sym -> - Tacticals.New.pf_constr_of_global e (fun e -> + Tacticals.New.pf_constr_of_global sym >>= fun sym -> + Tacticals.New.pf_constr_of_global e >>= fun e -> let eq = applist (e, [t1;c1;c2]) in tclTHENLAST (replace_core clause l2r eq) @@ -651,7 +667,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = [assumption; tclTHEN (apply sym) assumption; try_prove_eq - ]))) + ]) end } let replace c1 c2 = diff --git a/tactics/leminv.ml b/tactics/leminv.ml index daa962f1d6..83f3da30a9 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -260,22 +260,23 @@ let add_inversion_lemma_exn na com comsort bool tac = (* Applying a given inversion lemma *) (* ================================= *) -let lemInv id c gls = +let lemInv id c = + Proofview.Goal.enter { enter = begin fun gls -> try - let open Tacmach in let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in - Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls + Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false with | NoSuchBinding -> user_err - (hov 0 (pr_econstr_env (Refiner.pf_env gls) (Refiner.project gls) c ++ spc () ++ str "does not refer to an inversion lemma.")) + (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma.")) | UserError (a,b) -> user_err ~hdr:"LemInv" (str "Cannot refine current goal with the lemma " ++ - pr_leconstr_env (Refiner.pf_env gls) (Refiner.project gls) c) + pr_leconstr_env (pf_env gls) (project gls) c) + end } -let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id +let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id let lemInvIn id c ids = Proofview.Goal.enter { enter = begin fun gl -> @@ -289,7 +290,7 @@ let lemInvIn id c ids = else (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids)) in - ((tclTHEN (tclTHEN (bring_hyps hyps) (Proofview.V82.tactic (lemInv id c))) + ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c)) (intros_replace_ids))) end } diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 90b7d6581a..c8441a8cc9 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -51,10 +51,8 @@ let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE let tclFAIL = Refiner.tclFAIL let tclFAIL_lazy = Refiner.tclFAIL_lazy let tclDO = Refiner.tclDO -let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS let tclPROGRESS = Refiner.tclPROGRESS let tclSHOWHYPS = Refiner.tclSHOWHYPS -let tclNOTSAMEGOAL = Refiner.tclNOTSAMEGOAL let tclTHENTRY = Refiner.tclTHENTRY let tclIFTHENELSE = Refiner.tclIFTHENELSE let tclIFTHENSELSE = Refiner.tclIFTHENSELSE @@ -734,13 +732,11 @@ module New = struct let case_nodep_then_using = general_elim_then_using gl_make_case_nodep false - let pf_constr_of_global ref tac = - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let (sigma, c) = Evd.fresh_global env sigma ref in - let c = EConstr.of_constr c in - Proofview.Unsafe.tclEVARS sigma <*> (tac c) - end } + let pf_constr_of_global ref = + Proofview.tclEVARMAP >>= fun sigma -> + Proofview.tclENV >>= fun env -> + let (sigma, c) = Evd.fresh_global env sigma ref in + let c = EConstr.of_constr c in + Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c end diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 3b90ec514a..5a4ecbac75 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -44,10 +44,8 @@ val tclAT_LEAST_ONCE : tactic -> tactic val tclFAIL : int -> std_ppcmds -> tactic val tclFAIL_lazy : int -> std_ppcmds Lazy.t -> tactic val tclDO : int -> tactic -> tactic -val tclWEAK_PROGRESS : tactic -> tactic val tclPROGRESS : tactic -> tactic val tclSHOWHYPS : tactic -> tactic -val tclNOTSAMEGOAL : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclMAP : ('a -> tactic) -> 'a list -> tactic @@ -265,5 +263,5 @@ module New : sig val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic - val pf_constr_of_global : Globnames.global_reference -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic + val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e792585822..9c2a1d8509 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2811,20 +2811,18 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl = mkProd_or_LetIn decl cl', sigma' let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = - let env = Tacmach.pf_env gl in - let ids = Tacmach.pf_ids_of_hyps gl in - let sigma, t = Typing.type_of env sigma c in - generalize_goal_gen env sigma ids i o t cl - -let new_generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = - let env = Tacmach.New.pf_env gl in - let ids = Tacmach.New.pf_ids_of_hyps gl in + let open Tacmach.New in + let env = pf_env gl in + let ids = pf_ids_of_hyps gl in let sigma, t = Typing.type_of env sigma c in generalize_goal_gen env sigma ids i o t cl -let old_generalize_dep ?(with_let=false) c gl = +let generalize_dep ?(with_let=false) c = + let open Tacmach.New in + let open Tacticals.New in + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let env = pf_env gl in - let sign = pf_hyps gl in + let sign = Proofview.Goal.hyps gl in let sigma = project gl in let init_ids = ids_of_named_context (Global.named_context()) in let seek (d:named_declaration) (toquant:named_context) = @@ -2843,11 +2841,11 @@ let old_generalize_dep ?(with_let=false) c gl = -> id::tothin | _ -> tothin in - let cl' = it_mkNamedProd_or_LetIn (Tacmach.pf_concl gl) to_quantify in + let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in let body = if with_let then match EConstr.kind sigma c with - | Var id -> id |> Tacmach.pf_get_hyp gl |> NamedDecl.get_value + | Var id -> id |> (fun id -> pf_get_hyp id gl) |> NamedDecl.get_value | _ -> None else None in @@ -2856,20 +2854,19 @@ let old_generalize_dep ?(with_let=false) c gl = (** Check that the generalization is indeed well-typed *) let (evd, _) = Typing.type_of env evd cl'' in let args = Context.Named.to_instance mkVar to_quantify_rev in - tclTHENLIST - [tclEVARS evd; - Proofview.V82.of_tactic (apply_type cl'' (if Option.is_empty body then c::args else args)); - Proofview.V82.of_tactic (clear (List.rev tothin'))] - gl - -let generalize_dep ?(with_let = false) c = - Proofview.V82.tactic (old_generalize_dep ~with_let c) + let tac = + tclTHEN + (apply_type cl'' (if Option.is_empty body then c::args else args)) + (clear (List.rev tothin')) + in + Sigma.Unsafe.of_pair (tac, evd) + end } (** *) let generalize_gen_let lconstr = Proofview.Goal.s_enter { s_enter = begin fun gl -> let env = Proofview.Goal.env gl in let newcl, evd = - List.fold_right_i (new_generalize_goal gl) 0 lconstr + List.fold_right_i (generalize_goal gl) 0 lconstr (Tacmach.New.pf_concl gl,Tacmach.New.project gl) in let (evd, _) = Typing.type_of env evd newcl in @@ -4724,7 +4721,7 @@ let symmetry_red allowred = | Some eq_data,_,_ -> Tacticals.New.tclTHEN (convert_concl_no_check concl DEFAULTcast) - (Tacticals.New.pf_constr_of_global eq_data.sym apply) + (Tacticals.New.pf_constr_of_global eq_data.sym >>= apply) | None,eq,eq_kind -> prove_symmetry eq eq_kind end } @@ -4820,8 +4817,8 @@ let transitivity_red allowred t = Tacticals.New.tclTHEN (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])) + | 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]) | None,eq,eq_kind -> match t with | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.") diff --git a/vernac/command.ml b/vernac/command.ml index 45ff579552..b27d8a0a35 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -1198,11 +1198,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) fixnames fixtypes fiximps in let init_tac = - Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC) + Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in - let init_tac = - Option.map (List.map Proofview.V82.tactic) init_tac - in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint) evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) @@ -1235,11 +1232,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) fixnames fixtypes fiximps in let init_tac = - Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC) + Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in - let init_tac = - Option.map (List.map Proofview.V82.tactic) init_tac - in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) |