diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 50 | ||||
| -rw-r--r-- | tactics/auto.mli | 4 | ||||
| -rw-r--r-- | tactics/autorewrite.ml | 18 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 110 | ||||
| -rw-r--r-- | tactics/contradiction.ml | 26 | ||||
| -rw-r--r-- | tactics/eauto.ml | 34 | ||||
| -rw-r--r-- | tactics/elim.ml | 16 | ||||
| -rw-r--r-- | tactics/elimschemes.ml | 9 | ||||
| -rw-r--r-- | tactics/eqdecide.ml | 40 | ||||
| -rw-r--r-- | tactics/eqschemes.ml | 9 | ||||
| -rw-r--r-- | tactics/equality.ml | 161 | ||||
| -rw-r--r-- | tactics/hints.ml | 8 | ||||
| -rw-r--r-- | tactics/hipattern.mli | 6 | ||||
| -rw-r--r-- | tactics/inv.ml | 36 | ||||
| -rw-r--r-- | tactics/leminv.ml | 9 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 85 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 10 | ||||
| -rw-r--r-- | tactics/tactics.ml | 871 | ||||
| -rw-r--r-- | tactics/tactics.mli | 10 |
19 files changed, 713 insertions, 799 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index e213965485..272cb1edaa 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -97,11 +97,11 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = in clenv, c let unify_resolve poly flags ((c : raw_hint), clenv) = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let clenv, c = connect_hint_clenv poly c clenv gl in let clenv = clenv_unique_resolver ~flags clenv gl in Clenvtac.clenv_refine false clenv - end } + end let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h @@ -110,12 +110,12 @@ let unify_resolve_gen poly = function | Some flags -> unify_resolve poly flags let exact poly (c,clenv) = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let clenv', c = connect_hint_clenv poly c clenv gl in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (exact_check c) - end } + end (* Util *) @@ -141,7 +141,7 @@ let conclPattern concl pat tac = with Constr_matching.PatternMatchingFailure -> Tacticals.New.tclZEROMSG (str "pattern-matching failed") in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in constr_bindings env sigma >>= fun constr_bindings -> @@ -157,7 +157,7 @@ let conclPattern concl pat tac = match tac with | GenArg (Glbwit wit, tac) -> Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ()) - end } + end (***********************************************************) (** A debugging / verbosity framework for trivial and auto *) @@ -313,7 +313,7 @@ let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption let rec trivial_fail_db dbg mod_delta db_list local_db = let intro_tac = Tacticals.New.tclTHEN (dbg_intro dbg) - ( Proofview.Goal.enter { enter = begin fun gl -> + ( Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let nf c = Evarutil.nf_evar sigma c in @@ -322,9 +322,9 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = let hintl = make_resolve_hyp env sigma hyp in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list env sigma hintl local_db) - end }) + end) in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Tacmach.New.pf_concl gl in let sigma = Tacmach.New.project gl in let secvars = compute_secvars gl in @@ -332,7 +332,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = ((dbg_assumption dbg)::intro_tac:: (List.map Tacticals.New.tclCOMPLETE (trivial_resolve sigma dbg mod_delta db_list local_db secvars concl))) - end } + end and my_find_search_nodelta sigma db_list local_db secvars hdc concl = List.map (fun hint -> (None,hint)) @@ -375,7 +375,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.Goal.enter { enter = fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf") } + | ERes_pf _ -> Proofview.Goal.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 @@ -384,11 +384,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.Goal.enter { enter = begin fun gl -> + Proofview.Goal.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 } + end | Extern tacast -> conclPattern concl p tacast in @@ -417,7 +417,7 @@ and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl = "nocore" amongst the databases. *) let trivial ?(debug=Off) lems dbnames = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let db_list = make_db_list dbnames in @@ -425,10 +425,10 @@ let trivial ?(debug=Off) lems dbnames = let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (trivial_fail_db d false db_list hints) - end } + end let full_trivial ?(debug=Off) lems = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let db_list = current_pure_db () in @@ -436,7 +436,7 @@ let full_trivial ?(debug=Off) lems = let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (trivial_fail_db d false db_list hints) - end } + end let gen_trivial ?(debug=Off) lems = function | None -> full_trivial ~debug lems @@ -469,10 +469,10 @@ let extend_local_db decl db gl = let intro_register dbg kont db = Tacticals.New.tclTHEN (dbg_intro dbg) - (Proofview.Goal.enter { enter = begin fun gl -> + (Proofview.Goal.enter begin fun gl -> let extend_local_db decl db = extend_local_db decl db gl in Tacticals.New.onLastDecl (fun decl -> kont (extend_local_db decl db)) - end }) + end) (* n is the max depth of search *) (* local_db contains the local Hypotheses *) @@ -485,7 +485,7 @@ let search d n mod_delta db_list local_db = if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else Tacticals.New.tclORELSE0 (dbg_assumption d) (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db) - ( Proofview.Goal.enter { enter = begin fun gl -> + ( Proofview.Goal.enter begin fun gl -> let concl = Tacmach.New.pf_concl gl in let sigma = Tacmach.New.project gl in let secvars = compute_secvars gl in @@ -494,7 +494,7 @@ let search d n mod_delta db_list local_db = (List.map (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db)) (possible_resolve sigma d mod_delta db_list local_db secvars concl)) - end })) + end)) end [] in search d n local_db @@ -502,7 +502,7 @@ let search d n mod_delta db_list local_db = let default_search_depth = ref 5 let delta_auto debug mod_delta n lems dbnames = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let db_list = make_db_list dbnames in @@ -510,7 +510,7 @@ let delta_auto debug mod_delta n lems dbnames = let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (search d n mod_delta db_list hints) - end } + end let delta_auto = if Flags.profile then @@ -525,7 +525,7 @@ let new_auto ?(debug=Off) n = delta_auto debug true n let default_auto = auto !default_search_depth [] [] let delta_full_auto ?(debug=Off) mod_delta n lems = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let db_list = current_pure_db () in @@ -533,7 +533,7 @@ let delta_full_auto ?(debug=Off) mod_delta n lems = let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (search d n mod_delta db_list hints) - end } + end let full_auto ?(debug=Off) n = delta_full_auto ~debug false n let new_full_auto ?(debug=Off) n = delta_full_auto ~debug true n diff --git a/tactics/auto.mli b/tactics/auto.mli index 9ed9f0ae26..a6fb82bab2 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -16,14 +16,14 @@ open Decl_kinds open Hints open Tactypes -val compute_secvars : ('a,'b) Proofview.Goal.t -> Id.Pred.t +val compute_secvars : 'a Proofview.Goal.t -> Id.Pred.t val default_search_depth : int ref val auto_flags_of_state : transparent_state -> Unification.unify_flags val connect_hint_clenv : polymorphic -> raw_hint -> clausenv -> - ('a, 'r) Proofview.Goal.t -> clausenv * constr + 'a Proofview.Goal.t -> clausenv * constr (** Try unification with the precompiled clause, then use registered Apply *) val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index de544fe5f9..2d4f202769 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -15,7 +15,6 @@ open CErrors open Util open Mod_subst open Locus -open Proofview.Notations (* Rewriting rules *) type rew_rule = { rew_lemma: constr; @@ -90,15 +89,14 @@ type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_gen let one_base general_rewrite_maybe_in tac_main bas = let lrul = find_rewrites bas in let try_rewrite dir ctx c tc = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c in - let sigma = Sigma.to_evar_map sigma in let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in - let tac = general_rewrite_maybe_in dir c' tc in - Sigma.Unsafe.of_pair (tac, sigma) - end } in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (general_rewrite_maybe_in dir c' tc) + end in let lrul = List.map (fun h -> let tac = match h.rew_tac with | None -> Proofview.tclUNIT () @@ -125,7 +123,7 @@ let autorewrite ?(conds=Naive) tac_main lbas = (Proofview.tclUNIT()) lbas)) let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (* let's check at once if id exists (to raise the appropriate error) *) let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in let general_rewrite_in id dir cstr tac = @@ -137,7 +135,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = (List.fold_left (fun tac bas -> Tacticals.New.tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) (Proofview.tclUNIT()) lbas))) idl - end } + end let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id] @@ -162,10 +160,10 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = | None -> (* try to rewrite in all hypothesis (except maybe the rewritten one) *) - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let ids = Tacmach.New.pf_ids_of_hyps gl in try_do_hyps (fun id -> id) ids - end }) + end) let auto_multi_rewrite ?(conds=Naive) lems cl = Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds (Proofview.tclUNIT()) lems cl) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 672f9cffb5..de49a521fd 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -211,7 +211,7 @@ let auto_unif_flags freeze st = let e_give_exact flags poly (c,clenv) = let open Tacmach.New in - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = project gl in let (c, _, _) = c in let c, sigma = @@ -223,34 +223,34 @@ let e_give_exact flags poly (c,clenv) = else c, sigma in 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 } + Proofview.Unsafe.tclEVARS sigma <*> + Clenvtac.unify ~flags t1 <*> exact_no_check c + end let clenv_unique_resolver_tac with_evars ~flags clenv' = - Proofview.Goal.enter { enter = begin fun gls -> + Proofview.Goal.enter begin fun gls -> let resolve = try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls) with e -> Proofview.tclZERO e in resolve >>= fun clenv' -> Clenvtac.clenv_refine with_evars ~with_classes:false clenv' - end } + end -let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) -> +let unify_e_resolve poly flags = begin fun gls (c,_,clenv) -> let clenv', c = connect_hint_clenv poly c clenv gls in - clenv_unique_resolver_tac true ~flags clenv' end } + clenv_unique_resolver_tac true ~flags clenv' end -let unify_resolve poly flags = { enter = begin fun gls (c,_,clenv) -> +let unify_resolve poly flags = begin fun gls (c,_,clenv) -> let clenv', _ = connect_hint_clenv poly c clenv gls in clenv_unique_resolver_tac false ~flags clenv' - end } + end (** Application of a lemma using [refine] instead of the old [w_unify] *) let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) = let open Clenv in let env = Proofview.Goal.env gls in let concl = Proofview.Goal.concl gls in - Refine.refine ~unsafe:true { Sigma.run = fun sigma -> - let sigma = Sigma.to_evar_map sigma in + Refine.refine ~unsafe:true begin fun sigma -> let sigma, term, ty = if poly then let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in @@ -266,7 +266,7 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) = let sigma' = Evarconv.the_conv_x_leq env ~ts:flags.core_unify_flags.modulo_delta cl.cl_concl concl sigma' - in Sigma.here term (Sigma.Unsafe.of_evar_map sigma') } + in (sigma', term) end let unify_resolve_refine poly flags gl clenv = Proofview.tclORELSE @@ -297,32 +297,31 @@ let clenv_of_prods poly nprods (c, clenv) gl = let with_prods nprods poly (c, clenv) f = if get_typeclasses_limit_intros () then - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> try match clenv_of_prods poly nprods (c, clenv) gl with | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses") - | Some (diff, clenv') -> f.enter gl (c, diff, clenv') + | Some (diff, clenv') -> f gl (c, diff, clenv') with e when CErrors.noncritical e -> - Tacticals.New.tclZEROMSG (CErrors.print e) end } + Tacticals.New.tclZEROMSG (CErrors.print e) end else Proofview.Goal.enter - { enter = begin fun gl -> - if Int.equal nprods 0 then f.enter gl (c, None, clenv) - else Tacticals.New.tclZEROMSG (str"Not enough premisses") end } + begin fun gl -> + if Int.equal nprods 0 then f gl (c, None, clenv) + else Tacticals.New.tclZEROMSG (str"Not enough premisses") end let matches_pattern concl pat = let matches env sigma = match pat with | None -> Proofview.tclUNIT () | Some pat -> - let sigma = Sigma.to_evar_map sigma in if Constr_matching.is_matching env sigma pat concl then Proofview.tclUNIT () else Tacticals.New.tclZEROMSG (str "pattern does not match") in - Proofview.Goal.enter { enter = fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - matches env sigma } + matches env sigma end (** Semantics of type class resolution lemma application: @@ -363,7 +362,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars = let open Tacticals.New in let open Tacmach.New in let trivial_fail = - Proofview.Goal.enter { enter = + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -371,15 +370,15 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars = let hintl = make_resolve_hyp env sigma d in let hints = Hint_db.add_list env sigma hintl local_db in e_trivial_fail_db only_classes db_list hints secvars - end } + end in let trivial_resolve = - Proofview.Goal.enter { enter = + Proofview.Goal.enter begin fun gl -> let tacs = e_trivial_resolve db_list local_db secvars only_classes (project gl) (pf_concl gl) in tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs) - end} + end in let tacl = Eauto.registered_e_assumption :: @@ -418,9 +417,9 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co if get_typeclasses_filtered_unification () then let tac = with_prods nprods poly (term,cl) - ({ enter = fun gl clenv -> + (fun gl clenv -> matches_pattern concl p <*> - unify_resolve_refine poly flags gl clenv}) + unify_resolve_refine poly flags gl clenv) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else let tac = @@ -433,9 +432,9 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co | ERes_pf (term,cl) -> if get_typeclasses_filtered_unification () then let tac = (with_prods nprods poly (term,cl) - ({ enter = fun gl clenv -> + (fun gl clenv -> matches_pattern concl p <*> - unify_resolve_refine poly flags gl clenv})) in + unify_resolve_refine poly flags gl clenv)) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else let tac = @@ -450,7 +449,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co let tac = matches_pattern concl p <*> Proofview.Goal.nf_enter - { enter = fun gl -> unify_resolve_refine poly flags gl (c,None,clenv) } in + (fun gl -> unify_resolve_refine poly flags gl (c,None,clenv)) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else e_give_exact flags poly (c,clenv) @@ -1039,16 +1038,16 @@ module Search = struct sigma goals let fail_if_nonclass info = - Proofview.Goal.enter { enter = fun gl -> + Proofview.Goal.enter begin fun gl -> let gl = Proofview.Goal.assume gl in - let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let sigma = Proofview.Goal.sigma gl in if is_class_type sigma (Proofview.Goal.concl gl) then Proofview.tclUNIT () else (if !typeclasses_debug > 1 then Feedback.msg_debug (pr_depth info.search_depth ++ str": failure due to non-class subgoal " ++ pr_ev sigma (Proofview.Goal.goal gl)); - Proofview.tclZERO NoApplicableEx) } + Proofview.tclZERO NoApplicableEx) end (** The general hint application tactic. tac1 + tac2 .... The choice of OR or ORELSE is determined @@ -1060,18 +1059,17 @@ module Search = struct let env = Goal.env gl in let concl = Goal.concl gl in let sigma = Goal.sigma gl in - let s = Sigma.to_evar_map sigma in - let unique = not info.search_dep || is_unique env s concl in - let backtrack = needs_backtrack env s unique concl in + let unique = not info.search_dep || is_unique env sigma concl in + let backtrack = needs_backtrack env sigma unique concl in if !typeclasses_debug > 0 then Feedback.msg_debug (pr_depth info.search_depth ++ str": looking for " ++ - Printer.pr_econstr_env (Goal.env gl) s concl ++ + Printer.pr_econstr_env (Goal.env gl) sigma concl ++ (if backtrack then str" with backtracking" else str" without backtracking")); let secvars = compute_secvars gl in let poss = - e_possible_resolve hints info.search_hints secvars info.search_only_classes s concl in + e_possible_resolve hints info.search_hints secvars info.search_only_classes sigma concl in (* If no goal depends on the solution of this one or the instances are irrelevant/assumed to be unique, then we don't need to backtrack, as long as no evar appears in the goal @@ -1089,7 +1087,7 @@ module Search = struct pr_depth (idx :: info.search_depth) ++ str": " ++ Lazy.force pp ++ (if !foundone != true then - str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal (Proofview.Goal.assume gl)) + str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal (Proofview.Goal.assume gl)) else mt ()) in let msg = @@ -1104,15 +1102,14 @@ module Search = struct Feedback.msg_debug (header ++ str " failed with: " ++ msg) else () in - let tac_of gls i j = Goal.enter { enter = fun gl' -> + let tac_of gls i j = Goal.enter begin fun gl' -> let sigma' = Goal.sigma gl' in - let s' = Sigma.to_evar_map sigma' in let _concl = Goal.concl gl' in if !typeclasses_debug > 0 then Feedback.msg_debug (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++ - pr_ev s' (Proofview.Goal.goal (Proofview.Goal.assume gl'))); - let eq c1 c2 = EConstr.eq_constr s' c1 c2 in + pr_ev sigma' (Proofview.Goal.goal (Proofview.Goal.assume gl'))); + let eq c1 c2 = EConstr.eq_constr sigma' c1 c2 in let hints' = if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl)) then @@ -1120,7 +1117,7 @@ module Search = struct make_autogoal_hints info.search_only_classes ~st gl' else info.search_hints in - let dep' = info.search_dep || Proofview.unifiable s' (Goal.goal (Proofview.Goal.assume gl')) gls in + let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal (Proofview.Goal.assume gl')) gls in let info' = { search_depth = succ j :: i :: info.search_depth; last_tac = pp; @@ -1128,7 +1125,7 @@ module Search = struct search_only_classes = info.search_only_classes; search_hints = hints'; search_cut = derivs } - in kont info' } + in kont info' end in let rec result (shelf, ()) i k = foundone := true; @@ -1137,7 +1134,7 @@ module Search = struct (if !typeclasses_debug > 0 then Feedback.msg_debug (pr_depth (i :: info.search_depth) ++ str": " ++ Lazy.force pp - ++ str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal (Proofview.Goal.assume gl)) + ++ str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal (Proofview.Goal.assume gl)) ++ str", " ++ int j ++ str" subgoal(s)" ++ (Option.cata (fun k -> str " in addition to the first " ++ int k) (mt()) k))); @@ -1207,7 +1204,7 @@ module Search = struct if !foundone == false && !typeclasses_debug > 0 then Feedback.msg_debug (pr_depth info.search_depth ++ str": no match for " ++ - Printer.pr_econstr_env (Goal.env gl) s concl ++ + Printer.pr_econstr_env (Goal.env gl) sigma concl ++ str ", " ++ int (List.length poss) ++ str" possibilities"); match e with @@ -1219,18 +1216,17 @@ module Search = struct let hints_tac hints info kont : unit Proofview.tactic = Proofview.Goal.enter - { enter = fun gl -> hints_tac_gl hints info kont gl } + (fun gl -> hints_tac_gl hints info kont gl) let intro_tac info kont gl = let open Proofview in let env = Goal.env gl in let sigma = Goal.sigma gl in - let s = Sigma.to_evar_map sigma in let decl = Tacmach.New.pf_last_hyp gl in let hint = - make_resolve_hyp env s (Hint_db.transparent_state info.search_hints) + make_resolve_hyp env sigma (Hint_db.transparent_state info.search_hints) (true,false,false) info.search_only_classes empty_hint_info decl in - let ldb = Hint_db.add_list env s hint info.search_hints in + let ldb = Hint_db.add_list env sigma hint info.search_hints in let info' = { info with search_hints = ldb; last_tac = lazy (str"intro"); search_depth = 1 :: 1 :: info.search_depth } @@ -1238,7 +1234,7 @@ module Search = struct let intro info kont = Proofview.tclBIND Tactics.intro - (fun _ -> Proofview.Goal.enter { enter = fun gl -> intro_tac info kont gl }) + (fun _ -> Proofview.Goal.enter (fun gl -> intro_tac info kont gl)) let rec search_tac hints limit depth = let kont info = @@ -1271,8 +1267,8 @@ module Search = struct let open Proofview in let tac sigma gls i = Goal.enter - { enter = fun gl -> - search_tac_gl ~st only_classes dep hints depth (succ i) sigma gls gl } + begin fun gl -> + search_tac_gl ~st only_classes dep hints depth (succ i) sigma gls gl end in Proofview.Unsafe.tclGETGOALS >>= fun gls -> Proofview.tclEVARMAP >>= fun sigma -> @@ -1627,13 +1623,13 @@ let is_ground c = let autoapply c i = let open Proofview.Notations in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let flags = auto_unif_flags Evar.Set.empty (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in let cty = Tacmach.New.pf_unsafe_type_of gl c in let ce = mk_clenv_from gl (c,cty) in - (unify_e_resolve false flags).enter gl + unify_e_resolve false flags gl ((c,cty,Univ.ContextSet.empty),0,ce) <*> Proofview.tclEVARMAP >>= (fun sigma -> let sigma = Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals sigma in - Proofview.Unsafe.tclEVARS sigma) end } + Proofview.Unsafe.tclEVARS sigma) end diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 5e7090ded1..83c2be4106 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -25,22 +25,20 @@ let mk_absurd_proof coq_not t = mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|]))) let absurd c = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map sigma in let j = Retyping.get_judgment_of env sigma c in let sigma, j = Coercion.inh_coerce_to_sort env sigma j in let t = j.Environ.utj_val in - let tac = + Proofview.Unsafe.tclEVARS sigma <*> Tacticals.New.pf_constr_of_global (build_coq_not ()) >>= fun coqnot -> Tacticals.New.pf_constr_of_global (build_coq_False ()) >>= fun coqfalse -> Tacticals.New.tclTHENLIST [ elim_type coqfalse; Simple.apply (mk_absurd_proof coqnot t) - ] in - Sigma.Unsafe.of_pair (tac, sigma) - end } + ] + end let absurd c = absurd c @@ -54,13 +52,13 @@ let filter_hyp f tac = | [] -> Proofview.tclZERO Not_found | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d) | _::rest -> seek rest in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in seek hyps - end } + end let contradiction_context = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let rec seek_neg l = match l with @@ -89,11 +87,11 @@ let contradiction_context = | None -> Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type.")) (Proofview.tclORELSE - (Proofview.Goal.enter { enter = begin fun gl -> + (Proofview.Goal.enter begin fun gl -> let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in filter_hyp (fun typ -> is_conv_leq typ t) (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|]))) - end }) + end) begin function (e, info) -> match e with | Not_found -> seek_neg rest | e -> Proofview.tclZERO ~info e @@ -102,7 +100,7 @@ let contradiction_context = in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in seek_neg hyps - end } + end let is_negation_of env sigma typ t = match EConstr.kind sigma (whd_all env sigma t) with @@ -111,7 +109,7 @@ let is_negation_of env sigma typ t = | _ -> false let contradiction_term (c,lbind as cl) = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in @@ -134,7 +132,7 @@ let contradiction_term (c,lbind as cl) = | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.") | e -> Proofview.tclZERO ~info e end - end } + end let contradiction = function | None -> Tacticals.New.tclTHEN intros contradiction_context diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 986f531397..bae3344612 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -30,27 +30,27 @@ open Proofview.Notations let eauto_unif_flags = auto_flags_of_state full_transparent_state let e_give_exact ?(flags=eauto_unif_flags) c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let t1 = Tacmach.New.pf_unsafe_type_of gl c in let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in let sigma = Tacmach.New.project gl in if occur_existential sigma t1 || occur_existential sigma t2 then Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) else exact_check c - end } + end let assumption id = e_give_exact (mkVar id) let e_assumption = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl)) - end } + end let registered_e_assumption = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id)) (Tacmach.New.pf_ids_of_hyps gl)) - end } + end (************************************************************************) (* PROLOG tactic *) @@ -93,7 +93,7 @@ let out_term = function let prolog_tac l n = Proofview.V82.tactic begin fun gl -> let map c = - let (c, sigma) = Tactics.run_delayed (pf_env gl) (project gl) c in + let (sigma, c) = c (pf_env gl) (project gl) in let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in out_term c in @@ -112,13 +112,13 @@ open Auto let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l) let unify_e_resolve poly flags (c,clenv) = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let clenv', c = connect_hint_clenv poly c clenv gl in let clenv' = clenv_unique_resolver ~flags clenv' gl in Proofview.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (Tactics.Simple.eapply c) - end } + end let hintmap_of sigma secvars hdc concl = match hdc with @@ -130,20 +130,20 @@ let hintmap_of sigma secvars hdc concl = (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) let e_exact poly flags (c,clenv) = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let clenv', c = connect_hint_clenv poly c clenv gl in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (e_give_exact c) - end } + end let rec e_trivial_fail_db db_list local_db = - let next = Proofview.Goal.enter { enter = begin fun gl -> + let next = Proofview.Goal.enter begin fun gl -> let d = Tacmach.New.pf_last_hyp gl in let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Tacmach.New.project gl) d in e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db) - end } in - Proofview.Goal.enter { enter = begin fun gl -> + end in + Proofview.Goal.enter begin fun gl -> let secvars = compute_secvars gl in let tacl = registered_e_assumption :: @@ -151,7 +151,7 @@ let rec e_trivial_fail_db db_list local_db = (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl))) in Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) - end } + end and e_my_find_search sigma db_list local_db secvars hdc concl = let hint_of_db = hintmap_of sigma secvars hdc concl in @@ -497,7 +497,7 @@ let unfold_head env sigma (ids, csts) c = in aux c let autounfold_one db cl = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in @@ -517,4 +517,4 @@ let autounfold_one db cl = | Some hyp -> change_in_hyp None (make_change_arg c') hyp | None -> convert_concl_no_check c' DEFAULTcast else Tacticals.New.tclFAIL 0 (str "Nothing to unfold") - end } + end diff --git a/tactics/elim.ml b/tactics/elim.ml index 855cb206fe..13d64b8e3f 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -77,7 +77,7 @@ let tmphyp_name = Id.of_string "_TmpHyp" let up_to_delta = ref false (* true *) let general_decompose recognizer c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let type_of = pf_unsafe_type_of gl in let sigma = project gl in let typc = type_of c in @@ -87,7 +87,7 @@ let general_decompose recognizer c = (ifOnHyp (recognizer sigma) (general_decompose_aux (recognizer sigma)) (fun id -> clear [id]))); exact_no_check c ] - end } + end let head_in indl t gl = let env = Proofview.Goal.env gl in @@ -101,10 +101,10 @@ let head_in indl t gl = with Not_found -> false let decompose_these c l = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let indl = List.map (fun x -> x, Univ.Instance.empty) l in general_decompose (fun sigma (_,t) -> head_in indl t gl) c - end } + end let decompose_and c = general_decompose @@ -132,7 +132,7 @@ let induction_trailer abs_i abs_j bargs = (tclDO (abs_j - abs_i) intro) (onLastHypId (fun id -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let idty = pf_unsafe_type_of gl (mkVar id) in let fvty = global_vars (pf_env gl) (project gl) idty in let possible_bring_hyps = @@ -150,11 +150,11 @@ let induction_trailer abs_i abs_j bargs = let ids = List.rev (ids_of_named_context hyps) in (tclTHENLIST [revert ids; simple_elimination (mkVar id)]) - end } + end )) let double_ind h1 h2 = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let abs_i = depth_of_quantified_hypothesis true h1 gl in let abs_j = depth_of_quantified_hypothesis true h2 gl in let abs = @@ -167,7 +167,7 @@ let double_ind h1 h2 = (fun id -> elimination_then (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) - end } + end let h_double_induction = double_ind diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 93073fdc7e..466b1350d9 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -18,7 +18,6 @@ open Indrec open Declarations open Typeops open Ind_tables -open Sigma.Notations (* Induction/recursion schemes *) @@ -109,10 +108,10 @@ let rec_dep_scheme_kind_from_type = let build_case_analysis_scheme_in_type dep sort ind = let env = Global.env () in - let sigma = Sigma.Unsafe.of_evar_map (Evd.from_env env) in - let Sigma (indu, sigma, _) = Sigma.fresh_inductive_instance env sigma ind in - let Sigma (c, sigma, _) = build_case_analysis_scheme env sigma indu dep sort in - c, Evd.evar_universe_context (Sigma.to_evar_map sigma) + let sigma = Evd.from_env env in + let (sigma, indu) = Evd.fresh_inductive_instance env sigma ind in + let (sigma, c) = build_case_analysis_scheme env sigma indu dep sort in + c, Evd.evar_universe_context sigma let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 48ce52f092..0cee4b6edb 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -23,7 +23,6 @@ open Tacticals.New open Auto open Constr_matching open Misctypes -open Tactypes open Hipattern open Proofview.Notations open Tacmach.New @@ -66,22 +65,20 @@ let choose_noteq eqonleft = else left_with_bindings false Misctypes.NoBindings -open Sigma.Notations - (* A surgical generalize which selects the right occurrences by hand *) (* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *) let generalize_right mk typ c1 c2 = - Proofview.Goal.enter { Proofview.Goal.enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in - Refine.refine ~unsafe:true { Sigma.run = begin fun sigma -> + Refine.refine ~unsafe:true begin fun sigma -> let na = Name (next_name_away_with_default "x" Anonymous (Termops.ids_of_context env)) in let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in - let Sigma (x, sigma, p) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in - Sigma (mkApp (x, [|c2|]), sigma, p) - end } - end } + let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in + (sigma, mkApp (x, [|c2|])) + end + end let mkBranches (eqonleft,mk,c1,c2,typ) = tclTHENLIST @@ -93,7 +90,7 @@ let mkBranches (eqonleft,mk,c1,c2,typ) = intros] let discrHyp id = - let c = { delayed = fun env sigma -> Sigma.here (mkVar id, NoBindings) sigma } in + let c env sigma = (sigma, (mkVar id, NoBindings)) in let tac c = Equality.discr_tac false (Some (None, ElimOnConstr c)) in Tacticals.New.tclDELAYEDWITHHOLES false c tac @@ -138,7 +135,7 @@ let eqCase tac = tclTHEN intro (onLastHypId tac) let injHyp id = - let c = { delayed = fun env sigma -> Sigma.here (mkVar id, NoBindings) sigma } in + let c env sigma = (sigma, (mkVar id, NoBindings)) in let tac c = Equality.injClause None false (Some (None, ElimOnConstr c)) in Tacticals.New.tclDELAYEDWITHHOLES false c tac @@ -189,7 +186,7 @@ let rec solveArg hyps eqonleft mk largs rargs = match largs, rargs with intros_reflexivity; ] | a1 :: largs, a2 :: rargs -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let rectype = pf_unsafe_type_of gl a1 in let decide = mk rectype a1 a2 in let tac hyp = solveArg (hyp :: hyps) eqonleft mk largs rargs in @@ -197,13 +194,13 @@ let rec solveArg hyps eqonleft mk largs rargs = match largs, rargs with if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto] else [diseqCase hyps eqonleft;eqCase tac;default_auto] in (tclTHENS (elim_type decide) subtacs) - end } + end | _ -> invalid_arg "List.fold_right2" let solveEqBranch rectype = Proofview.tclORELSE begin - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = pf_concl gl in let sigma = project gl in match_eqdec sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) -> @@ -212,8 +209,9 @@ let solveEqBranch rectype = let getargs l = List.skipn nparams (snd (decompose_app sigma l)) in let rargs = getargs rhs and largs = getargs lhs in + solveArg [] eqonleft mk largs rargs - end } + end end begin function (e, info) -> match e with | PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!") @@ -229,7 +227,7 @@ let hd_app sigma c = match EConstr.kind sigma c with let decideGralEquality = Proofview.tclORELSE begin - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = pf_concl gl in let sigma = project gl in match_eqdec sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) -> @@ -241,7 +239,7 @@ let decideGralEquality = (tclTHEN (mkBranches data) (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype))) - end } + end end begin function (e, info) -> match e with | PatternMatchingFailure -> @@ -252,10 +250,10 @@ let decideGralEquality = let decideEqualityGoal = tclTHEN intros decideGralEquality let decideEquality rectype ops = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let decide = mkGenDecideEqGoal rectype ops gl in (tclTHENS (cut decide) [default_auto;decideEqualityGoal]) - end } + end (* The tactic Compare *) @@ -264,7 +262,7 @@ let compare c1 c2 = pf_constr_of_global (build_coq_sumbool ()) >>= fun opc -> pf_constr_of_global (Coqlib.build_coq_eq ()) >>= fun eqc -> pf_constr_of_global (build_coq_not ()) >>= fun notc -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let rectype = pf_unsafe_type_of gl c1 in let ops = (opc,eqc,notc) in let decide = mkDecideEqGoal true ops rectype c1 c2 in @@ -272,4 +270,4 @@ let compare c1 c2 = [(tclTHEN intro (tclTHEN (onLastHyp simplest_case) clear_last)); decideEquality rectype ops]) - end } + end diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 507ff10eea..efcefcf16a 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -57,7 +57,6 @@ open Namegen open Inductiveops open Ind_tables open Indrec -open Sigma.Notations open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -656,10 +655,10 @@ let fix_r2l_forward_rew_scheme (c, ctx') = (**********************************************************************) let build_r2l_rew_scheme dep env ind k = - let sigma = Sigma.Unsafe.of_evar_map (Evd.from_env env) in - let Sigma (indu, sigma, _) = Sigma.fresh_inductive_instance env sigma ind in - let Sigma (c, sigma, _) = build_case_analysis_scheme env sigma indu dep k in - c, Evd.evar_universe_context (Sigma.to_evar_map sigma) + let sigma = Evd.from_env env in + let (sigma, indu) = Evd.fresh_inductive_instance env sigma ind in + let (sigma, c) = build_case_analysis_scheme env sigma indu dep k in + c, Evd.evar_universe_context sigma let build_l2r_rew_scheme = build_l2r_rew_scheme let build_l2r_forward_rew_scheme = build_l2r_forward_rew_scheme diff --git a/tactics/equality.ml b/tactics/equality.ml index d64cc38eff..05c5cd5ec1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -40,7 +40,6 @@ open Eqschemes open Locus open Locusops open Misctypes -open Sigma.Notations open Proofview.Notations open Unification open Context.Named.Declaration @@ -254,16 +253,16 @@ let rewrite_keyed_unif_flags = { } let rewrite_elim with_evars frzevars cls c e = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let flags = if Unification.is_keyed_unification () then rewrite_keyed_unif_flags else rewrite_conv_closed_unif_flags in let flags = make_flags frzevars (Tacmach.New.project gl) flags c in general_elim_clause with_evars flags cls c e - end } + end let tclNOTSAMEGOAL tac = let goal gl = Proofview.Goal.goal (Proofview.Goal.assume gl) in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let sigma = project gl in let ev = goal gl in tac >>= fun () -> @@ -278,7 +277,7 @@ let tclNOTSAMEGOAL tac = tclZEROMSG (str"Tactic generated a subgoal identical to the original goal.") else Proofview.tclUNIT () - end } + end (* Ad hoc asymmetric general_elim_clause *) let general_elim_clause with_evars frzevars cls rew elim = @@ -313,7 +312,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim = (general_elim_clause with_evars frzevars cls c elim)) tac in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let instantiate_lemma concl = if not all then instantiate_lemma gl c t l l2r concl else instantiate_lemma_all frzevars gl c t l l2r concl @@ -325,7 +324,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim = let cs = instantiate_lemma typ in if firstonly then tclFIRST (List.map try_clause cs) else tclMAP try_clause cs - end } + end (* The next function decides in particular whether to try a regular rewrite or a generalized rewrite. @@ -387,9 +386,9 @@ let find_elim hdcncl lft2rgt dep cls ot gl = Logic.eq or Jmeq just before *) assert false in - let Sigma (elim, sigma, p) = Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in + let (sigma, elim) = fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in let elim = EConstr.of_constr elim in - Sigma ((elim, Safe_typing.empty_private_constants), sigma, p) + (sigma, (elim, Safe_typing.empty_private_constants)) else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case *) @@ -407,11 +406,11 @@ let find_elim hdcncl lft2rgt dep cls ot gl = | Ind (ind,u) -> let c, eff = find_scheme scheme_name ind in (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *) - let Sigma (elim, sigma, p) = - Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) + let (sigma, elim) = + fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in let elim = EConstr.of_constr elim in - Sigma ((elim, eff), sigma, p) + (sigma, (elim, eff)) | _ -> assert false let type_of_clause cls gl = match cls with @@ -419,21 +418,19 @@ let type_of_clause cls gl = match cls with | Some id -> pf_get_hyp_typ id gl let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl = - Proofview.Goal.s_enter { s_enter = begin fun gl -> - let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + Proofview.Goal.enter begin fun gl -> + let evd = Proofview.Goal.sigma gl in let isatomic = isProd evd (whd_zeta evd hdcncl) in let dep_fun = if isatomic then dependent else dependent_no_evar in let type_of_cls = type_of_clause cls gl in let dep = dep_proof_ok && dep_fun evd c type_of_cls in - let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in - let tac = + let (sigma, (elim, effs)) = find_elim hdcncl lft2rgt dep cls (Some t) gl in + Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclEFFECTS effs <*> general_elim_clause with_evars frzevars tac cls c t l (match lft2rgt with None -> false | Some b -> b) {elimindex = None; elimbody = (elim,NoBindings); elimrename = None} - in - Sigma (tac, sigma, p) - end } + end let adjust_rewriting_direction args lft2rgt = match args with @@ -456,7 +453,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac if occs != AllOccurrences then ( rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac) else - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let ctype = get_type_of env sigma c in @@ -485,7 +482,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac | None -> Proofview.tclZERO ~info e (* error "The provided term does not end with an equality or a declared rewrite relation." *) end - end } + end let general_rewrite_ebindings = general_rewrite_ebindings_clause None @@ -547,9 +544,9 @@ let general_rewrite_clause l2r with_evars ?tac c cl = let ids_of_hyps = pf_ids_of_hyps gl in Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> do_hyps_atleastonce (ids gl) - end } + end in if cl.concl_occs == NoOccurrences then do_hyps else tclIFTHENTRYELSEMUST @@ -557,25 +554,25 @@ let general_rewrite_clause l2r with_evars ?tac c cl = do_hyps let apply_special_clear_request clear_flag f = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in try - let ((c, bl), sigma) = run_delayed env sigma f in + let (sigma, (c, bl)) = f env sigma in apply_clear_request clear_flag (use_clear_hyp_by_default ()) c with e when catchable_exception e -> tclIDTAC - end } + end let general_multi_rewrite with_evars l cl tac = let do1 l2r f = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let (c, sigma) = run_delayed env sigma f in + let (sigma, c) = f env sigma in tclWITHHOLES with_evars (general_rewrite_clause l2r with_evars ?tac c cl) sigma - end } + end in let rec doN l2r c = function | Precisely n when n <= 0 -> Proofview.tclUNIT () @@ -638,7 +635,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = | None -> Proofview.tclUNIT () | Some tac -> tclCOMPLETE tac in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let get_type_of = pf_apply get_type_of gl in let t1 = get_type_of c1 and t2 = get_type_of c2 in @@ -664,7 +661,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = tclTHEN (apply sym) assumption; try_prove_eq ]) - end } + end let replace c1 c2 = replace_using_leibniz onConcl c2 c1 false false None @@ -934,13 +931,9 @@ let build_selector env sigma dirn c ind special default = let ci = make_case_info env ind RegularStyle in sigma, mkCase (ci, p, c, Array.of_list brl) -let new_global sigma gr = - let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr - in Sigma.to_evar_map sigma, c - -let build_coq_False sigma = new_global sigma (build_coq_False ()) -let build_coq_True sigma = new_global sigma (build_coq_True ()) -let build_coq_I sigma = new_global sigma (build_coq_I ()) +let build_coq_False sigma = Evarutil.new_global sigma (build_coq_False ()) +let build_coq_True sigma = Evarutil.new_global sigma (build_coq_True ()) +let build_coq_I sigma = Evarutil.new_global sigma (build_coq_I ()) let rec build_discriminator env sigma dirn c = function | [] -> @@ -967,7 +960,7 @@ let rec build_discriminator env sigma dirn c = function *) let gen_absurdity id = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = project gl in let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in if is_empty_type sigma hyp_typ @@ -975,7 +968,7 @@ let gen_absurdity id = simplest_elim (mkVar id) else tclZEROMSG (str "Not the negation of an equality.") - end } + end (* Precondition: eq is leibniz equality @@ -1032,17 +1025,17 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in match find_positions env sigma ~no_discr:false t1 t2 with | Inr _ -> tclZEROMSG (str"Not a discriminable equality.") | Inl (cpath, (_,dirn), _) -> discr_positions env sigma u eq_clause cpath dirn - end } + end let onEquality with_evars tac (c,lbindc) = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let type_of = pf_unsafe_type_of gl in let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in let t = type_of c in @@ -1054,10 +1047,10 @@ let onEquality with_evars tac (c,lbindc) = tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) (tac (eq,eqn,eq_args) eq_clause') - end } + end let onNegatedEquality with_evars tac = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let ccl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in @@ -1068,7 +1061,7 @@ let onNegatedEquality with_evars tac = onEquality with_evars tac (mkVar id,NoBindings))) | _ -> tclZEROMSG (str "Not a negated primitive equality.") - end } + end let discrSimpleClause with_evars = function | None -> onNegatedEquality with_evars discrEq @@ -1327,7 +1320,7 @@ let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined") let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k) let inject_if_homogenous_dependent_pair ty = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> try let sigma = Tacmach.New.project gl in let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in @@ -1367,7 +1360,7 @@ let inject_if_homogenous_dependent_pair ty = ])] with Exit -> Proofview.tclUNIT () - end } + end (* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it expands then only when the whdnf has a constructor of an inductive type @@ -1451,7 +1444,7 @@ let injEq ?(old=false) with_evars clear_flag ipats = let post_tac c n = match ipats_style with | Some ipats -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = project gl in let destopt = match EConstr.kind sigma c with | Var id -> get_previous_hyp_position id gl @@ -1464,7 +1457,7 @@ let injEq ?(old=false) with_evars clear_flag ipats = then intro_patterns_bound_to with_evars n destopt ipats else intro_patterns_to with_evars destopt ipats in tclTHEN clear_tac intro_tac - end } + end | None -> tclIDTAC in injEqThen post_tac l2r @@ -1482,7 +1475,7 @@ let injConcl = injClause None false None let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.tag id))) let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = clause.evd in let env = Proofview.Goal.env gl in match find_positions env sigma ~no_discr:false t1 t2 with @@ -1493,7 +1486,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = | Inr posns -> inject_at_positions env sigma true u clause posns (ntac (clenv_value clause)) - end } + end let dEqThen with_evars ntac = function | None -> onNegatedEquality with_evars (decompEqThen (ntac None)) @@ -1504,10 +1497,10 @@ let dEq with_evars = (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)) let intro_decomp_eq tac data (c, t) = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in decompEqThen (fun _ -> tac) data cl - end } + end let _ = declare_intro_decomp_eq intro_decomp_eq @@ -1558,7 +1551,6 @@ let decomp_tuple_term env sigma c t = in decomprec (mkRel 1) c t let subst_tuple_term env sigma dep_pair1 dep_pair2 b = - let sigma = Sigma.to_evar_map sigma in let typ = get_type_of env sigma dep_pair1 in (* We find all possible decompositions *) let decomps1 = decomp_tuple_term env sigma dep_pair1 typ in @@ -1583,7 +1575,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* Retype to get universes right *) let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in let sigma, _ = Typing.type_of env sigma body in - Sigma.Unsafe.of_pair ((body, expected_goal), sigma) + (sigma, (body, expected_goal)) (* Like "replace" but decompose dependent equalities *) (* i.e. if equality is "exists t v = exists u w", and goal is "phi(t,u)", *) @@ -1591,42 +1583,38 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* on for further iterated sigma-tuples *) let cutSubstInConcl l2r eqn = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in let typ = pf_concl gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in - let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in - let tac = - tclTHENFIRST + let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in + tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (tclTHENFIRST (tclTHENLIST [ (change_concl typ); (* Put in pattern form *) (replace_core onConcl l2r eqn) ]) - (change_concl expected) (* Put in normalized form *) - in - Sigma (tac, sigma, p) - end } + (change_concl expected)) (* Put in normalized form *) + end let cutSubstInHyp l2r eqn id = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in let typ = pf_get_hyp_typ id gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in - let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in - let tac = - tclTHENFIRST + let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in + tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (tclTHENFIRST (tclTHENLIST [ (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly)); (replace_core (onHyp id) l2r eqn) ]) - (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly)) - in - Sigma (tac, sigma, p) - end } + (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly))) + end let try_rewrite tac = Proofview.tclORELSE tac begin function (e, info) -> match e with @@ -1648,11 +1636,11 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id) let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None let substClause l2r c cls = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let eq = pf_apply get_type_of gl c in tclTHENS (cutSubstClause l2r eq cls) [Proofview.tclUNIT (); exact_no_check c] - end } + end let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls) let rewriteInHyp l2r c id = rewriteClause l2r c (Some id) @@ -1713,7 +1701,7 @@ let is_eq_x gl x d = erase hyp and x; proceed by generalizing all dep hyps *) let subst_one dep_proof_ok x (hyp,rhs,dir) = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in @@ -1742,13 +1730,13 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = else [Proofview.tclUNIT ()]) @ [tclTRY (clear [x; hyp])]) - end } + end (* Look for an hypothesis hyp of the form "x=rhs" or "rhs=x", rewrite it everywhere, and erase hyp and x; proceed by generalizing all dep hyps *) let subst_one_var dep_proof_ok x = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let gl = Proofview.Goal.assume gl in let decl = pf_get_hyp x gl in (* If x has a body, simply replace x with body and clear x *) @@ -1765,7 +1753,7 @@ let subst_one_var dep_proof_ok x = str".") with FoundHyp res -> res in subst_one dep_proof_ok x res - end } + end let subst_gen dep_proof_ok ids = tclMAP (subst_one_var dep_proof_ok) ids @@ -1818,7 +1806,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = (* Second step: treat equations *) let process hyp = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let gl = Proofview.Goal.assume gl in let sigma = project gl in let env = Proofview.Goal.env gl in @@ -1834,19 +1822,19 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> Proofview.tclUNIT () - end } + end in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let ids = find_equations gl in tclMAP process ids - end } + end else (* Old implementation, not able to manage configurations like a=b, a=t, or situations like "a = S b, b = S a", or also accidentally unfolding let-ins *) - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = project gl in let find_eq_data_decompose = find_eq_data_decompose gl in let test (_,c) = @@ -1865,7 +1853,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let ids = List.map_filter test hyps in let ids = List.uniquize ids in subst_gen flags.rewrite_dependent_proof ids - end } + end (* Rewrite the first assumption for which a condition holds and gives the direction of the rewrite *) @@ -1902,11 +1890,10 @@ let rewrite_assumption_cond cond_eq_term cl = with | Failure _ | UserError _ -> arec rest gl end in - Proofview.Goal.enter { enter = begin fun gl -> - let gl = Proofview.Goal.lift gl Sigma.Unsafe.le in + Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps gl in arec hyps gl - end } + end (* Generalize "subst x" to substitution of subterm appearing as an equation in the context, but not clearing the hypothesis *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 70e62eabac..773abb9f0c 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -22,7 +22,6 @@ open Namegen open Libnames open Smartlocate open Misctypes -open Tactypes open Termops open Inductiveops open Typing @@ -34,7 +33,6 @@ open Pfedit open Tacred open Printer open Vernacexpr -open Sigma.Notations module NamedDecl = Context.Named.Declaration @@ -1363,11 +1361,7 @@ let add_hint_lemmas env sigma eapply lems hint_db = Hint_db.add_list env sigma hintlist' hint_db let make_local_hint_db env sigma ts eapply lems = - let map c = - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (c, sigma, _) = c.delayed env sigma in - (Sigma.to_evar_map sigma, c) - in + let map c = c env sigma in let lems = List.map map lems in let sign = EConstr.named_context env in let ts = match ts with diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 9110830aae..a1d986544a 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -120,11 +120,11 @@ val match_with_equation: (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *) -val find_eq_data_decompose : ('a, 'r) Proofview.Goal.t -> constr -> +val find_eq_data_decompose : 'a Proofview.Goal.t -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** Idem but fails with an error message instead of PatternMatchingFailure *) -val find_this_eq_data_decompose : ('a, 'r) Proofview.Goal.t -> constr -> +val find_this_eq_data_decompose : 'a Proofview.Goal.t -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** A variant that returns more informative structure on the equality found *) @@ -145,7 +145,7 @@ val is_matching_sigma : evar_map -> constr -> bool val match_eqdec : evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) -val dest_nf_eq : ('a, 'r) Proofview.Goal.t -> constr -> (constr * constr * constr) +val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr) (** Match a negation *) val is_matching_not : evar_map -> constr -> bool diff --git a/tactics/inv.ml b/tactics/inv.ml index b951e7ceba..ec038f638e 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -25,7 +25,6 @@ open Tactics open Elim open Equality open Misctypes -open Sigma.Notations open Proofview.Notations module NamedDecl = Context.Named.Declaration @@ -272,14 +271,14 @@ Nota: with Inversion_clear, only four useless hypotheses let generalizeRewriteIntros as_mode tac depids id = Proofview.tclENV >>= fun env -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let dids = dependent_hyps env id depids gl in let reintros = if as_mode then intros_replacing else intros_possibly_replacing in (tclTHENLIST [bring_hyps dids; tac; (* may actually fail to replace if dependent in a previous eq *) reintros (ids_of_named_context dids)]) - end } + end let error_too_many_names pats = let loc = Loc.merge_opt (fst (List.hd pats)) (fst (List.last pats)) in @@ -287,7 +286,7 @@ let error_too_many_names pats = tclZEROMSG ?loc ( str "Unexpected " ++ str (String.plural (List.length pats) "introduction pattern") ++ - str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (fst (run_delayed env Evd.empty c))))) pats ++ + str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ str ".") let get_names (allow_conj,issimple) (loc, pat as x) = match pat with @@ -341,7 +340,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC)) in let substHypIfVariable tac id = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = project gl in (** We only look at the type of hypothesis "id" *) let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in @@ -350,7 +349,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2 | _ -> tac id - end } + end in let deq_trailer id clear_flag _ neqns = assert (clear_flag == None); @@ -377,7 +376,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = id let nLastDecls i tac = - Proofview.Goal.enter { enter = begin fun gl -> tac (nLastDecls gl i) end } + Proofview.Goal.enter begin fun gl -> tac (nLastDecls gl i) end (* Introduction of the equations on arguments othin: discriminates Simple Inversion, Inversion and Inversion_clear @@ -385,7 +384,7 @@ let nLastDecls i tac = Some thin: the equations are rewritten, and cleared if thin is true *) let rewrite_equations as_mode othin neqns names ba = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in let first_eq = ref MoveLast in let avoid = if as_mode then List.map NamedDecl.get_id nodepids else [] in @@ -418,7 +417,7 @@ let rewrite_equations as_mode othin neqns names ba = [tclDO neqns intro; bring_hyps nodepids; clear (ids_of_named_context nodepids)]) - end } + end let interp_inversion_kind = function | SimpleInversion -> None @@ -435,9 +434,8 @@ let rewrite_equations_tac as_mode othin id neqns names ba = tac let raw_inversion inv_kind id status names = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let c = mkVar id in @@ -462,11 +460,11 @@ let raw_inversion inv_kind id status names = in let refined id = let prf = mkApp (mkVar id, args) in - Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) } + Refine.refine (fun h -> (h, prf)) in let neqns = List.length realargs in let as_mode = names != None in - let tac = + tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENS (assert_before Anonymous cut_concl) [case_tac names @@ -474,9 +472,7 @@ let raw_inversion inv_kind id status names = (rewrite_equations_tac as_mode inv_kind id neqns)) (Some elim_predicate) ind (c,t); onLastHypId (fun id -> tclTHEN (refined id) reflexivity)]) - in - Sigma.Unsafe.of_pair (tac, sigma) - end } + end (* Error messages of the inversion tactics *) let wrap_inv_error id = function (e, info) -> match e with @@ -516,13 +512,13 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id) * back to their places in the hyp-list. *) let invIn k names ids id = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let hyps = List.map (fun id -> pf_get_hyp id gl) ids in let concl = Proofview.Goal.concl gl in let sigma = project gl in let nb_prod_init = nb_prod sigma concl in let intros_replace_ids = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = pf_concl gl in let sigma = project gl in let nb_of_new_hyp = @@ -532,7 +528,7 @@ let invIn k names ids id = intros_replacing ids else tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids) - end } + end in Proofview.tclORELSE (tclTHENLIST @@ -540,7 +536,7 @@ let invIn k names ids id = inversion k NoDep names id; intros_replace_ids]) (wrap_inv_error id) - end } + end let invIn_gen k names idl = try_intros_until (invIn k names idl) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 83f3da30a9..87d815fc81 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -27,7 +27,6 @@ open Declare open Tacticals.New open Tactics open Decl_kinds -open Proofview.Notations open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -261,7 +260,7 @@ let add_inversion_lemma_exn na com comsort bool tac = (* ================================= *) let lemInv id c = - Proofview.Goal.enter { enter = begin fun gls -> + Proofview.Goal.enter begin fun gls -> try 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 @@ -274,12 +273,12 @@ let lemInv id c = user_err ~hdr:"LemInv" (str "Cannot refine current goal with the lemma " ++ pr_leconstr_env (pf_env gls) (project gls) c) - end } + end 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 -> + Proofview.Goal.enter begin fun gl -> let hyps = List.map (fun id -> pf_get_hyp id gl) ids in let intros_replace_ids = let concl = Proofview.Goal.concl gl in @@ -292,7 +291,7 @@ let lemInvIn id c ids = in ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c)) (intros_replace_ids))) - end } + end let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index a7eadc3c3e..aa574e41c5 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -17,7 +17,6 @@ open Declarations open Tacmach open Clenv open Tactypes -open Sigma.Notations module NamedDecl = Context.Named.Declaration @@ -511,12 +510,12 @@ module New = struct Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if let tclDELAYEDWITHHOLES check x tac = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let Sigma (x, sigma, _) = x.delayed env sigma in - tclWITHHOLES check (tac x) (Sigma.to_evar_map sigma) - end } + let (sigma, x) = x env sigma in + tclWITHHOLES check (tac x) sigma + end let tclTIMEOUT n t = Proofview.tclOR @@ -547,66 +546,66 @@ module New = struct mkVar (nthHypId m gl) let onNthHypId m tac = - Proofview.Goal.enter { enter = begin fun gl -> tac (nthHypId m gl) end } + Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end let onNthHyp m tac = - Proofview.Goal.enter { enter = begin fun gl -> tac (nthHyp m gl) end } + Proofview.Goal.enter begin fun gl -> tac (nthHyp m gl) end let onLastHypId = onNthHypId 1 let onLastHyp = onNthHyp 1 let onNthDecl m tac = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> Proofview.tclUNIT (nthDecl m gl) >>= tac - end } + end let onLastDecl = onNthDecl 1 let ifOnHyp pred tac1 tac2 id = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let typ = Tacmach.New.pf_get_hyp_typ id gl in if pred (id,typ) then tac1 id else tac2 id - end } + end - let onHyps find tac = Proofview.Goal.enter { enter = begin fun gl -> tac (find.enter gl) end } + let onHyps find tac = Proofview.Goal.enter begin fun gl -> tac (find gl) end let afterHyp id tac = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in let rem, _ = List.split_when (NamedDecl.get_id %> Id.equal id) hyps in tac rem - end } + end let fullGoal gl = let hyps = Tacmach.New.pf_ids_of_hyps gl in None :: List.map Option.make hyps let tryAllHyps tac = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let hyps = Tacmach.New.pf_ids_of_hyps gl in tclFIRST_PROGRESS_ON tac hyps - end } + end let tryAllHypsAndConcl tac = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> tclFIRST_PROGRESS_ON tac (fullGoal gl) - end } + end let onClause tac cl = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let hyps = Tacmach.New.pf_ids_of_hyps gl in tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl) - end } + end (* Find the right elimination suffix corresponding to the sort of the goal *) (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim isrec allnames tac predicate ind (c, t) = - Proofview.Goal.enter { enter = begin fun gl -> - let sigma, elim = (mk_elim ind).enter gl in + Proofview.Goal.enter begin fun gl -> + let sigma, elim = mk_elim ind gl in let ind = on_snd (fun u -> EInstance.kind sigma u) ind in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Proofview.Goal.enter { enter = begin fun gl -> + (Proofview.Goal.enter begin fun gl -> let indclause = mk_clenv_from gl (c, t) in (* applying elimination_scheme just a little modified *) let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim) in @@ -655,7 +654,7 @@ module New = struct Proofview.tclTHEN (Clenvtac.clenv_refine false clenv') (Proofview.tclEXTEND [] tclIDTAC branchtacs) - end }) end } + end) end let elimination_sort_of_goal gl = (** Retyping will expand evars anyway. *) @@ -673,29 +672,29 @@ module New = struct (* computing the case/elim combinators *) - let gl_make_elim ind = { enter = begin fun gl -> + let gl_make_elim ind = begin fun gl -> let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in let (sigma, c) = pf_apply Evd.fresh_global gl gr in (sigma, EConstr.of_constr c) - end } + end - let gl_make_case_dep (ind, u) = { enter = begin fun gl -> - let sigma = Sigma.Unsafe.of_evar_map (project gl) in + let gl_make_case_dep (ind, u) = begin fun gl -> + let sigma = project gl in let u = EInstance.kind (project gl) u in - let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true + let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true (elimination_sort_of_goal gl) in - (Sigma.to_evar_map sigma, EConstr.of_constr r) - end } + (sigma, EConstr.of_constr r) + end - let gl_make_case_nodep (ind, u) = { enter = begin fun gl -> - let sigma = Sigma.Unsafe.of_evar_map (project gl) in - let u = EInstance.kind (project gl) u in - let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false + let gl_make_case_nodep (ind, u) = begin fun gl -> + let sigma = project gl in + let u = EInstance.kind sigma u in + let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false (elimination_sort_of_goal gl) in - (Sigma.to_evar_map sigma, EConstr.of_constr r) - end } + (sigma, EConstr.of_constr r) + end let make_elim_branch_assumptions ba hyps = let assums = @@ -704,19 +703,19 @@ module New = struct { ba = ba; assums = assums } let elim_on_ba tac ba = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in tac branches - end } + end let case_on_ba tac ba = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in tac branches - end } + end let elimination_then tac c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with @@ -724,7 +723,7 @@ module New = struct | Some _ -> false,gl_make_case_dep in general_elim_then_using mkelim isrec None tac None ind (c, t) - end } + end let case_then_using = general_elim_then_using gl_make_case_dep false diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 96270f748e..9603212de6 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -225,7 +225,7 @@ module New : sig val tclTIMEOUT : int -> unit tactic -> unit tactic val tclTIME : string option -> 'a tactic -> 'a tactic - val nLastDecls : ('a, 'r) Proofview.Goal.t -> int -> named_context + val nLastDecls : 'a Proofview.Goal.t -> int -> named_context val ifOnHyp : (identifier * types -> bool) -> (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> @@ -236,7 +236,7 @@ module New : sig val onLastHyp : (constr -> unit tactic) -> unit tactic val onLastDecl : (named_declaration -> unit tactic) -> unit tactic - val onHyps : ([ `LZ ], named_context) Proofview.Goal.enter -> + val onHyps : ([ `LZ ] Proofview.Goal.t -> named_context) -> (named_context -> unit tactic) -> unit tactic val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic @@ -244,9 +244,9 @@ module New : sig val tryAllHypsAndConcl : (identifier option -> unit tactic) -> unit tactic val onClause : (identifier option -> unit tactic) -> clause -> unit tactic - val elimination_sort_of_goal : ('a, 'r) Proofview.Goal.t -> sorts_family - val elimination_sort_of_hyp : Id.t -> ('a, 'r) Proofview.Goal.t -> sorts_family - val elimination_sort_of_clause : Id.t option -> ('a, 'r) Proofview.Goal.t -> sorts_family + val elimination_sort_of_goal : 'a Proofview.Goal.t -> sorts_family + val elimination_sort_of_hyp : Id.t -> 'a Proofview.Goal.t -> sorts_family + val elimination_sort_of_clause : Id.t option -> 'a Proofview.Goal.t -> sorts_family val elimination_then : (branch_args -> unit Proofview.tactic) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a93a86d3a3..b553f316c2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -43,9 +43,7 @@ open Unification open Locus open Locusops open Misctypes -open Tactypes open Proofview.Notations -open Sigma.Notations open Context.Named.Declaration module RelDecl = Context.Rel.Declaration @@ -55,7 +53,7 @@ let inj_with_occurrences e = (AllOccurrences,e) let typ_of env sigma c = let open Retyping in - try get_type_of ~lax:true env (Sigma.to_evar_map sigma) c + try get_type_of ~lax:true env sigma c with RetypeError e -> user_err (print_retype_error e) @@ -165,18 +163,18 @@ let _ = (** This tactic creates a partial proof realizing the introduction rule, but does not check anything. *) let unsafe_intro env store decl b = - Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~unsafe:true begin fun sigma -> let ctx = named_context_val env in let nctx = push_named_context_val decl ctx in let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in let ninst = mkRel 1 :: inst in let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in - let Sigma (ev, sigma, p) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in - Sigma (mkNamedLambda_or_LetIn decl ev, sigma, p) - end } + let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in + (sigma, mkNamedLambda_or_LetIn decl ev) + end let introduction ?(check=true) id = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in @@ -192,49 +190,48 @@ let introduction ?(check=true) id = | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b | _ -> raise (RefinerError IntroNeedsProduct) - end } + end let refine = Tacmach.refine let error msg = CErrors.user_err Pp.(str msg) let convert_concl ?(check=true) ty k = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in let conclty = Proofview.Goal.concl gl in - Refine.refine ~unsafe:true { run = begin fun sigma -> - let Sigma ((), sigma, p) = + Refine.refine ~unsafe:true begin fun sigma -> + let sigma = if check then begin - let sigma = Sigma.to_evar_map sigma in 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.Unsafe.of_pair ((), sigma) - end else Sigma.here () sigma in - let Sigma (x, sigma, q) = Evarutil.new_evar env sigma ~principal:true ~store ty in + sigma + end else sigma in + let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in - Sigma (ans, sigma, p +> q) - end } - end } + (sigma, ans) + end + end let convert_hyp ?(check=true) d = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ty = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in let sign = convert_hyp check (named_context_val env) sigma d in let env = reset_with_named_context sign env in - Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~unsafe:true begin fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty - end } - end } + end + end let convert_concl_no_check = convert_concl ~check:false let convert_hyp_no_check = convert_hyp ~check:false let convert_gen pb x y = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> try let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in if b then Proofview.Unsafe.tclEVARS sigma @@ -242,7 +239,7 @@ let convert_gen pb x y = with (* Reduction.NotConvertible *) _ -> (** FIXME: Sometimes an anomaly is raised from conversion *) Tacticals.New.tclFAIL 0 (str "Not convertible") -end } +end let convert x y = convert_gen Reduction.CONV x y let convert_leq x y = convert_gen Reduction.CUMUL x y @@ -282,7 +279,7 @@ let error_replacing_dependency env sigma id err = let clear_gen fail = function | [] -> Proofview.tclUNIT () | ids -> - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let ids = List.fold_right Id.Set.add ids Id.Set.empty in (** clear_hyps_in_evi does not require nf terms *) let gl = Proofview.Goal.assume gl in @@ -295,11 +292,11 @@ let clear_gen fail = function with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err in let env = reset_with_named_context hyps env in - let tac = Refine.refine ~unsafe:true { run = fun sigma -> + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) + (Refine.refine ~unsafe:true begin fun sigma -> Evarutil.new_evar env sigma ~principal:true concl - } in - Sigma.Unsafe.of_pair (tac, !evdref) - end } + end) + end let clear ids = clear_gen error_clear_dependency ids let clear_for_replacing ids = clear_gen error_replacing_dependency ids @@ -318,7 +315,7 @@ let apply_clear_request clear_flag dft c = (* Moving hypotheses *) let move_hyp id dest = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ty = Proofview.Goal.concl gl in @@ -326,10 +323,10 @@ let move_hyp id dest = let sign = named_context_val env in let sign' = move_hyp_in_named_context sigma id dest sign in let env = reset_with_named_context sign' env in - Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~unsafe:true begin fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty - end } - end } + end + end (* Renaming hypotheses *) let rename_hyp repl = @@ -348,7 +345,7 @@ let rename_hyp repl = match dom with | None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping") | Some (src, dst) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in @@ -380,10 +377,10 @@ let rename_hyp repl = let nconcl = subst concl in let nctx = val_of_named_context nhyps in let instance = List.map (NamedDecl.get_id %> mkVar) hyps in - Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~unsafe:true begin fun sigma -> Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance - end } - end } + end + end (**************************************************************) (* Fresh names *) @@ -447,7 +444,7 @@ let find_name mayrepl decl naming gl = match naming with let assert_before_then_gen b naming t tac = let open Context.Rel.Declaration in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let id = find_name b (LocalAssum (Anonymous,t)) naming gl in Tacticals.New.tclTHENLAST (Proofview.V82.tactic @@ -456,7 +453,7 @@ let assert_before_then_gen b naming t tac = with Evarutil.ClearDependencyError (id,err) -> error_replacing_dependency (pf_env gl) (project gl) id err)) (tac id) - end } + end let assert_before_gen b naming t = assert_before_then_gen b naming t (fun _ -> Proofview.tclUNIT ()) @@ -466,7 +463,7 @@ let assert_before_replacing id = assert_before_gen true (NamingMustBe (Loc.tag i let assert_after_then_gen b naming t tac = let open Context.Rel.Declaration in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let id = find_name b (LocalAssum (Anonymous,t)) naming gl in Tacticals.New.tclTHENFIRST (Proofview.V82.tactic @@ -475,7 +472,7 @@ let assert_after_then_gen b naming t tac = with Evarutil.ClearDependencyError (id,err) -> error_replacing_dependency (pf_env gl) (project gl) id err)) (tac id) - end } + end let assert_after_gen b naming t = assert_after_then_gen b naming t (fun _ -> (Proofview.tclUNIT ())) @@ -487,13 +484,12 @@ let assert_after_replacing id = assert_after_gen true (NamingMustBe (Loc.tag id) (* Fixpoints and CoFixpoints *) (**************************************************************) -let rec mk_holes : type r s. _ -> r Sigma.t -> (s, r) Sigma.le -> _ -> (_, s) Sigma.sigma = -fun env sigma p -> function -| [] -> Sigma ([], sigma, p) +let rec mk_holes env sigma = function +| [] -> (sigma, []) | arg :: rem -> - let Sigma (arg, sigma, q) = Evarutil.new_evar env sigma arg in - let Sigma (rem, sigma, r) = mk_holes env sigma (p +> q) rem in - Sigma (arg :: rem, sigma, r) + let (sigma, arg) = Evarutil.new_evar env sigma arg in + let (sigma, rem) = mk_holes env sigma rem in + (sigma, arg :: rem) let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast sigma cl) with | Prod (na, c1, b) -> @@ -511,7 +507,7 @@ let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast | _ -> error "Not enough products." (* Refine as a fixpoint *) -let mutual_fix f n rest j = Proofview.Goal.enter { enter = begin fun gl -> +let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in @@ -531,8 +527,8 @@ let mutual_fix f n rest j = Proofview.Goal.enter { enter = begin fun gl -> mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth in let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in - Refine.refine { run = begin fun sigma -> - let Sigma (evs, sigma, p) = mk_holes nenv sigma Sigma.refl (List.map pi3 all) in + Refine.refine begin fun sigma -> + let (sigma, evs) = mk_holes nenv sigma (List.map pi3 all) in let ids = List.map pi1 all in let evs = List.map (Vars.subst_vars (List.rev ids)) evs in let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in @@ -540,17 +536,17 @@ let mutual_fix f n rest j = Proofview.Goal.enter { enter = begin fun gl -> let typarray = Array.of_list (List.map pi3 all) in let bodies = Array.of_list evs in let oterm = mkFix ((indxs,0),(funnames,typarray,bodies)) in - Sigma (oterm, sigma, p) - end } -end } + (sigma, oterm) + end +end let fix ido n = match ido with | None -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let name = Pfedit.get_current_proof_name () in let id = new_fresh_id [] name gl in mutual_fix id n [] 0 - end } + end | Some id -> mutual_fix id n [] 0 @@ -567,7 +563,7 @@ let rec check_is_mutcoind env sigma cl = error "All methods must construct elements in coinductive types." (* Refine as a cofixpoint *) -let mutual_cofix f others j = Proofview.Goal.enter { enter = begin fun gl -> +let mutual_cofix f others j = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in @@ -583,25 +579,25 @@ let mutual_cofix f others j = Proofview.Goal.enter { enter = begin fun gl -> mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth in let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in - Refine.refine { run = begin fun sigma -> + Refine.refine begin fun sigma -> let (ids, types) = List.split all in - let Sigma (evs, sigma, p) = mk_holes nenv sigma Sigma.refl types in + let (sigma, evs) = mk_holes nenv sigma types in let evs = List.map (Vars.subst_vars (List.rev ids)) evs in let funnames = Array.of_list (List.map (fun i -> Name i) ids) in let typarray = Array.of_list types in let bodies = Array.of_list evs in let oterm = mkCoFix (0, (funnames, typarray, bodies)) in - Sigma (oterm, sigma, p) - end } -end } + (sigma, oterm) + end +end let cofix ido = match ido with | None -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let name = Pfedit.get_current_proof_name () in let id = new_fresh_id [] name gl in mutual_cofix id [] 0 - end } + end | Some id -> mutual_cofix id [] 0 @@ -693,14 +689,14 @@ let bind_red_expr_occurrences occs nbcl redexp = certain hypothesis *) let reduct_in_concl (redfun,sty) = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> convert_concl_no_check (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty - end } + end let reduct_in_hyp ?(check=false) redfun (id,where) = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> convert_hyp ~check (pf_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl) - end } + end let revert_cast (redfun,kind as r) = if kind == DEFAULTcast then (redfun,REVERTcast) else r @@ -714,30 +710,32 @@ let reduct_option ?(check=false) redfun = function let pf_e_reduce_decl redfun where decl gl = let open Context.Named.Declaration in let sigma = Proofview.Goal.sigma gl in - let redfun sigma c = redfun.e_redfun (Tacmach.New.pf_env gl) sigma c in + let redfun sigma c = redfun (Tacmach.New.pf_env gl) sigma c in match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then user_err (pr_id id ++ str " has no value."); - let Sigma (ty', sigma, p) = redfun sigma ty in - Sigma (LocalAssum (id, ty'), sigma, p) + let (sigma, ty') = redfun sigma ty in + (sigma, LocalAssum (id, ty')) | LocalDef (id,b,ty) -> - let Sigma (b', sigma, p) = if where != InHypTypeOnly then redfun sigma b else Sigma.here b sigma in - let Sigma (ty', sigma, q) = if where != InHypValueOnly then redfun sigma ty else Sigma.here ty sigma in - Sigma (LocalDef (id, b', ty'), sigma, p +> q) + let (sigma, b') = if where != InHypTypeOnly then redfun sigma b else (sigma, b) in + let (sigma, ty') = if where != InHypValueOnly then redfun sigma ty else (sigma, ty) in + (sigma, LocalDef (id, b', ty')) let e_reduct_in_concl ~check (redfun, sty) = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let Sigma (c', sigma, p) = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in - Sigma (convert_concl ~check c' sty, sigma, p) - end } + let (sigma, c') = redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (convert_concl ~check c' sty) + end let e_reduct_in_hyp ?(check=false) redfun (id, where) = - Proofview.Goal.s_enter { s_enter = begin fun gl -> - let Sigma (decl', sigma, p) = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in - Sigma (convert_hyp ~check decl', sigma, p) - end } + Proofview.Goal.enter begin fun gl -> + let (sigma, decl') = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (convert_hyp ~check decl') + end let e_reduct_option ?(check=false) redfun = function | Some id -> e_reduct_in_hyp ~check (fst redfun) id @@ -747,11 +745,12 @@ let e_reduct_option ?(check=false) redfun = function from conversions. *) let e_change_in_concl (redfun,sty) = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let Sigma (c, sigma, p) = redfun.e_redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.concl gl) in - Sigma (convert_concl_no_check c sty, sigma, p) - end } + let (sigma, c) = redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.concl gl) in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (convert_concl_no_check c sty) + end let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma = let open Context.Named.Declaration in @@ -759,29 +758,29 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm | LocalAssum (id,ty) -> if where == InHypValueOnly then user_err (pr_id id ++ str " has no value."); - let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma ty in - Sigma (LocalAssum (id, ty'), sigma, p) + let (sigma, ty') = redfun false env sigma ty in + (sigma, LocalAssum (id, ty')) | LocalDef (id,b,ty) -> - let Sigma (b', sigma, p) = - if where != InHypTypeOnly then (redfun true).e_redfun env sigma b else Sigma.here b sigma + let (sigma, b') = + if where != InHypTypeOnly then redfun true env sigma b else (sigma, b) in - let Sigma (ty', sigma, q) = - if where != InHypValueOnly then (redfun false).e_redfun env sigma ty else Sigma.here ty sigma + let (sigma, ty') = + if where != InHypValueOnly then redfun false env sigma ty else (sigma, ty) in - Sigma (LocalDef (id,b',ty'), sigma, p +> q) + (sigma, LocalDef (id,b',ty')) let e_change_in_hyp redfun (id,where) = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let hyp = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in - let Sigma (c, sigma, p) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in - Sigma (convert_hyp c, sigma, p) - end } + let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (convert_hyp c) + end -type change_arg = Pattern.patvar_map -> EConstr.constr Sigma.run +type change_arg = Pattern.patvar_map -> evar_map -> evar_map * EConstr.constr -let make_change_arg c pats = - { run = fun sigma -> Sigma.here (replace_vars (Id.Map.bindings pats) c) sigma } +let make_change_arg c pats sigma = (sigma, replace_vars (Id.Map.bindings pats) c) let check_types env sigma mayneedglobalcheck deep newc origc = let t1 = Retyping.get_type_of env sigma newc in @@ -805,33 +804,30 @@ let check_types env sigma mayneedglobalcheck deep newc origc = else sigma (* Now we introduce different instances of the previous tacticals *) -let change_and_check cv_pb mayneedglobalcheck deep t = { e_redfun = begin fun env sigma c -> - let Sigma (t', sigma, p) = t.run sigma in - let sigma = Sigma.to_evar_map sigma in +let change_and_check cv_pb mayneedglobalcheck deep t env sigma c = + let (sigma, t') = t sigma in let sigma = check_types env sigma mayneedglobalcheck deep t' c in let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible."); - Sigma.Unsafe.of_pair (t', sigma) -end } + (sigma, t') (* Use cumulativity only if changing the conclusion not a subterm *) -let change_on_subterm cv_pb deep t where = { e_redfun = begin fun env sigma c -> +let change_on_subterm cv_pb deep t where env sigma c = let mayneedglobalcheck = ref false in - let Sigma (c, sigma, p) = match where with - | None -> (change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty)).e_redfun env sigma c + let (sigma, c) = match where with + | None -> change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c | Some occl -> - (e_contextually false occl + e_contextually false occl (fun subst -> - change_and_check Reduction.CONV mayneedglobalcheck true (t subst))).e_redfun + change_and_check Reduction.CONV mayneedglobalcheck true (t subst)) env sigma c in if !mayneedglobalcheck then begin - try ignore (Typing.unsafe_type_of env (Sigma.to_evar_map 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; - Sigma (c, sigma, p) -end } + (sigma, c) let change_in_concl occl t = e_change_in_concl ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast) @@ -844,7 +840,7 @@ let change_option occl t = function | None -> change_in_concl occl t let change chg c cls = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in Tacticals.New.tclMAP (function | OnHyp (id,occs,where) -> @@ -852,7 +848,7 @@ let change chg c cls = | OnConcl occs -> change_option (bind_change_occurrences occs chg) c None) cls - end } + end let change_concl t = change_in_concl None (make_change_arg t) @@ -893,14 +889,14 @@ let reduce redexp cl = Pp.(hov 2 (Pputils.pr_red_expr pr str redexp)) in Proofview.Trace.name_tactic trace begin - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in let redexps = reduction_clause redexp cl' in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in Tacticals.New.tclMAP (fun (where,redexp) -> e_reduct_option ~check (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps - end } + end end (* Unfolding occurrences of a constant *) @@ -936,7 +932,7 @@ let build_intro_tac id dest tac = match dest with let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let open Context.Rel.Declaration in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in match EConstr.kind sigma concl with @@ -962,7 +958,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = Tacticals.New.tclZEROMSG (str "No product even after head-reduction.") | e -> Proofview.tclZERO ~info e end - end } + end let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ()) let intro_mustbe_force id = intro_gen (NamingMustBe (Loc.tag id)) MoveLast true false @@ -1027,14 +1023,14 @@ let get_previous_hyp_position id gl = aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) let intro_replacing id = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let next_hyp = get_next_hyp_position id gl in Tacticals.New.tclTHENLIST [ clear_for_replacing [id]; introduction id; move_hyp id next_hyp; ] - end } + end (* We have e.g. [x, y, y', x', y'' |- forall y y' y'', G] and want to reintroduce y, y,' y''. Note that we have to clear y, y' and y'' @@ -1046,7 +1042,7 @@ let intro_replacing id = (* the behavior of inversion *) let intros_possibly_replacing ids = let suboptimal = true in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in Tacticals.New.tclTHEN (Tacticals.New.tclMAP (fun id -> @@ -1055,16 +1051,16 @@ let intros_possibly_replacing ids = (Tacticals.New.tclMAP (fun (id,pos) -> Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id)) posl) - end } + end (* This version assumes that replacement is actually possible *) let intros_replacing ids = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in Tacticals.New.tclTHEN (clear_for_replacing ids) (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl) - end } + end (* User-level introduction tactics *) @@ -1078,7 +1074,7 @@ let lookup_hypothesis_as_renamed_gen red h gl = match lookup_hypothesis_as_renamed env (Tacmach.New.project gl) ccl h with | None when red -> let (redfun, _) = Redexpr.reduction_of_red_expr env (Red true) in - let Sigma (c, _, _) = redfun.e_redfun env (Proofview.Goal.sigma gl) ccl in + let (_, c) = redfun env (Proofview.Goal.sigma gl) ccl in aux c | x -> x in @@ -1108,10 +1104,10 @@ let depth_of_quantified_hypothesis red h gl = str".") let intros_until_gen red h = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let n = depth_of_quantified_hypothesis red h gl in Tacticals.New.tclDO n (if red then introf else intro) - end } + end let intros_until_id id = intros_until_gen false (NamedHyp id) let intros_until_n_gen red n = intros_until_gen red (AnonHyp n) @@ -1120,10 +1116,10 @@ let intros_until = intros_until_gen true let intros_until_n = intros_until_n_gen true let tclCHECKVAR id = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let _ = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in Proofview.tclUNIT () - end } + end let try_intros_until_id_check id = Tacticals.New.tclORELSE (intros_until_id id) (tclCHECKVAR id) @@ -1138,9 +1134,6 @@ let rec intros_move = function Tacticals.New.tclTHEN (intro_gen (NamingMustBe (Loc.tag hyp)) destopt false false) (intros_move rest) -let run_delayed env sigma c = - Sigma.run sigma { Sigma.run = fun sigma -> c.delayed env sigma } - (* Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) @@ -1154,7 +1147,7 @@ let tactic_infer_flags with_evar = { let onOpenInductionArg env sigma tac = function | clear_flag,ElimOnConstr f -> - let (cbl, sigma') = run_delayed env sigma f in + let (sigma', cbl) = f env sigma in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma') (tac clear_flag (sigma,cbl)) @@ -1163,18 +1156,18 @@ let onOpenInductionArg env sigma tac = function (intros_until_n n) (Tacticals.New.onLastHyp (fun c -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in tac clear_flag (sigma,(c,NoBindings)) - end })) + end)) | clear_flag,ElimOnIdent (_,id) -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) - (Proofview.Goal.enter { enter = begin fun gl -> + (Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in tac clear_flag (sigma,(mkVar id,NoBindings)) - end }) + end) let onInductionArg tac = function | clear_flag,ElimOnConstr cbl -> @@ -1195,11 +1188,10 @@ let map_destruction_arg f sigma = function | clear_flag,ElimOnIdent id as x -> (sigma,x) let finish_delayed_evar_resolution with_evars env sigma f = - let ((c, lbind), sigma') = run_delayed env sigma f in - let sigma' = Sigma.Unsafe.of_evar_map sigma' in + let (sigma', (c, lbind)) = f env sigma in let flags = tactic_infer_flags with_evars in - let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (sigma,c) in - (Sigma.to_evar_map sigma', (c, lbind)) + let (sigma', c) = finish_evar_resolution ~flags env sigma' (sigma,c) in + (sigma', (c, lbind)) let with_no_bindings (c, lbind) = if lbind != NoBindings then error "'with' clause not supported here."; @@ -1215,7 +1207,7 @@ let force_destruction_arg with_evars env sigma c = let normalize_cut = false let cut c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in @@ -1233,15 +1225,15 @@ let cut c = let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in (** Backward compat: normalize [c]. *) let c = if normalize_cut then local_strong whd_betaiota sigma c else c in - Refine.refine ~unsafe:true { run = begin fun h -> - let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in - let Sigma (x, h, q) = Evarutil.new_evar env h c in + Refine.refine ~unsafe:true begin fun h -> + let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in + let (h, x) = Evarutil.new_evar env h c in let f = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in - Sigma (f, h, p +> q) - end } + (h, f) + end else Tacticals.New.tclZEROMSG (str "Not a proposition or a type.") - end } + end let error_uninstantiated_metas t clenv = let t = EConstr.Unsafe.to_constr t in @@ -1352,12 +1344,12 @@ let enforce_prop_bound_names rename tac = mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t') | _ -> assert false in let rename_branch i = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let t = Proofview.Goal.concl gl in change_concl (aux env sigma i t) - end } in + end in (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) tac (Array.map rename_branch nn) @@ -1372,7 +1364,7 @@ let rec contract_letin_in_lam_header sigma c = let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ()) rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let elim = contract_letin_in_lam_header sigma elim in @@ -1385,7 +1377,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags) - end } + end (* * Elimination tactic with bindings and using an arbitrary @@ -1402,7 +1394,7 @@ type eliminator = { } let general_elim_clause_gen elimtac indclause elim = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let (elimc,lbindelimc) = elim.elimbody in @@ -1410,10 +1402,10 @@ let general_elim_clause_gen elimtac indclause elim = let i = match elim.elimindex with None -> index_of_ind_arg sigma elimt | Some i -> i in elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause - end } + end let general_elim with_evars clear_flag (c, lbindc) elim = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ct = Retyping.get_type_of env sigma c in @@ -1425,32 +1417,30 @@ let general_elim with_evars clear_flag (c, lbindc) elim = Tacticals.New.tclTHEN (general_elim_clause_gen elimtac indclause elim) (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c) - end } + end (* Case analysis tactics *) let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in - let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in + let t = Retyping.get_type_of env sigma c in + let (mind,_) = reduce_to_quantified_ind env sigma t in let sort = Tacticals.New.elimination_sort_of_goal gl in - let mind = on_snd (fun u -> EInstance.kind (Sigma.to_evar_map sigma) u) mind in - let Sigma (elim, sigma, p) = - if occur_term (Sigma.to_evar_map sigma) c concl then + let mind = on_snd (fun u -> EInstance.kind sigma u) mind in + let (sigma, elim) = + if occur_term sigma c concl then build_case_analysis_scheme env sigma mind true sort else build_case_analysis_scheme_default env sigma mind sort in let elim = EConstr.of_constr elim in - let tac = + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (general_elim with_evars clear_flag (c,lbindc) {elimindex = None; elimbody = (elim,NoBindings); elimrename = Some (false, constructors_nrealdecls (fst mind))}) - in - Sigma (tac, sigma, p) - end } + end let general_case_analysis with_evars clear_flag (c,lbindc as cx) = Proofview.tclEVARMAP >>= fun sigma -> @@ -1486,13 +1476,11 @@ let find_eliminator c gl = let default_elim with_evars clear_flag (c,_ as cx) = Proofview.tclORELSE - (Proofview.Goal.s_enter { s_enter = begin fun gl -> + (Proofview.Goal.enter begin fun gl -> let sigma, elim = find_eliminator c gl in - let tac = - (general_elim with_evars clear_flag cx elim) - in - Sigma.Unsafe.of_pair (tac, sigma) - end }) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (general_elim with_evars clear_flag cx elim) + end) begin function (e, info) -> match e with | IsNonrec -> (* For records, induction principles aren't there by default @@ -1540,7 +1528,7 @@ let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause = let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let elim = contract_letin_in_lam_header sigma elim in @@ -1563,7 +1551,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) (str "Nothing to rewrite in " ++ pr_id id ++ str"."); clenv_refine_in with_evars id id sigma elimclause'' (fun id -> Proofview.tclUNIT ()) - end } + end let general_elim_clause with_evars flags id c e = let elim = match id with @@ -1622,7 +1610,7 @@ let make_projection env sigma params cstr sign elim i n c u = in elim let descend_in_conjunctions avoid tac (err, info) c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in try @@ -1641,14 +1629,13 @@ let descend_in_conjunctions avoid tac (err, info) c = try DefinedRecord (Recordops.lookup_projections ind) with Not_found -> let u = EInstance.kind sigma u in - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (elim, _, _) = build_case_analysis_scheme env sigma (ind,u) false sort in + let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in let elim = EConstr.of_constr elim in NotADefinedRecordUseScheme elim in Tacticals.New.tclORELSE0 (Tacticals.New.tclFIRST (List.init n (fun i -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in match make_projection env sigma params cstr sign elim i n c u with @@ -1659,32 +1646,31 @@ let descend_in_conjunctions avoid tac (err, info) c = [Proofview.V82.tactic (refine p); (* Might be ill-typed due to forbidden elimination. *) Tacticals.New.onLastHypId (tac (not isrec))] - end }))) + end))) (Proofview.tclZERO ~info err) | None -> Proofview.tclZERO ~info err with RefinerError _|UserError _ -> Proofview.tclZERO ~info err - end } + end (****************************************************) (* Resolution tactics *) (****************************************************) let solve_remaining_apply_goals = - Proofview.Goal.s_enter { s_enter = begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.enter begin fun gl -> + let evd = Proofview.Goal.sigma gl in if !apply_solve_class_goals then try let env = Proofview.Goal.env gl in - let evd = Sigma.to_evar_map sigma in let concl = Proofview.Goal.concl gl in if Typeclasses.is_class_type evd concl then let evd', c' = Typeclasses.resolve_one_typeclass env evd concl in - let tac = Refine.refine ~unsafe:true { run = fun h -> Sigma.here c' h } in - Sigma.Unsafe.of_pair (tac, evd') - else Sigma.here (Proofview.tclUNIT ()) sigma - with Not_found -> Sigma.here (Proofview.tclUNIT ()) sigma - else Sigma.here (Proofview.tclUNIT ()) sigma - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd') + (Refine.refine ~unsafe:true (fun h -> (h,c'))) + else Proofview.tclUNIT () + with Not_found -> Proofview.tclUNIT () + else Proofview.tclUNIT () + end let tclORELSEOPT t k = Proofview.tclORELSE t @@ -1695,7 +1681,7 @@ let tclORELSEOPT t k = | Some tac -> tac) let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : EConstr.constr with_bindings)) = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let flags = @@ -1705,7 +1691,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : step. *) let concl_nprod = nb_prod_modulo_zeta sigma concl in let rec try_main_apply with_destruct c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -1759,14 +1745,14 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : | PretypeError _|RefinerError _|UserError _|Failure _ -> Some (try_red_apply thm_ty0 (e, info)) | _ -> None) - end } + end in Tacticals.New.tclTHENLIST [ try_main_apply with_destruct c; solve_remaining_apply_goals; apply_clear_request clear_flag (use_clear_hyp_by_default ()) c ] - end } + end let rec apply_with_bindings_gen b e = function | [] -> Proofview.tclUNIT () @@ -1778,13 +1764,13 @@ let rec apply_with_bindings_gen b e = function let apply_with_delayed_bindings_gen b e l = let one k (loc, f) = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let (cb, sigma) = run_delayed env sigma f in + let (sigma, cb) = f env sigma in Tacticals.New.tclWITHHOLES e (general_apply b b e k (loc,cb)) sigma - end } + end in let rec aux = function | [] -> Proofview.tclUNIT () @@ -1861,7 +1847,7 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = let apply_in_once sidecond_first with_delta with_destruct with_evars naming id (clear_flag,(loc,(d,lbind))) tac = let open Context.Rel.Declaration in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let flags = @@ -1870,7 +1856,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in let rec aux idstoclear with_destruct c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in try @@ -1887,22 +1873,22 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming (descend_in_conjunctions [targetid] (fun b id -> aux (id::idstoclear) b (mkVar id)) (e, info) c) - end } + end in aux [] with_destruct d - end } + end let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming id (clear_flag,(loc,f)) tac = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let (c, sigma) = run_delayed env sigma f in + let (sigma, c) = f env sigma in Tacticals.New.tclWITHHOLES with_evars (apply_in_once sidecond_first with_delta with_destruct with_evars naming id (clear_flag,(loc,c)) tac) sigma - end } + end (* A useful resolution tactic which, if c:A->B, transforms |- C into |- B -> C and |- A @@ -1922,21 +1908,20 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam *) let cut_and_apply c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in match EConstr.kind sigma (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with | Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 -> let concl = Proofview.Goal.concl gl in let env = Tacmach.New.pf_env gl in - Refine.refine { run = begin fun sigma -> + Refine.refine begin fun sigma -> let typ = mkProd (Anonymous, c2, concl) in - let Sigma (f, sigma, p) = Evarutil.new_evar env sigma typ in - let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c1 in - let ans = mkApp (f, [|mkApp (c, [|x|])|]) in - Sigma (ans, sigma, p +> q) - end } + let (sigma, f) = Evarutil.new_evar env sigma typ in + let (sigma, x) = Evarutil.new_evar env sigma c1 in + (sigma, mkApp (f, [|mkApp (c, [|x|])|])) + end | _ -> error "lapply needs a non-dependent product." - end } + end (********************************************************************) (* Exact tactics *) @@ -1949,42 +1934,38 @@ let cut_and_apply c = (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *) let exact_no_check c = - Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h } + Refine.refine ~unsafe:true (fun h -> (h,c)) let exact_check c = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in (** We do not need to normalize the goal because we just check convertibility *) let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map sigma in let sigma, ct = Typing.type_of env sigma c in - let tac = - Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c) - in - Sigma.Unsafe.of_pair (tac, sigma) - end } + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c)) + end let cast_no_check cast c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in exact_no_check (mkCast (c, cast, concl)) - end } + end let vm_cast_no_check c = cast_no_check Term.VMcast c let native_cast_no_check c = cast_no_check Term.NATIVEcast c let exact_proof c = let open Tacmach.New in - Proofview.Goal.enter { enter = begin fun gl -> - Refine.refine { run = begin fun sigma -> - let sigma = Sigma.to_evar_map sigma in + Proofview.Goal.enter begin fun gl -> + Refine.refine begin fun sigma -> let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (pf_concl gl) in let c = EConstr.of_constr c in let sigma = Evd.merge_universe_context sigma ctx in - Sigma.Unsafe.of_pair (c, sigma) - end } - end } + (sigma, c) + end + end let assumption = let rec arec gl only_eq = function @@ -2008,10 +1989,10 @@ let assumption = exact_no_check (mkVar (NamedDecl.get_id decl)) else arec gl only_eq rest in - let assumption_tac = { enter = begin fun gl -> + let assumption_tac gl = let hyps = Proofview.Goal.hyps gl in arec gl true hyps - end } in + in Proofview.Goal.enter assumption_tac (*****************************************************************) @@ -2050,7 +2031,7 @@ let check_decl env sigma decl = let clear_body ids = let open Context.Named.Declaration in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in let sigma = Tacmach.New.project gl in @@ -2095,10 +2076,10 @@ let clear_body ids = Tacticals.New.tclZEROMSG msg in check <*> - Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~unsafe:true begin fun sigma -> Evarutil.new_evar env sigma ~principal:true concl - end } - end } + end + end let clear_wildcards ids = Tacticals.New.tclMAP (fun (loc, id) -> clear [id]) ids @@ -2117,7 +2098,7 @@ let rec intros_clearing = function (* Keeping only a few hypotheses *) let keep hyps = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> Proofview.tclENV >>= fun env -> let ccl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in @@ -2133,7 +2114,7 @@ let keep hyps = ~init:([],[]) (Proofview.Goal.env gl) in clear cl - end } + end (*********************************) (* Basic generalization tactics *) @@ -2144,16 +2125,16 @@ let keep hyps = this generalizes [hyps |- goal] into [hyps |- T] *) let apply_type newcl args = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in - Refine.refine { run = begin fun sigma -> - let newcl = nf_betaiota (Sigma.to_evar_map sigma) newcl (* As in former Logic.refine *) in - let Sigma (ev, sigma, p) = + Refine.refine begin fun sigma -> + let newcl = nf_betaiota sigma newcl (* As in former Logic.refine *) in + let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true ~store newcl in - Sigma (applist (ev, args), sigma, p) - end } - end } + (sigma, applist (ev, args)) + end + end (* Given a context [hyps] with domain [x1..xn], possibly with let-ins, and well-typed in the current goal, [bring_hyps hyps] generalizes @@ -2162,25 +2143,25 @@ let apply_type newcl args = let bring_hyps hyps = if List.is_empty hyps then Tacticals.New.tclIDTAC else - Proofview.Goal.enter { enter = begin fun gl -> + 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_concl gl in let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in let args = Array.of_list (Context.Named.to_instance mkVar hyps) in - Refine.refine { run = begin fun sigma -> - let Sigma (ev, sigma, p) = + Refine.refine begin fun sigma -> + let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true ~store newcl in - Sigma (mkApp (ev, args), sigma, p) - end } - end } + (sigma, mkApp (ev, args)) + end + end let revert hyps = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let gl = Proofview.Goal.assume gl in let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in (bring_hyps ctx) <*> (clear hyps) - end } + end (************************) (* Introduction tactics *) @@ -2197,7 +2178,7 @@ let check_number_of_constructors expctdnumopt i nconstr = if i > nconstr then error "Not enough constructors." let constructor_tac with_evars expctdnumopt i lbind = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let cl = Tacmach.New.pf_concl gl in let reduce_to_quantified_ind = @@ -2208,19 +2189,16 @@ let constructor_tac with_evars expctdnumopt i lbind = Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in check_number_of_constructors expctdnumopt i nconstr; - let Sigma ((cons, u), sigma, p) = Sigma.fresh_constructor_instance + let (sigma, (cons, u)) = Evd.fresh_constructor_instance (Proofview.Goal.env gl) sigma (fst mind, i) in let cons = mkConstructU (cons, EInstance.make u) in let apply_tac = general_apply true false with_evars None (Loc.tag (cons,lbind)) in - let tac = - (Tacticals.New.tclTHENLIST - [ - convert_concl_no_check redcl DEFAULTcast; - intros; apply_tac]) - in - Sigma (tac, sigma, p) - end } + Tacticals.New.tclTHENLIST + [ Proofview.Unsafe.tclEVARS sigma; + convert_concl_no_check redcl DEFAULTcast; + intros; apply_tac] + end let one_constructor i lbind = constructor_tac false None i lbind @@ -2237,7 +2215,7 @@ let rec tclANY tac = function let any_constructor with_evars tacopt = let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in let tac i = Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let cl = Tacmach.New.pf_concl gl in let reduce_to_quantified_ind = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl @@ -2247,7 +2225,7 @@ let any_constructor with_evars tacopt = Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in if Int.equal nconstr 0 then error "The type has no constructors."; tclANY tac (List.interval 1 nconstr) - end } + end let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1 let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2 @@ -2298,7 +2276,7 @@ let my_find_eq_data_decompose gl t = | Constr_matching.PatternMatchingFailure -> None let intro_decomp_eq ?loc l thin tac id = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in @@ -2309,10 +2287,10 @@ let intro_decomp_eq ?loc l thin tac id = (eq,t,eq_args) (c, t) | None -> Tacticals.New.tclZEROMSG (str "Not a primitive equality here.") - end } + end let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in @@ -2324,7 +2302,7 @@ let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id = (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id])) (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l) nv_with_let ll) - end } + end let rewrite_hyp_then assert_style with_evars thin l2r id tac = let rew_on l2r = @@ -2334,7 +2312,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = let clear_var_and_eq id' = clear [id';id] in let early_clear id' thin = List.filter (fun (_,id) -> not (Id.equal id id')) thin in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in @@ -2366,7 +2344,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = thin in (* Skip the side conditions of the rewriting step *) Tacticals.New.tclTHENFIRST eqtac (tac thin) - end } + end let prepare_naming ?loc = function | IntroIdentifier id -> NamingMustBe (Loc.tag ?loc id) @@ -2525,10 +2503,8 @@ and intro_pattern_action ?loc with_evars b style pat thin destopt tac id = Proofview.tclUNIT () (* apply_in_once do a replacement *) else clear [id] in - let f = { delayed = fun env sigma -> - let Sigma (c, sigma, p) = f.delayed env sigma in - Sigma ((c, NoBindings), sigma, p) - } in + let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings)) + in apply_in_delayed_once false true true with_evars naming id (None,(loc',f)) (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []]) @@ -2547,12 +2523,12 @@ and prepare_intros ?loc with_evars dft destopt = function (str "Introduction pattern for one hypothesis expected.") let intro_patterns_head_core with_evars b destopt bound pat = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in check_name_unicity env [] [] pat; intro_patterns_core with_evars b [] [] [] destopt bound 0 (fun _ l -> clear_wildcards l) pat - end } + end let intro_patterns_bound_to with_evars n destopt = intro_patterns_head_core with_evars true destopt @@ -2602,7 +2578,7 @@ 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 - Proofview.Goal.enter { enter = begin fun gl -> + 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 @@ -2614,7 +2590,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars 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 } + end (* if sidecond_first then @@ -2625,7 +2601,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars *) let apply_in simple with_evars id lemmas ipat = - let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, { delayed = fun _ sigma -> Sigma.here l sigma })) lemmas in + let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, (fun _ sigma -> (sigma,l)))) lemmas in general_apply_in false simple simple with_evars id lemmas ipat let apply_delayed_in simple with_evars id lemmas ipat = @@ -2649,17 +2625,16 @@ let decode_hyp = function *) let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let Sigma (t, sigma, p) = match ty with - | Some t -> Sigma.here t sigma + let (sigma, t) = match ty with + | Some t -> (sigma, t) | None -> let t = typ_of env sigma c in - let sigma, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env (Sigma.to_evar_map sigma) t in - Sigma.Unsafe.of_pair (c, sigma) + Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t in - let Sigma ((newcl, eq_tac), sigma, q) = match with_eq with + let (sigma, (newcl, eq_tac)) = match with_eq with | Some (lr,(loc,ido)) -> let heq = match ido with | IntroAnonymous -> new_fresh_id [id] (add_prefix "Heq" id) gl @@ -2667,33 +2642,31 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = | IntroIdentifier id -> id in let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in - let Sigma (eq, sigma, p) = Sigma.fresh_global env sigma eqdata.eq in + let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in let eq = EConstr.of_constr eq in - let Sigma (refl, sigma, q) = Sigma.fresh_global env sigma eqdata.refl in + let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in let refl = EConstr.of_constr refl in 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 = Sigma.to_evar_map sigma in let sigma, _ = Typing.type_of env sigma term in let ans = term, - Tacticals.New.tclTHEN - (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false) - (clear_body [heq;id]) + Tacticals.New.tclTHENLIST + [ + intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false; + clear_body [heq;id]] in - Sigma.Unsafe.of_pair (ans, sigma) + (sigma, ans) | None -> - Sigma.here (mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) sigma + (sigma, (mkNamedLetIn id c t ccl, Proofview.tclUNIT ())) in - let tac = Tacticals.New.tclTHENLIST - [ convert_concl_no_check newcl DEFAULTcast; + [ Proofview.Unsafe.tclEVARS sigma; + convert_concl_no_check newcl DEFAULTcast; intro_gen (NamingMustBe (Loc.tag id)) (decode_hyp lastlhyp) true false; Tacticals.New.tclMAP convert_hyp_no_check depdecls; eq_tac ] - in - Sigma (tac, sigma, p +> q) - end } + end let insert_before decls lasthyp env = match lasthyp with @@ -2725,22 +2698,22 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = id in let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in - let Sigma (eq, sigma, p) = Sigma.fresh_global env sigma eqdata.eq in + let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in let eq = EConstr.of_constr eq in - let Sigma (refl, sigma, q) = Sigma.fresh_global env sigma eqdata.refl in + let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in let refl = EConstr.of_constr refl in let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in - let Sigma (x, sigma, r) = new_evar newenv sigma ~principal:true ~store ccl in - Sigma (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x), sigma, p +> q +> r) + let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in + (sigma, mkNamedLetIn id c t (mkNamedLetIn heq refl eq x)) | None -> let newenv = insert_before [decl] lastlhyp env in - let Sigma (x, sigma, p) = new_evar newenv sigma ~principal:true ~store ccl in - Sigma (mkNamedLetIn id c t x, sigma, p) + let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in + (sigma, mkNamedLetIn id c t x) let letin_tac with_eq id c ty occs = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let ccl = Proofview.Goal.concl gl in @@ -2748,41 +2721,39 @@ let letin_tac with_eq id c ty occs = let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in (* We keep the original term to match but record the potential side-effects of unifying universes. *) - let Sigma (c, sigma, p) = match res with - | None -> Sigma.here c sigma - | Some (Sigma (_, sigma, p)) -> Sigma (c, sigma, p) + let (sigma, c) = match res with + | None -> (sigma, c) + | Some (sigma, _) -> (sigma, c) in - let tac = letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty in - Sigma (tac, sigma, p) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty) + end let letin_pat_tac with_evars with_eq id c occs = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let ccl = Proofview.Goal.concl gl in let check t = true in let abs = AbstractPattern (false,check,id,c,occs,false) in let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in - let Sigma (c, sigma, p) = match res with + let (sigma, c) = match res with | None -> finish_evar_resolution ~flags:(tactic_infer_flags with_evars) env sigma c | Some res -> res in - let tac = - (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) None) - in - Sigma (tac, sigma, p) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) None) + end (* Tactics "pose proof" (usetac=None) and "assert"/"enough" (otherwise) *) let forward b usetac ipat c = match usetac with | None -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let t = Tacmach.New.pf_get_type_of gl c in let sigma = Tacmach.New.project gl in let hd = head_ident sigma c in Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c) - end } + end | Some tac -> let tac = match tac with | None -> Tacticals.New.tclIDTAC @@ -2847,7 +2818,7 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = 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 -> + Proofview.Goal.nf_enter begin fun gl -> let env = pf_env gl in let sign = Proofview.Goal.hyps gl in let sigma = project gl in @@ -2881,16 +2852,14 @@ let generalize_dep ?(with_let=false) c = (** 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 - 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 } + tclTHENLIST + [ Proofview.Unsafe.tclEVARS evd; + apply_type cl'' (if Option.is_empty body then c::args else args); + clear (List.rev tothin')] + end (** *) -let generalize_gen_let lconstr = Proofview.Goal.s_enter { s_enter = begin fun gl -> +let generalize_gen_let lconstr = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let newcl, evd = List.fold_right_i (generalize_goal gl) 0 lconstr @@ -2898,16 +2867,15 @@ let generalize_gen_let lconstr = Proofview.Goal.s_enter { s_enter = begin fun gl in let (evd, _) = Typing.type_of env evd newcl in let map ((_, c, b),_) = if Option.is_empty b then Some c else None in - let tac = apply_type newcl (List.map_filter map lconstr) in - Sigma.Unsafe.of_pair (tac, evd) -end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) + (apply_type newcl (List.map_filter map lconstr)) +end let new_generalize_gen_let lconstr = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in - let sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let ids = Tacmach.New.pf_ids_of_hyps gl in let newcl, sigma, args = @@ -2919,14 +2887,12 @@ let new_generalize_gen_let lconstr = (cl, sigma, args)) 0 lconstr (concl, sigma, []) in - let tac = - Refine.refine { run = begin fun sigma -> - let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true newcl in - Sigma ((applist (ev, args)), sigma, p) - end } - in - Sigma.Unsafe.of_pair (tac, sigma) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Refine.refine begin fun sigma -> + let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true newcl in + (sigma, applist (ev, args)) + end) + end let generalize_gen lconstr = generalize_gen_let (List.map (fun (occs_c,na) -> @@ -2968,9 +2934,9 @@ let quantify lconstr = of inferred args and yi. The overall effect is to remove from H as much quantification as possible given lbind. *) let specialize (c,lbind) ipat = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let sigma = Proofview.Goal.sigma gl in let sigma, term = if lbind == NoBindings then sigma, c @@ -3046,7 +3012,7 @@ let specialize (c,lbind) ipat = (exact_no_check term) in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac - end } + end (*****************************) (* Ad hoc unfold *) @@ -3056,7 +3022,7 @@ let specialize (c,lbind) ipat = (* Unfolds x by its definition everywhere *) let unfold_body x = let open Context.Named.Declaration in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (** We normalize the given hypothesis immediately. *) let env = Proofview.Goal.env (Proofview.Goal.assume gl) in let xval = match Environ.lookup_named x env with @@ -3072,7 +3038,7 @@ let unfold_body x = let reductc = reduct_in_concl (rfun, DEFAULTcast) in Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc] end - end } + end (* Either unfold and clear if defined or simply clear if not a definition *) let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] @@ -3117,7 +3083,7 @@ let warn_unused_intro_pattern = strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++ str": " ++ prlist_with_sep spc (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_econstr (fst (run_delayed (Global.env()) Evd.empty c)))) names) + (fun c -> Printer.pr_econstr (snd (c (Global.env()) Evd.empty)))) names) let check_unused_names names = if not (List.is_empty names) then @@ -3201,7 +3167,7 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = match ra with | (RecArg,_,deprec,recvarname) :: (IndArg,_,depind,hyprecname) :: ra' -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (recpat,names) = match names with | [loc,IntroNaming (IntroIdentifier id) as pat] -> let id' = next_ident_away (add_prefix "IH" id) avoid in @@ -3209,37 +3175,37 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = | _ -> consume_pattern avoid (Name recvarname) deprec gl names in let dest = get_recarg_dest dests in dest_intro_patterns with_evars avoid thin dest [recpat] (fun ids thin -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (hyprec,names) = consume_pattern avoid (Name hyprecname) depind gl names in dest_intro_patterns with_evars avoid thin MoveLast [hyprec] (fun ids' thin -> peel_tac ra' (update_dest dests ids') names thin) - end }) - end } + end) + end | (IndArg,_,dep,hyprecname) :: ra' -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (* Rem: does not happen in Coq schemes, only in user-defined schemes *) let pat,names = consume_pattern avoid (Name hyprecname) dep gl names in dest_intro_patterns with_evars avoid thin MoveLast [pat] (fun ids thin -> peel_tac ra' (update_dest dests ids) names thin) - end } + end | (RecArg,_,dep,recvarname) :: ra' -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (pat,names) = consume_pattern avoid (Name recvarname) dep gl names in let dest = get_recarg_dest dests in dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin -> peel_tac ra' dests names thin) - end } + end | (OtherArg,_,dep,_) :: ra' -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (pat,names) = consume_pattern avoid Anonymous dep gl names in let dest = get_recarg_dest dests in safe_dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin -> peel_tac ra' dests names thin) - end } + end | [] -> check_unused_names names; Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests) @@ -3262,7 +3228,7 @@ let expand_projections env sigma c = (* Marche pas... faut prendre en compte l'occurrence précise... *) let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in @@ -3316,7 +3282,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = (atomize_one (i-1) (mkVar x::args) (mkVar x::args') (x::avoid)) in atomize_one (List.length argl) [] [] [] - end } + end (* [cook_sign] builds the lists [beforetoclear] (preceding the ind. var.) and [aftertoclear] (coming after the ind. var.) of hyps @@ -3561,16 +3527,12 @@ let error_ind_scheme s = let s = if not (String.is_empty s) then s^" " else s in user_err ~hdr:"Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.") -let glob sigma gr = - let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr - in Sigma.to_evar_map sigma, c - -let coq_eq sigma = glob sigma (Coqlib.build_coq_eq ()) -let coq_eq_refl sigma = glob sigma (Coqlib.build_coq_eq_refl ()) +let coq_eq sigma = Evarutil.new_global sigma (Coqlib.build_coq_eq ()) +let coq_eq_refl sigma = Evarutil.new_global sigma (Coqlib.build_coq_eq_refl ()) let coq_heq_ref = lazy (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq") -let coq_heq sigma = glob sigma (Lazy.force coq_heq_ref) -let coq_heq_refl sigma = glob sigma (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl") +let coq_heq sigma = Evarutil.new_global sigma (Lazy.force coq_heq_ref) +let coq_heq_refl sigma = Evarutil.new_global sigma (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl") let mkEq sigma t x y = let sigma, eq = coq_eq sigma in @@ -3625,25 +3587,24 @@ let decompose_indapp sigma f args = | _ -> f, args let mk_term_eq homogeneous env sigma ty t ty' t' = - let sigma = Sigma.to_evar_map sigma in if homogeneous then let sigma, eq = mkEq sigma ty t t' in let sigma, refl = mkRefl sigma ty' t' in - Sigma.Unsafe.of_evar_map sigma, (eq, refl) + sigma, (eq, refl) else let sigma, heq = mkHEq sigma ty t ty' t' in let sigma, hrefl = mkHRefl sigma ty' t' in - Sigma.Unsafe.of_evar_map sigma, (heq, hrefl) + sigma, (heq, hrefl) let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = let open Context.Rel.Declaration in - Refine.refine { run = begin fun sigma -> + Refine.refine begin fun sigma -> let eqslen = List.length eqs in (* Abstract by the "generalized" hypothesis equality proof if necessary. *) let sigma, abshypeq, abshypt = if dep then let ty = lift 1 c in - let homogeneous = Reductionops.is_conv env (Sigma.to_evar_map sigma) ty typ in + let homogeneous = Reductionops.is_conv env sigma ty typ in let sigma, (eq, refl) = mk_term_eq homogeneous (push_rel_context ctx env) sigma ty (mkRel 1) typ (mkVar id) in sigma, mkProd (Anonymous, eq, lift 1 concl), [| refl |] @@ -3661,7 +3622,7 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = (* Abstract by the extension of the context *) let genctyp = it_mkProd_or_LetIn genarg ctx in (* The goal will become this product. *) - let Sigma (genc, sigma, p) = Evarutil.new_evar env sigma ~principal:true genctyp in + let (sigma, genc) = Evarutil.new_evar env sigma ~principal:true genctyp in (* Apply the old arguments giving the proper instantiation of the hyp *) let instc = mkApp (genc, Array.of_list args) in (* Then apply to the original instantiated hyp. *) @@ -3669,8 +3630,8 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = (* Apply the reflexivity proofs on the indices. *) let appeqs = mkApp (instc, Array.of_list refls) in (* Finally, apply the reflexivity proof for the original hyp, to get a term of type gl again. *) - Sigma (mkApp (appeqs, abshypt), sigma, p) - end } + (sigma, mkApp (appeqs, abshypt)) + end let hyps_of_vars env sigma sign nogen hyps = if Id.Set.is_empty hyps then [] @@ -3802,7 +3763,7 @@ let abstract_args gl generalize_vars dep id defined f args = let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = let open Context.Named.Declaration in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> Coqlib.check_required_library Coqlib.jmeq_module_name; let sigma = Tacmach.New.project gl in let (f, args, def, id, oldid) = @@ -3838,7 +3799,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = [revert vars ; Tacticals.New.tclMAP (fun id -> Tacticals.New.tclTRY (generalize_dep ~with_let:true (mkVar id))) vars]) - end } + end let compare_upto_variables sigma x y = let rec compare x y = @@ -3899,12 +3860,12 @@ let specialize_eqs id gl = else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl -let specialize_eqs id = Proofview.Goal.enter { enter = begin fun gl -> +let specialize_eqs id = Proofview.Goal.enter begin fun gl -> let msg = str "Specialization not allowed on dependent hypotheses" in Proofview.tclOR (clear [id]) (fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () -> Proofview.V82.tactic (specialize_eqs id) -end } +end let occur_rel sigma n c = let res = not (noccurn sigma n c) in @@ -4118,17 +4079,17 @@ let guess_elim isrec dep s hyp0 gl = if isrec && not (is_nonrec mind) then find_ind_eliminator mind s gl else let env = Tacmach.New.pf_env gl in - let sigma = Sigma.Unsafe.of_evar_map (Tacmach.New.project gl) in + let sigma = Tacmach.New.project gl in let u = EInstance.kind (Tacmach.New.project gl) u in if use_dependent_propositions_elimination () && dep then - let Sigma (ind, sigma, _) = build_case_analysis_scheme env sigma (mind, u) true s in + let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in let ind = EConstr.of_constr ind in - (Sigma.to_evar_map sigma, ind) + (sigma, ind) else - let Sigma (ind, sigma, _) = build_case_analysis_scheme_default env sigma (mind, u) s in + let (sigma, ind) = build_case_analysis_scheme_default env sigma (mind, u) s in let ind = EConstr.of_constr ind in - (Sigma.to_evar_map sigma, ind) + (sigma, ind) in let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in evd, ((elimc, NoBindings), elimt), mkIndU (mind, u) @@ -4235,7 +4196,7 @@ let recolle_clenv i params args elimclause gl = produce new ones). Then refine with the resulting term with holes. *) let induction_tac with_evars params indvars elim = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in let i = match i with None -> index_of_ind_arg sigma elimt | Some i -> i in @@ -4248,17 +4209,16 @@ let induction_tac with_evars params indvars elim = (* one last resolution (useless?) *) let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved) - end } + end (* Apply induction "in place" taking into account dependent hypotheses from the context, replacing the main hypothesis on which induction applies with the induction hypotheses *) let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_tac = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map sigma in let concl = Tacmach.New.pf_concl gl in let statuslists,lhyp0,toclear,deps,avoid,dep_in_hyps = cook_sign hyp0 inhyps indvars env sigma in let dep_in_concl = Option.cata (fun id -> occur_var env sigma id concl) false hyp0 in @@ -4288,16 +4248,16 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ (re_intro_dependent_hypotheses statuslists)) indsign names) in - Sigma.Unsafe.of_pair (tac, sigma) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac + end let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in atomize_param_of_ind_then elim_info hyp0 (fun indvars -> apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names (fun elim -> induction_tac with_evars [] [hyp0] elim)) - end } + end let msg_not_right_number_induction_arguments scheme = str"Not the right number of induction arguments (expected " ++ @@ -4314,7 +4274,7 @@ let msg_not_right_number_induction_arguments scheme = must be given, so we help a bit the unifier by making the "pattern" by hand before calling induction_tac *) let induction_without_atomization isrec with_evars elim names lid = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma, (indsign,scheme) = get_elim_signature elim (List.hd lid) gl in let nargs_indarg_farg = scheme.nargs + (if scheme.farg_in_concl then 1 else 0) in @@ -4345,11 +4305,11 @@ let induction_without_atomization isrec with_evars elim names lid = ] in let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in apply_induction_in_context with_evars None [] elim indvars names induct_tac - end } + end (* assume that no occurrences are selected *) let clear_unselected_context id inhyps cls = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> if occur_var (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id (Tacmach.New.pf_concl gl) && cls.concl_occs == NoOccurrences then user_err @@ -4367,10 +4327,9 @@ let clear_unselected_context id inhyps cls = let ids = List.map_filter to_erase (Proofview.Goal.hyps gl) in clear ids | None -> Proofview.tclUNIT () - end } + end let use_bindings env sigma elim must_be_closed (c,lbind) typ = - let sigma = Sigma.to_evar_map sigma in let typ = if elim == None then (* w/o an scheme, the term has to be applied at least until @@ -4392,8 +4351,7 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ = if must_be_closed && occur_meta indclause.evd (clenv_value indclause) then error "Need a fully applied argument."; (* We lose the possibility of coercions in with-bindings *) - let (sigma, c) = pose_all_metas_as_evars env indclause.evd (clenv_value indclause) in - Sigma.Unsafe.of_pair (c, sigma) + pose_all_metas_as_evars env indclause.evd (clenv_value indclause) with e when catchable_exception e -> try find_clause (try_red_product env sigma typ) with Redelimination -> raise e in @@ -4411,7 +4369,6 @@ let check_expected_type env sigma (elimc,bl) elimt = fun t -> Evarconv.e_cumul env (ref sigma) t u let check_enough_applied env sigma elim = - let sigma = Sigma.to_evar_map sigma in (* A heuristic to decide whether the induction arg is enough applied *) match elim with | None -> @@ -4436,13 +4393,13 @@ let guard_no_unifiable = Proofview.guard_no_unifiable >>= function let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let ccl = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in let check = check_enough_applied env sigma elim in - let Sigma (c, sigma', p) = use_bindings env sigma elim false (c0,lbind) t0 in + let (sigma', c) = use_bindings env sigma elim false (c0,lbind) t0 in let abs = AbstractPattern (from_prefix,check,Name id,(pending,c),cls,false) in let (id,sign,_,lastlhyp,ccl,res) = make_abstraction env sigma' ccl abs in match res with @@ -4452,7 +4409,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim (* we restart using bindings after having tried type-class resolution etc. on the term given by the user *) let flags = tactic_infer_flags (with_evars && (* do not give a success semantics to edestruct on an open term yet *) false) in - let Sigma (c0, sigma, q) = finish_evar_resolution ~flags env sigma (pending,c0) in + let (sigma, c0) = finish_evar_resolution ~flags env sigma (pending,c0) in let tac = (if isrec then (* Historically, induction has side conditions last *) @@ -4461,13 +4418,12 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim (* and destruct has side conditions first *) Tacticals.New.tclTHENLAST) (Tacticals.New.tclTHENLIST [ - Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~unsafe:true begin fun sigma -> let b = not with_evars && with_eq != None in - let Sigma (c, sigma, p) = use_bindings env sigma elim b (c0,lbind) t0 in - let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in - let Sigma (ans, sigma, q) = mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t) in - Sigma (ans, sigma, p +> q) - end }; + let (sigma, c) = use_bindings env sigma elim b (c0,lbind) t0 in + let t = Retyping.get_type_of env sigma c in + mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t) + end; if with_evars then Proofview.shelve_unifiable else guard_no_unifiable; if is_arg_pure_hyp then Proofview.tclEVARMAP >>= fun sigma -> Tacticals.New.tclTRY (clear [destVar sigma c0]) @@ -4476,23 +4432,23 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim ]) tac in - Sigma (tac, sigma, q) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac - | Some (Sigma (c, sigma', q)) -> + | Some (sigma', c) -> (* pattern found *) let with_eq = Option.map (fun eq -> (false,eq)) eqname in (* TODO: if ind has predicate parameters, use JMeq instead of eq *) let env = reset_with_named_context sign env in let tac = Tacticals.New.tclTHENLIST [ - Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~unsafe:true begin fun sigma -> mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None - end }; + end; tac ] in - Sigma (tac, sigma', p +> q) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma') tac + end let has_generic_occurrences_but_goal cls id env sigma ccl = clause_with_generic_context_selection cls && @@ -4504,19 +4460,18 @@ let induction_gen clear_flag isrec with_evars elim let inhyps = match cls with | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps | _ -> [] in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let evd = Sigma.to_evar_map sigma in + let evd = Proofview.Goal.sigma gl in let ccl = Proofview.Goal.concl gl in let cls = Option.default allHypsAndConcl cls in - let t = typ_of env sigma c in + let t = typ_of env evd c in let is_arg_pure_hyp = isVar evd c && not (mem_named_context_val (destVar evd c) (Global.named_context_val ())) && lbind == NoBindings && not with_evars && Option.is_empty eqname && clear_flag == None && has_generic_occurrences_but_goal cls (destVar evd c) env evd ccl in - let enough_applied = check_enough_applied env sigma elim t in + let enough_applied = check_enough_applied env evd elim t in if is_arg_pure_hyp && enough_applied then (* First case: induction on a variable already in an inductive type and with maximal abstraction over the variable. @@ -4540,7 +4495,7 @@ let induction_gen clear_flag isrec with_evars elim isrec with_evars info_arg elim id arg t inhyps cls (induction_with_atomization_of_ind_arg isrec with_evars elim names id inhyps) - end } + end (* Induction on a list of arguments. First make induction arguments atomic (using letins), then do induction. The specificity here is @@ -4566,7 +4521,7 @@ let induction_gen_l isrec with_evars elim names lc = atomize_list l' | _ -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in let sigma = Tacmach.New.project gl in let x = @@ -4578,7 +4533,7 @@ let induction_gen_l isrec with_evars elim names lc = Tacticals.New.tclTHEN (letin_tac None (Name id) c None allHypsAndConcl) (atomize_list newl') - end } in + end in Tacticals.New.tclTHENLIST [ (atomize_list lc); @@ -4595,7 +4550,7 @@ let induction_destruct isrec with_evars (lc,elim) = match lc with | [] -> assert false (* ensured by syntax, but if called inside caml? *) | [c,(eqname,names as allnames),cls] -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in match elim with @@ -4612,9 +4567,9 @@ let induction_destruct isrec with_evars (lc,elim) = (* standard induction *) onOpenInductionArg env sigma (fun clear_flag c -> induction_gen clear_flag isrec with_evars elim (c,allnames) cls) c - end } + end | _ -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in match elim with @@ -4630,12 +4585,12 @@ let induction_destruct isrec with_evars (lc,elim) = (onOpenInductionArg env sigma (fun clear_flag a -> induction_gen clear_flag isrec with_evars None (a,b) cl) a) (Tacticals.New.tclMAP (fun (a,b,cl) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in onOpenInductionArg env sigma (fun clear_flag a -> induction_gen clear_flag false with_evars None (a,b) cl) a - end }) l) + end) l) | Some elim -> (* Several induction hyps with induction scheme *) let lc = List.map (on_pi1 (fun c -> snd (force_destruction_arg false env sigma c))) lc in @@ -4654,7 +4609,7 @@ let induction_destruct isrec with_evars (lc,elim) = error "'as' clause with multiple arguments and 'using' clause can only occur last."; let newlc = List.map (fun (x,_) -> (x,None)) newlc in induction_gen_l isrec with_evars elim names newlc - end } + end let induction ev clr c l e = induction_gen clr true ev e @@ -4696,7 +4651,7 @@ let simple_destruct = function *) let elim_scheme_type elim t = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let clause = mk_clenv_type_of gl elim in match EConstr.kind clause.evd (last_arg clause.evd clause.templval.rebus) with | Meta mv -> @@ -4706,26 +4661,26 @@ let elim_scheme_type elim t = (clenv_meta_type clause mv) clause in Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false | _ -> anomaly (Pp.str "elim_scheme_type.") - end } + end let elim_type t = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in - Sigma.Unsafe.of_pair (elim_scheme_type elimc t, evd) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t) + end let case_type t = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Tacmach.New.pf_env gl in - let ((ind, u), t) = reduce_to_atomic_ind env (Sigma.to_evar_map sigma) t in - let u = EInstance.kind (Sigma.to_evar_map sigma) u in + let ((ind, u), t) = reduce_to_atomic_ind env sigma t in + let u = EInstance.kind sigma u in let s = Tacticals.New.elimination_sort_of_goal gl in - let Sigma (elimc, evd, p) = build_case_analysis_scheme_default env sigma (ind, u) s in + let (evd, elimc) = build_case_analysis_scheme_default env sigma (ind, u) s in let elimc = EConstr.of_constr elimc in - Sigma (elim_scheme_type elimc t, evd, p) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t) + end (************************************************) @@ -4745,7 +4700,7 @@ let maybe_betadeltaiota_concl allowred gl = whd_all env sigma concl let reflexivity_red allowred = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (* PL: usual reflexivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) @@ -4754,7 +4709,7 @@ let reflexivity_red allowred = match match_with_equality_type sigma concl with | None -> Proofview.tclZERO NoEquationFound | Some _ -> one_constructor 1 NoBindings - end } + end let reflexivity = Proofview.tclORELSE @@ -4796,7 +4751,7 @@ let match_with_equation sigma c = Proofview.tclZERO NoEquationFound let symmetry_red allowred = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (* PL: usual symmetry don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) @@ -4809,7 +4764,7 @@ let symmetry_red allowred = (convert_concl_no_check concl DEFAULTcast) (Tacticals.New.pf_constr_of_global eq_data.sym >>= apply) | None,eq,eq_kind -> prove_symmetry eq eq_kind - end } + end let symmetry = Proofview.tclORELSE @@ -4823,7 +4778,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in let sign,t = decompose_prod_assum sigma ctype in @@ -4843,7 +4798,7 @@ let symmetry_in id = | NoEquationFound -> Hook.get forward_setoid_symmetry_in id | e -> Proofview.tclZERO ~info e end - end } + end let intros_symmetry = Tacticals.New.onClause @@ -4868,7 +4823,7 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make () (* This is probably not very useful any longer *) let prove_transitivity hdcncl eq_kind t = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let (eq1,eq2) = match eq_kind with | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]) @@ -4888,10 +4843,10 @@ let prove_transitivity hdcncl eq_kind t = [ Tacticals.New.tclDO 2 intro; Tacticals.New.onLastHyp simplest_case; assumption ])) - end } + end let transitivity_red allowred t = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (* PL: usual transitivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) @@ -4909,7 +4864,7 @@ let transitivity_red allowred t = match t with | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.") | Some t -> prove_transitivity eq eq_kind t - end } + end let transitivity_gen t = Proofview.tclORELSE @@ -4994,11 +4949,10 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let current_sign = Global.named_context_val () and global_sign = Proofview.Goal.hyps gl in - let sigma = Sigma.to_evar_map sigma in let evdref = ref sigma in let sign,secsign = List.fold_right @@ -5065,8 +5019,8 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = tacK lem args in let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in - Sigma.Unsafe.of_pair (tac, evd) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac + end let abstract_subproof ~opaque id gk tac = cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args))) @@ -5093,7 +5047,7 @@ let tclABSTRACT ?(opaque=true) name_op tac = abstract_subproof ~opaque s gk tac let unify ?(state=full_transparent_state) x y = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in try let core_flags = @@ -5106,12 +5060,11 @@ let unify ?(state=full_transparent_state) x y = merge_unify_flags = core_flags; subterm_unify_flags = { core_flags with modulo_delta = empty_transparent_state } } in - let sigma = Sigma.to_evar_map sigma in let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in - Sigma.Unsafe.of_pair (Proofview.tclUNIT (), sigma) + Proofview.Unsafe.tclEVARS sigma with e when CErrors.noncritical e -> - Sigma.here (Tacticals.New.tclFAIL 0 (str"Not unifiable")) sigma - end } + Tacticals.New.tclFAIL 0 (str"Not unifiable") + end module Simple = struct (** Simplified version of some of the above tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 0dbcce02c5..ec8fe11456 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -29,7 +29,7 @@ open Locus (** {6 General functions. } *) -val is_quantified_hypothesis : Id.t -> ('a, 'r) Proofview.Goal.t -> bool +val is_quantified_hypothesis : Id.t -> 'a Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) @@ -75,7 +75,7 @@ val intros : unit Proofview.tactic (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in the conclusion of goal [g], up to head-reduction if [b] is [true] *) val depth_of_quantified_hypothesis : - bool -> quantified_hypothesis -> ('a, 'r) Proofview.Goal.t -> int + bool -> quantified_hypothesis -> 'a Proofview.Goal.t -> int val intros_until : quantified_hypothesis -> unit Proofview.tactic @@ -131,7 +131,7 @@ val exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic type tactic_reduction = env -> evar_map -> constr -> constr -type change_arg = patvar_map -> constr Sigma.run +type change_arg = patvar_map -> evar_map -> evar_map * constr val make_change_arg : constr -> change_arg val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic @@ -211,8 +211,6 @@ val apply_delayed_in : (clear_flag * delayed_open_constr_with_bindings located) list -> intro_pattern option -> unit Proofview.tactic -val run_delayed : Environ.env -> evar_map -> 'a delayed_open -> 'a * evar_map - (** {6 Elimination tactics. } *) (* @@ -437,7 +435,7 @@ end module New : sig - val refine : ?unsafe:bool -> constr Sigma.run -> unit Proofview.tactic + val refine : ?unsafe:bool -> (evar_map -> evar_map * constr) -> unit Proofview.tactic (** [refine ?unsafe c] is [Refine.refine ?unsafe c] followed by beta-iota-reduction of the conclusion. *) |