From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- tactics/tactics.ml | 377 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 233 insertions(+), 144 deletions(-) (limited to 'tactics/tactics.ml') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7484139c..2a46efd8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -109,6 +109,44 @@ let _ = optread = (fun () -> !clear_hyp_by_default) ; optwrite = (fun b -> clear_hyp_by_default := b) } +(* Compatibility option useful in developments using apply intensively + in ltac code *) + +let universal_lemma_under_conjunctions = ref false + +let accept_universal_lemma_under_conjunctions () = + !universal_lemma_under_conjunctions + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "trivial unification in tactics applying under conjunctions"; + optkey = ["Universal";"Lemma";"Under";"Conjunction"]; + optread = (fun () -> !universal_lemma_under_conjunctions) ; + optwrite = (fun b -> universal_lemma_under_conjunctions := b) } + +(* The following boolean governs what "intros []" do on examples such + as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]"; + if false, it behaves as "intro H; case H; clear H" for fresh H. + Kept as false for compatibility. + *) + +let bracketing_last_or_and_intro_pattern = ref false + +let use_bracketing_last_or_and_intro_pattern () = + !bracketing_last_or_and_intro_pattern + && Flags.version_strictly_greater Flags.V8_4 + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "bracketing last or-and introduction pattern"; + optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; + optread = (fun () -> !bracketing_last_or_and_intro_pattern) ; + optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) } + (*********************************************) (* Tactics *) (*********************************************) @@ -139,7 +177,8 @@ let introduction ?(check=true) id = let store = Proofview.Goal.extra gl in let env = Proofview.Goal.env gl in let () = if check && mem_named_context id hyps then - error ("Variable " ^ Id.to_string id ^ " is already declared.") + errorlabstrm "Tactics.introduction" + (str "Variable " ++ pr_id id ++ str " is already declared.") in match kind_of_term (whd_evar sigma concl) with | Prod (_, t, b) -> unsafe_intro env store (id, None, t) b @@ -157,7 +196,7 @@ let convert_concl ?(check=true) ty k = Proofview.Refine.refine ~unsafe:true begin fun sigma -> let sigma = if check then begin - ignore (Typing.type_of env sigma ty); + ignore (Typing.unsafe_type_of env sigma ty); let sigma,b = Reductionops.infer_conv env sigma ty conclty in if not b then error "Not convertible."; sigma @@ -184,8 +223,9 @@ let convert_hyp_no_check = convert_hyp ~check:false let convert_gen pb x y = Proofview.Goal.enter begin fun gl -> try - let sigma = Tacmach.New.pf_apply Evd.conversion gl pb x y in - Proofview.Unsafe.tclEVARS sigma + let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in + if b then Proofview.Unsafe.tclEVARS sigma + else Tacticals.New.tclFAIL 0 (str "Not convertible") with (* Reduction.NotConvertible *) _ -> (** FIXME: Sometimes an anomaly is raised from conversion *) Tacticals.New.tclFAIL 0 (str "Not convertible") @@ -627,7 +667,7 @@ let change_on_subterm cv_pb deep t where env sigma c = env sigma c in if !mayneedglobalcheck then begin - try ignore (Typing.type_of env sigma c) + try ignore (Typing.unsafe_type_of env sigma c) with e when catchable_exception e -> error "Replacement would lead to an ill-typed term." end; @@ -687,12 +727,11 @@ let reduction_clause redexp cl = let reduce redexp cl goal = let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in let redexps = reduction_clause redexp cl in + let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in let tac = tclMAP (fun (where,redexp) -> - e_reduct_option ~check:true + e_reduct_option ~check (Redexpr.reduction_of_red_expr (pf_env goal) redexp) where) redexps in - match redexp with - | Fold _ | Pattern _ -> with_check tac goal - | _ -> tac goal + if check then with_check tac goal else tac goal (* Unfolding occurrences of a constant *) @@ -751,8 +790,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = (intro_then_gen name_flag move_flag false dep_flag tac)) begin function (e, info) -> match e with | RefinerError IntroNeedsProduct -> - Proofview.tclZERO - (Errors.UserError("Intro",str "No product even after head-reduction.")) + Tacticals.New.tclZEROMSG (str "No product even after head-reduction.") | e -> Proofview.tclZERO ~info e end end @@ -800,16 +838,23 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = aux n [] let get_next_hyp_position id gl = - let rec get_next_hyp_position id = function + let rec aux = function | [] -> raise (RefinerError (NoSuchHyp id)) | (hyp,_,_) :: right -> if Id.equal hyp id then match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast else - get_next_hyp_position id right + aux right + in + aux (Proofview.Goal.hyps (Proofview.Goal.assume gl)) + +let get_previous_hyp_position id gl = + let rec aux dest = function + | [] -> raise (RefinerError (NoSuchHyp id)) + | (hyp,_,_) :: right -> + if Id.equal hyp id then dest else aux (MoveAfter hyp) right in - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - get_next_hyp_position id hyps + aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) let intro_replacing id = Proofview.Goal.enter begin fun gl -> @@ -979,7 +1024,7 @@ let cut c = let is_sort = try (** Backward compat: ensure that [c] is well-typed. *) - let typ = Typing.type_of env sigma c in + let typ = Typing.unsafe_type_of env sigma c in let typ = whd_betadeltaiota env sigma typ in match kind_of_term typ with | Sort _ -> true @@ -1224,7 +1269,7 @@ let find_ind_eliminator ind s gl = evd, c let find_eliminator c gl = - let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_type_of gl c) in + let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in if is_nonrec ind then raise IsNonrec; let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in evd, {elimindex = None; elimbody = (c,NoBindings); @@ -1332,7 +1377,7 @@ let make_projection env sigma params cstr sign elim i n c u = (* to avoid surprising unifications, excludes flexible projection types or lambda which will be instantiated by Meta/Evar *) && not (isEvar (fst (whd_betaiota_stack sigma t))) - && not (isRel t && destRel t > n-i) + && (accept_universal_lemma_under_conjunctions () || not (isRel t)) then let t = lift (i+1-n) t in let abselim = beta_applist (elim,params@[t;branch]) in @@ -1358,7 +1403,7 @@ let make_projection env sigma params cstr sign elim i n c u = | None -> None in elim -let descend_in_conjunctions avoid tac exit c = +let descend_in_conjunctions avoid tac (err, info) c = Proofview.Goal.nf_enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -1392,9 +1437,8 @@ let descend_in_conjunctions avoid tac exit c = (* Might be ill-typed due to forbidden elimination. *) Tacticals.New.onLastHypId (tac (not isrec))] end)) - | None -> - raise Exit - with RefinerError _|UserError _|Exit -> exit () + | None -> Proofview.tclZERO ~info err + with RefinerError _|UserError _ -> Proofview.tclZERO ~info err end (****************************************************) @@ -1417,7 +1461,15 @@ let solve_remaining_apply_goals = with Not_found -> Proofview.tclUNIT () else Proofview.tclUNIT () end - + +let tclORELSEOPT t k = + Proofview.tclORELSE t + (fun e -> match k e with + | None -> + let (e, info) = e in + Proofview.tclZERO ~info e + | Some tac -> tac) + let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in @@ -1442,50 +1494,46 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) with UserError _ as exn -> Proofview.tclZERO exn in - Proofview.tclORELSE + let rec try_red_apply thm_ty (exn0, info) = + try + (* Try to head-reduce the conclusion of the theorem *) + let red_thm = try_red_product env sigma thm_ty in + tclORELSEOPT + (try_apply red_thm concl_nprod) + (function (e, info) -> match e with + | PretypeError _|RefinerError _|UserError _|Failure _ -> + Some (try_red_apply red_thm (exn0, info)) + | _ -> None) + with Redelimination -> + (* Last chance: if the head is a variable, apply may try + second order unification *) + let info = Loc.add_loc info loc in + let tac = + if with_destruct then + descend_in_conjunctions [] + (fun b id -> + Tacticals.New.tclTHEN + (try_main_apply b (mkVar id)) + (Proofview.V82.tactic (thin [id]))) + (exn0, info) c + else + Proofview.tclZERO ~info exn0 in + if not (Int.equal concl_nprod 0) then + tclORELSEOPT + (try_apply thm_ty 0) + (function (e, info) -> match e with + | PretypeError _|RefinerError _|UserError _|Failure _-> + Some tac + | _ -> None) + else + tac + in + tclORELSEOPT (try_apply thm_ty0 concl_nprod) (function (e, info) -> match e with - | PretypeError _|RefinerError _|UserError _|Failure _ as exn0 -> - let rec try_red_apply thm_ty = - try - (* Try to head-reduce the conclusion of the theorem *) - let red_thm = try_red_product env sigma thm_ty in - Proofview.tclORELSE - (try_apply red_thm concl_nprod) - (function (e, info) -> match e with - | PretypeError _|RefinerError _|UserError _|Failure _ -> - try_red_apply red_thm - | exn -> iraise (exn, info)) - with Redelimination -> - (* Last chance: if the head is a variable, apply may try - second order unification *) - let tac = - if with_destruct then - descend_in_conjunctions [] - (fun b id -> - Tacticals.New.tclTHEN - (try_main_apply b (mkVar id)) - (Proofview.V82.tactic (thin [id]))) - (fun _ -> - let info = Loc.add_loc info loc in - Proofview.tclZERO ~info exn0) c - else - let info = Loc.add_loc info loc in - Proofview.tclZERO ~info exn0 in - if not (Int.equal concl_nprod 0) then - try - Proofview.tclORELSE - (try_apply thm_ty 0) - (function (e, info) -> match e with - | PretypeError _|RefinerError _|UserError _|Failure _-> - tac - | exn -> iraise (exn, info)) - with UserError _ | Exit -> - tac - else - tac - in try_red_apply thm_ty0 - | exn -> iraise (exn, info)) + | PretypeError _|RefinerError _|UserError _|Failure _ -> + Some (try_red_apply thm_ty0 (e, info)) + | _ -> None) end in Tacticals.New.tclTHENLIST [ @@ -1596,10 +1644,10 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming tac id ]) with e when with_destruct && Errors.noncritical e -> - let e = Errors.push e in + let (e, info) = Errors.push e in (descend_in_conjunctions [targetid] (fun b id -> aux (id::idstoclear) b (mkVar id)) - (fun _ -> iraise e) c) + (e, info) c) end in aux [] with_destruct d @@ -1636,7 +1684,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam let cut_and_apply c = Proofview.Goal.nf_enter begin fun gl -> - match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_type_of gl c)) with + match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) -> let concl = Proofview.Goal.concl gl in let env = Tacmach.New.pf_env gl in @@ -1669,7 +1717,7 @@ let exact_check c = let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let sigma, ct = Typing.e_type_of env sigma c in + let sigma, ct = Typing.type_of env sigma c in Proofview.Unsafe.tclEVARS sigma <*> Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) end @@ -1818,7 +1866,7 @@ let specialize (c,lbind) g = let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in tclEVARS evd, nf_evar evd c else - let clause = pf_apply make_clenv_binding g (c,pf_type_of g c) lbind in + let clause = pf_apply make_clenv_binding g (c,pf_unsafe_type_of g c) lbind in let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in @@ -1838,11 +1886,11 @@ let specialize (c,lbind) g = | Var id when Id.List.mem id (pf_ids_of_hyps g) -> tclTHEN tac (tclTHENFIRST - (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_type_of g term)) g) + (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_unsafe_type_of g term)) g) (exact_no_check term)) g | _ -> tclTHEN tac (tclTHENLAST - (fun g -> Proofview.V82.of_tactic (cut (pf_type_of g term)) g) + (fun g -> Proofview.V82.of_tactic (cut (pf_unsafe_type_of g term)) g) (exact_no_check term)) g (* Keeping only a few hypotheses *) @@ -1871,8 +1919,8 @@ let check_number_of_constructors expctdnumopt i nconstr = if Int.equal i 0 then error "The constructors are numbered starting from 1."; begin match expctdnumopt with | Some n when not (Int.equal n nconstr) -> - error ("Not an inductive goal with "^ - string_of_int n ^ String.plural n " constructor"^".") + errorlabstrm "Tactics.check_number_of_constructors" + (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".") | _ -> () end; if i > nconstr then error "Not enough constructors." @@ -1977,7 +2025,7 @@ let my_find_eq_data_decompose gl t = let intro_decomp_eq loc l thin tac id = Proofview.Goal.nf_enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in match my_find_eq_data_decompose gl t with | Some (eq,u,eq_args) -> @@ -1991,7 +2039,7 @@ let intro_decomp_eq loc l thin tac id = let intro_or_and_pattern loc bracketed ll thin tac id = Proofview.Goal.enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in let nv = constructors_nrealargs ind in let ll = fix_empty_or_and_pattern (Array.length nv) ll in @@ -2010,7 +2058,7 @@ let rewrite_hyp assert_style l2r id = let clear_var_and_eq c = tclTHEN (clear [id]) (clear [destVar c]) in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in let t = whd_betadeltaiota (type_of (mkVar id)) in match match_with_equality_type t with @@ -2074,7 +2122,7 @@ let make_tmp_naming avoid l = function case of IntroFresh, we should use check_thin_clash_then anyway to prevent the case of an IntroFresh precisely using the wild_id *) | IntroWildcard -> NamingBasedOn (wild_id,avoid@explicit_intro_names l) - | _ -> NamingAvoid(avoid@explicit_intro_names l) + | pat -> NamingAvoid(avoid@explicit_intro_names ((dloc,IntroAction pat)::l)) let fit_bound n = function | None -> true @@ -2088,6 +2136,21 @@ let exceed_bound n = function to ensure that dependent hypotheses are cleared in the right dependency order (see bug #1000); we use fresh names, not used in the tactic, for the hyps to clear *) + (* In [intro_patterns_core b avoid ids thin destopt bound n tac patl]: + [b]: compatibility flag, if false at toplevel, do not complete incomplete + trailing toplevel or_and patterns (as in "intros []", see + [bracketing_last_or_and_intro_pattern]) + [avoid]: names to avoid when creating an internal name + [ids]: collect introduced names for possible use by the [tac] continuation + [thin]: collect names to erase at the end + [destopt]: position in the context where to introduce the hypotheses + [bound]: number of pending intros to do in the current or-and pattern, + with remembering of [b] flag if at toplevel + [n]: number of introduction done in the current or-and pattern + [tac]: continuation tactic + [patl]: introduction patterns to interpret + *) + let rec intro_patterns_core b avoid ids thin destopt bound n tac = function | [] when fit_bound n bound -> tac ids thin @@ -2105,31 +2168,33 @@ let rec intro_patterns_core b avoid ids thin destopt bound n tac = function (n+List.length ids) tac l) | IntroAction pat -> intro_then_gen (make_tmp_naming avoid l pat) - MoveLast true false + destopt true false (intro_pattern_action loc (b || not (List.is_empty l)) false pat thin + destopt (fun thin bound' -> intro_patterns_core b avoid ids thin destopt bound' 0 (fun ids thin -> intro_patterns_core b avoid ids thin destopt bound (n+1) tac l))) | IntroNaming pat -> - intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l + intro_pattern_naming loc b avoid ids pat thin destopt bound (n+1) tac l + (* Pi-introduction rule, used backwards *) and intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l = match pat with | IntroIdentifier id -> check_thin_clash_then id thin avoid (fun thin -> intro_then_gen (NamingMustBe (loc,id)) destopt true false - (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l)) + (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l)) | IntroAnonymous -> intro_then_gen (NamingAvoid (avoid@explicit_intro_names l)) destopt true false - (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l) + (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l) | IntroFresh id -> (* todo: avoid thinned names to interfere with generation of fresh name *) intro_then_gen (NamingBasedOn (id, avoid@explicit_intro_names l)) destopt true false - (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l) + (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l) -and intro_pattern_action loc b style pat thin tac id = match pat with +and intro_pattern_action loc b style pat thin destopt tac id = match pat with | IntroWildcard -> tac ((loc,id)::thin) None [] | IntroOrAndPattern ll -> @@ -2142,7 +2207,13 @@ and intro_pattern_action loc b style pat thin tac id = match pat with (rewrite_hyp style l2r id) (tac thin None []) | IntroApplyOn (f,(loc,pat)) -> - let naming,tac_ipat = prepare_intros_loc loc (IntroIdentifier id) pat in + let naming,tac_ipat = + prepare_intros_loc loc (IntroIdentifier id) destopt pat in + let doclear = + if naming = NamingMustBe (loc,id) then + Proofview.tclUNIT () (* apply_in_once do a replacement *) + else + Proofview.V82.tactic (clear [id]) in Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in @@ -2151,36 +2222,31 @@ and intro_pattern_action loc b style pat thin tac id = match pat with (Tacticals.New.tclTHENFIRST (* Skip the side conditions of the apply *) (apply_in_once false true true true naming id - (None,(sigma,(c,NoBindings))) tac_ipat) (tac thin None [])) + (None,(sigma,(c,NoBindings))) + (fun id -> Tacticals.New.tclTHEN doclear (tac_ipat id))) + (tac thin None [])) sigma end -and prepare_intros_loc loc dft = function +and prepare_intros_loc loc dft destopt = function | IntroNaming ipat -> prepare_naming loc ipat, - (fun _ -> Proofview.tclUNIT ()) + (fun id -> Proofview.V82.tactic (move_hyp id destopt)) | IntroAction ipat -> prepare_naming loc dft, (let tac thin bound = - intro_patterns_core true [] [] thin MoveLast bound 0 + intro_patterns_core true [] [] thin destopt bound 0 (fun _ l -> clear_wildcards l) in - fun id -> intro_pattern_action loc true true ipat [] tac id) + fun id -> intro_pattern_action loc true true ipat [] destopt tac id) | IntroForthcoming _ -> user_err_loc (loc,"",str "Introduction pattern for one hypothesis expected.") let intro_patterns_bound_to n destopt = intro_patterns_core true [] [] [] destopt - (Some (true,n)) 0 (fun _ -> clear_wildcards) - -(* The following boolean governs what "intros []" do on examples such - as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]"; - if false, it behaves as "intro H; case H; clear H" for fresh H. - Kept as false for compatibility. - *) -let bracketing_last_or_and_intro_pattern = false + (Some (true,n)) 0 (fun _ l -> clear_wildcards l) let intro_patterns_to destopt = - intro_patterns_core bracketing_last_or_and_intro_pattern + intro_patterns_core (use_bracketing_last_or_and_intro_pattern ()) [] [] [] destopt None 0 (fun _ l -> clear_wildcards l) let intro_pattern_to destopt pat = @@ -2197,23 +2263,24 @@ let intros_patterns = function (* Forward reasoning *) (**************************) -let prepare_intros dft = function +let prepare_intros dft destopt = function | None -> prepare_naming dloc dft, (fun _id -> Proofview.tclUNIT ()) - | Some (loc,ipat) -> prepare_intros_loc loc dft ipat + | Some (loc,ipat) -> prepare_intros_loc loc dft destopt ipat let ipat_of_name = function | Anonymous -> None | Name id -> Some (dloc, IntroNaming (IntroIdentifier id)) - let head_ident c = +let head_ident c = let c = fst (decompose_app ((strip_lam_assum c))) in if isVar c then Some (destVar c) else None -let assert_as first ipat c = - let naming,tac = prepare_intros IntroAnonymous ipat in - let repl = do_replace (head_ident c) naming in - if first then assert_before_then_gen repl naming c tac - else assert_after_then_gen repl naming c tac +let assert_as first hd ipat t = + let naming,tac = prepare_intros IntroAnonymous MoveLast ipat in + let repl = do_replace hd naming in + let tac = if repl then (fun id -> Proofview.tclUNIT ()) else tac in + if first then assert_before_then_gen repl naming t tac + else assert_after_then_gen repl naming t tac (* apply in as *) @@ -2222,13 +2289,18 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars let tac (naming,lemma) tac id = apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming id lemma tac in - let naming,ipat_tac = prepare_intros (IntroIdentifier id) ipat in + Proofview.Goal.enter begin fun gl -> + let destopt = + if with_evars then MoveLast (* evars would depend on the whole context *) + else get_previous_hyp_position id gl in + let naming,ipat_tac = prepare_intros (IntroIdentifier id) destopt ipat in let lemmas_target, last_lemma_target = let last,first = List.sep_last lemmas in List.map (fun lem -> (NamingMustBe (dloc,id),lem)) first, (naming,last) in (* We chain apply_in_once, ending with an intro pattern *) List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id + end (* if sidecond_first then @@ -2287,7 +2359,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in - let sigma, _ = Typing.e_type_of env sigma term in + let sigma, _ = Typing.type_of env sigma term in sigma, term, Tacticals.New.tclTHEN (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false) @@ -2373,16 +2445,17 @@ let forward b usetac ipat c = match usetac with | None -> Proofview.Goal.enter begin fun gl -> - let t = Tacmach.New.pf_type_of gl c in - Tacticals.New.tclTHENFIRST (assert_as true ipat t) + let t = Tacmach.New.pf_unsafe_type_of gl c in + let hd = head_ident c in + Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (Proofview.V82.tactic (exact_no_check c)) end | Some tac -> if b then - Tacticals.New.tclTHENFIRST (assert_as b ipat c) tac + Tacticals.New.tclTHENFIRST (assert_as b None ipat c) tac else Tacticals.New.tclTHENS3PARTS - (assert_as b ipat c) [||] tac [|Tacticals.New.tclIDTAC|] + (assert_as b None ipat c) [||] tac [|Tacticals.New.tclIDTAC|] let pose_proof na c = forward true None (ipat_of_name na) c let assert_by na t tac = forward true (Some tac) (ipat_of_name na) t @@ -2408,11 +2481,13 @@ let bring_hyps hyps = else Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in + let store = Proofview.Goal.extra gl in let concl = Tacmach.New.pf_nf_concl gl in let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in let args = Array.of_list (instance_from_named_context hyps) in Proofview.Refine.refine begin fun sigma -> - let (sigma, ev) = Evarutil.new_evar env sigma newcl in + let (sigma, ev) = + Evarutil.new_evar env sigma ~principal:true ~store newcl in (sigma, (mkApp (ev, args))) end end @@ -2456,7 +2531,7 @@ let generalize_goal_gen env ids i ((occs,c,b),na) t (cl,evd) = mkProd_or_LetIn (na,b,t) cl', evd' let generalize_goal gl i ((occs,c,b),na as o) cl = - let t = pf_type_of gl c in + let t = pf_unsafe_type_of gl c in let env = pf_env gl in generalize_goal_gen env (pf_ids_of_hyps gl) i o t cl @@ -2517,7 +2592,7 @@ let new_generalize_gen_let lconstr = let (newcl, sigma), args = List.fold_right_i (fun i ((_,c,b),_ as o) (cl, args) -> - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in let args = if Option.is_empty b then c :: args else args in generalize_goal_gen env ids i o t cl, args) 0 lconstr ((concl, sigma), []) @@ -2794,7 +2869,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = let id = match kind_of_term c with | Var id -> id | _ -> - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN @@ -3043,7 +3118,7 @@ let make_up_names n ind_opt cname = let error_ind_scheme s = let s = if not (String.is_empty s) then s^" " else s in - error ("Cannot recognize "^s^"an induction scheme.") + errorlabstrm "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.") let glob = Universes.constr_of_global @@ -3178,7 +3253,7 @@ let is_defined_variable env id = match lookup_named id env with | (_, Some _, _) -> true let abstract_args gl generalize_vars dep id defined f args = - let sigma = project gl in + let sigma = ref (project gl) in let env = pf_env gl in let concl = pf_concl gl in let dep = dep || dependent (mkVar id) concl in @@ -3195,11 +3270,12 @@ let abstract_args gl generalize_vars dep id defined f args = *) let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg = let (name, _, ty), arity = - let rel, c = Reductionops.splay_prod_n env sigma 1 prod in + let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in List.hd rel, c in - let argty = pf_type_of gl arg in - let ty = (* refresh_universes_strict *) ty in + let argty = pf_unsafe_type_of gl arg in + let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in + let () = sigma := sigma' in let lenctx = List.length ctx in let liftargty = lift lenctx argty in let leq = constr_cmp Reduction.CUMUL liftargty ty in @@ -3238,8 +3314,9 @@ let abstract_args gl generalize_vars dep id defined f args = true, mkApp (f', before), after in if dogen then + let tyf' = pf_unsafe_type_of gl f' in let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = - Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' + Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' in let args, refls = List.rev args, List.rev refls in let vars = @@ -3248,9 +3325,12 @@ let abstract_args gl generalize_vars dep id defined f args = hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars else [] in - let body, c' = if defined then Some c', typ_of ctxenv Evd.empty c' else None, c' in - Some (make_abstract_generalize gl id concl dep ctx body c' eqs args refls, - dep, succ (List.length ctx), vars) + let body, c' = + if defined then Some c', typ_of ctxenv !sigma c' + else None, c' + in + let term = make_abstract_generalize {gl with sigma = !sigma} id concl dep ctx body c' eqs args refls in + Some (term, !sigma, dep, succ (List.length ctx), vars) else None let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = @@ -3272,20 +3352,26 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = let newc = Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) gl in match newc with | None -> Proofview.tclUNIT () - | Some (newc, dep, n, vars) -> + | Some (newc, sigma, dep, n, vars) -> let tac = if dep then - Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro; - Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))] - else - Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); Proofview.V82.tactic (clear [id]); Tacticals.New.tclDO n intro] + Tacticals.New.tclTHENLIST + [Proofview.Unsafe.tclEVARS sigma; + Proofview.V82.tactic (refine newc); + rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro; + Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))] + else Tacticals.New.tclTHENLIST + [Proofview.Unsafe.tclEVARS sigma; + Proofview.V82.tactic (refine newc); + Proofview.V82.tactic (clear [id]); + Tacticals.New.tclDO n intro] in if List.is_empty vars then tac else Tacticals.New.tclTHEN tac (Tacticals.New.tclFIRST [revert vars ; Proofview.V82.tactic (fun gl -> tclMAP (fun id -> - tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)]) + tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)]) end let rec compare_upto_variables x y = @@ -3563,13 +3649,13 @@ let guess_elim isrec dep s hyp0 gl = Tacmach.New.pf_apply build_case_analysis_scheme gl mind true s else Tacmach.New.pf_apply build_case_analysis_scheme_default gl mind s in - let elimt = Tacmach.New.pf_type_of gl elimc in + let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in evd, ((elimc, NoBindings), elimt), mkIndU mind let given_elim hyp0 (elimc,lbind as e) gl = let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in - Proofview.Goal.sigma gl, (e, Tacmach.New.pf_type_of gl elimc), ind_type_guess + Proofview.Goal.sigma gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess type scheme_signature = (Id.t list * (elim_arg_kind * bool * Id.t) list) array @@ -3594,14 +3680,17 @@ let find_induction_type isrec elim hyp0 gl = if Option.is_empty scheme.indarg then error "Cannot find induction type"; let indsign = compute_scheme_signature scheme hyp0 ind_guess in let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in - scheme, ElimUsing (elim,indsign) in - (Option.get scheme.indref,scheme.nparams, elim) + scheme, ElimUsing (elim,indsign) + in + match scheme.indref with + | None -> error_ind_scheme "" + | Some ref -> ref, scheme.nparams, elim let get_elim_signature elim hyp0 gl = compute_elim_signature (given_elim hyp0 elim gl) hyp0 let is_functional_induction elimc gl = - let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_type_of gl (fst elimc)) in + let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in (* The test is not safe: with non-functional induction on non-standard induction scheme, this may fail *) Option.is_empty scheme.indarg @@ -3960,7 +4049,7 @@ let induction_gen_l isrec with_evars elim names lc = | _ -> Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let x = id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in @@ -4222,7 +4311,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = Proofview.Goal.enter begin fun gl -> - let ctype = Tacmach.New.pf_type_of gl (mkVar id) in + let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in let sign,t = decompose_prod_assum ctype in Proofview.tclORELSE begin @@ -4273,7 +4362,7 @@ let prove_transitivity hdcncl eq_kind t = | HeterogenousEq (typ1,c1,typ2,c2) -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let type_of = Typing.type_of env sigma in + let type_of = Typing.unsafe_type_of env sigma in let typt = type_of t in (mkApp(hdcncl, [| typ1; c1; typt ;t |]), mkApp(hdcncl, [| typt; t; typ2; c2 |])) @@ -4374,13 +4463,13 @@ let abstract_subproof id gk tac = let cd = Entries.DefinitionEntry const in let decl = (cd, IsProof Lemma) in (** ppedrot: seems legit to have abstracted subproofs as local*) - let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in let evd = Evd.set_universe_context evd ectx in - let open Declareops in - let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in - let effs = cons_side_effects eff + let open Safe_typing in + let eff = private_con_of_con (Global.safe_env ()) cst in + let effs = add_private eff Entries.(snd (Future.force const.const_entry_body)) in let args = List.rev (instance_from_named_context sign) in let solve = -- cgit v1.2.3