aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml18
-rw-r--r--tactics/auto.mli1
-rw-r--r--tactics/autorewrite.ml58
-rw-r--r--tactics/autorewrite.mli6
-rw-r--r--tactics/btermdn.mli1
-rw-r--r--tactics/class_tactics.ml77
-rw-r--r--tactics/class_tactics.mli4
-rw-r--r--tactics/contradiction.ml6
-rw-r--r--tactics/contradiction.mli1
-rw-r--r--tactics/dnet.mli2
-rw-r--r--tactics/eauto.ml14
-rw-r--r--tactics/eauto.mli2
-rw-r--r--tactics/elim.ml1
-rw-r--r--tactics/elim.mli1
-rw-r--r--tactics/eqdecide.ml61
-rw-r--r--tactics/eqschemes.ml13
-rw-r--r--tactics/equality.ml90
-rw-r--r--tactics/equality.mli4
-rw-r--r--tactics/hints.ml40
-rw-r--r--tactics/hints.mli1
-rw-r--r--tactics/hipattern.ml25
-rw-r--r--tactics/hipattern.mli1
-rw-r--r--tactics/inv.ml23
-rw-r--r--tactics/inv.mli1
-rw-r--r--tactics/leminv.ml15
-rw-r--r--tactics/leminv.mli1
-rw-r--r--tactics/tacticals.ml50
-rw-r--r--tactics/tacticals.mli6
-rw-r--r--tactics/tactics.ml271
-rw-r--r--tactics/tactics.mli4
-rw-r--r--tactics/term_dnet.ml2
31 files changed, 405 insertions, 395 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 74cb7a364f..b76c0a96ae 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -10,16 +10,12 @@ module CVars = Vars
open Pp
open Util
-open CErrors
open Names
-open Vars
open Termops
open EConstr
open Environ
-open Tacmach
open Genredexpr
open Tactics
-open Tacticals
open Clenv
open Locus
open Proofview.Notations
@@ -178,8 +174,7 @@ let global_info_auto = ref false
let add_option ls refe =
let _ = Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = String.concat " " ls;
Goptions.optkey = ls;
Goptions.optread = (fun () -> !refe);
@@ -380,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.V82.tactic (fun gl -> error "eres_pf")
+ | ERes_pf _ -> Proofview.Goal.enter { enter = fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf") }
| Give_exact (c, cl) -> exact poly (c, cl)
| Res_pf_THEN_trivial_fail (c,cl) ->
Tacticals.New.tclTHEN
@@ -389,10 +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.V82.tactic (fun gl ->
- if exists_evaluable_reference (pf_env gl) c then
- tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl
- else tclFAIL 0 (str"Unbound reference") gl)
+ Proofview.Goal.enter { enter = begin fun gl ->
+ if exists_evaluable_reference (Tacmach.New.pf_env gl) c then
+ Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
+ else Tacticals.New.tclFAIL 0 (str"Unbound reference")
+ end }
| Extern tacast ->
conclPattern concl p tacast
in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 32710e3470..9ed9f0ae26 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -9,7 +9,6 @@
(** This files implements auto and related automation tactics *)
open Names
-open Term
open EConstr
open Clenv
open Pattern
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index e58ec5a31f..de544fe5f9 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -9,8 +9,6 @@
open Equality
open Names
open Pp
-open Tacticals
-open Tactics
open Term
open Termops
open CErrors
@@ -86,7 +84,7 @@ let print_rewrite_hintdb bas =
Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac)
(find_rewrites bas))
-type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option
+type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) Loc.located
(* Applies all the rules of one base *)
let one_base general_rewrite_maybe_in tac_main bas =
@@ -127,45 +125,13 @@ let autorewrite ?(conds=Naive) tac_main lbas =
(Proofview.tclUNIT()) lbas))
let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { 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 =
- let id = ref id in
- let to_be_cleared = ref false in
- fun dir cstr tac gl ->
- let last_hyp_id =
- match Tacmach.pf_hyps gl with
- d :: _ -> Context.Named.Declaration.get_id d
- | _ -> (* even the hypothesis id is missing *)
- raise (Logic.RefinerError (Logic.NoSuchHyp !id))
- in
- let gl' = Proofview.V82.of_tactic (general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false !id cstr false) gl in
- let gls = gl'.Evd.it in
- match gls with
- g::_ ->
- (match Environ.named_context_of_val (Goal.V82.hyps gl'.Evd.sigma g) with
- d ::_ ->
- let lastid = Context.Named.Declaration.get_id d in
- if not (Id.equal last_hyp_id lastid) then
- begin
- let gl'' =
- if !to_be_cleared then
- tclTHEN (fun _ -> gl') (tclTRY (Proofview.V82.of_tactic (clear [!id]))) gl
- else gl' in
- id := lastid ;
- to_be_cleared := true ;
- gl''
- end
- else
- begin
- to_be_cleared := false ;
- gl'
- end
- | _ -> assert false) (* there must be at least an hypothesis *)
- | _ -> assert false (* rewriting cannot complete a proof *)
- in
- let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y (EConstr.of_constr z) w) in
+ let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in
+ let general_rewrite_in id dir cstr tac =
+ let cstr = EConstr.of_constr cstr in
+ general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false id cstr false
+ in
Tacticals.New.tclMAP (fun id ->
Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS
(List.fold_left (fun tac bas ->
@@ -291,12 +257,12 @@ let decompose_applied_relation metas env sigma c ctype left2right =
| Some c -> Some c
| None -> None
-let find_applied_relation metas loc env sigma c left2right =
+let find_applied_relation ?loc metas env sigma c left2right =
let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in
match decompose_applied_relation metas env sigma c ctype left2right with
| Some c -> c
| None ->
- user_err ~loc ~hdr:"decompose_applied_relation"
+ user_err ?loc ~hdr:"decompose_applied_relation"
(str"The type" ++ spc () ++ Printer.pr_econstr_env env sigma ctype ++
spc () ++ str"of this term does not end with an applied relation.")
@@ -305,13 +271,13 @@ let add_rew_rules base lrul =
let counter = ref 0 in
let env = Global.env () in
let sigma = Evd.from_env env in
- let ist = { Genintern.ltacvars = Id.Set.empty; genv = Global.env () } in
+ let ist = Genintern.empty_glob_sign (Global.env ()) in
let intern tac = snd (Genintern.generic_intern ist tac) in
let lrul =
List.fold_left
- (fun dn (loc,(c,ctx),b,t) ->
+ (fun dn (loc,((c,ctx),b,t)) ->
let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
- let info = find_applied_relation false loc env sigma c b in
+ let info = find_applied_relation ?loc false env sigma c b in
let pat = if b then info.hyp_left else info.hyp_right in
let rul = { rew_lemma = c; rew_type = info.hyp_ty;
rew_pat = pat; rew_ctx = ctx; rew_l2r = b;
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 49e8588da3..f765318d04 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -12,7 +12,7 @@ open Term
open Equality
(** Rewriting rules before tactic interpretation *)
-type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option
+type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) Loc.located
(** To add rewriting rules to a base *)
val add_rew_rules : string -> raw_rew_rule list -> unit
@@ -56,7 +56,7 @@ type hypinfo = {
hyp_right : constr;
}
-val find_applied_relation : bool ->
- Loc.t ->
+val find_applied_relation :
+ ?loc:Loc.t -> bool ->
Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 2a5e7c3458..27f624f716 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Term
open Pattern
open Names
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index ea19660931..46d66b9d06 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -18,9 +18,7 @@ open Names
open Term
open Termops
open EConstr
-open Reduction
open Proof_type
-open Tacticals
open Tacmach
open Tactics
open Clenv
@@ -94,8 +92,7 @@ open Goptions
let _ =
declare_bool_option
- { optsync = true;
- optdepr = true;
+ { optdepr = true;
optname = "do typeclass search modulo eta conversion";
optkey = ["Typeclasses";"Modulo";"Eta"];
optread = get_typeclasses_modulo_eta;
@@ -103,8 +100,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "do typeclass search avoiding eta-expansions " ^
" in proof terms (expensive)";
optkey = ["Typeclasses";"Limit";"Intros"];
@@ -113,8 +109,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "during typeclass resolution, solve instances according to their dependency order";
optkey = ["Typeclasses";"Dependency";"Order"];
optread = get_typeclasses_dependency_order;
@@ -122,8 +117,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "use iterative deepening strategy";
optkey = ["Typeclasses";"Iterative";"Deepening"];
optread = get_typeclasses_iterative_deepening;
@@ -131,8 +125,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "compat";
optkey = ["Typeclasses";"Legacy";"Resolution"];
optread = get_typeclasses_legacy_resolution;
@@ -140,8 +133,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "compat";
optkey = ["Typeclasses";"Filtered";"Unification"];
optread = get_typeclasses_filtered_unification;
@@ -149,8 +141,7 @@ let _ =
let set_typeclasses_debug =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "debug output for typeclasses proof search";
optkey = ["Typeclasses";"Debug"];
optread = get_typeclasses_debug;
@@ -158,8 +149,7 @@ let set_typeclasses_debug =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "debug output for typeclasses proof search";
optkey = ["Debug";"Typeclasses"];
optread = get_typeclasses_debug;
@@ -167,8 +157,7 @@ let _ =
let _ =
declare_int_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "verbosity of debug output for typeclasses proof search";
optkey = ["Typeclasses";"Debug";"Verbosity"];
optread = get_typeclasses_verbose;
@@ -176,8 +165,7 @@ let _ =
let set_typeclasses_depth =
declare_int_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "depth for typeclasses proof search";
optkey = ["Typeclasses";"Depth"];
optread = get_typeclasses_depth;
@@ -221,18 +209,22 @@ let auto_unif_flags freeze st =
resolve_evars = false
}
-let e_give_exact flags poly (c,clenv) gl =
+let e_give_exact flags poly (c,clenv) =
+ let open Tacmach.New in
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
+ let sigma = project gl in
let (c, _, _) = c in
- let c, gl =
+ let c, sigma =
if poly then
let clenv', subst = Clenv.refresh_undefined_univs clenv in
- let evd = evars_reset_evd ~with_conv_pbs:true gl.sigma clenv'.evd in
+ let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in
let c = Vars.subst_univs_level_constr subst c in
- c, {gl with sigma = evd}
- else c, gl
+ c, evd
+ else c, sigma
in
- let t1 = pf_unsafe_type_of gl c in
- Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
+ let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
+ Sigma.Unsafe.of_pair (Clenvtac.unify ~flags t1 <*> exact_no_check c, sigma)
+ end }
let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
let clenv', c = connect_hint_clenv poly c clenv gls in
@@ -353,12 +345,12 @@ let shelve_dependencies gls =
let hintmap_of sigma hdc secvars concl =
match hdc with
- | None -> fun db -> Hint_db.map_none secvars db
+ | None -> fun db -> Hint_db.map_none ~secvars db
| Some hdc ->
fun db ->
if Hint_db.use_dn db then (* Using dnet *)
- Hint_db.map_eauto sigma secvars hdc concl db
- else Hint_db.map_existential sigma secvars hdc concl db
+ Hint_db.map_eauto sigma ~secvars hdc concl db
+ else Hint_db.map_existential sigma ~secvars hdc concl db
(** Hack to properly solve dependent evars that are typeclasses *)
let rec e_trivial_fail_db only_classes db_list local_db secvars =
@@ -455,15 +447,14 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
{ enter = fun gl -> unify_resolve_refine poly flags gl (c,None,clenv) } in
Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
- Proofview.V82.tactic (e_give_exact flags poly (c,clenv))
+ e_give_exact flags poly (c,clenv)
| Res_pf_THEN_trivial_fail (term,cl) ->
let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
let snd = if complete then Tacticals.New.tclIDTAC
else e_trivial_fail_db only_classes db_list local_db secvars in
Tacticals.New.tclTHEN fst snd
| Unfold_nth c ->
- let tac = Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c]) in
- Proofview.V82.tactic (tclWEAK_PROGRESS tac)
+ Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c])
| Extern tacast -> conclPattern concl p tacast
in
let tac = run_hint t tac in
@@ -590,7 +581,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
info.Vernacexpr.hint_pattern }
in
make_resolves env sigma ~name:(PathHints path)
- (true,false,Flags.is_verbose()) info false
+ (true,false,not !Flags.quiet) info false
(IsConstr (EConstr.of_constr c,Univ.ContextSet.empty)))
hints)
else []
@@ -947,7 +938,7 @@ module V85 = struct
| Some (evd', fk) ->
if unique then
(match get_result (fk NotApplicable) with
- | Some (evd'', fk') -> error "Typeclass resolution gives multiple solutions"
+ | Some (evd'', fk') -> user_err Pp.(str "Typeclass resolution gives multiple solutions")
| None -> evd')
else evd'
@@ -1201,7 +1192,7 @@ module Search = struct
Feedback.msg_debug
(pr_depth info.search_depth ++ str": no match for " ++
Printer.pr_econstr_env (Goal.env gl) s concl ++
- spc () ++ str ", " ++ int (List.length poss) ++
+ str ", " ++ int (List.length poss) ++
str" possibilities");
match e with
| (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx
@@ -1216,7 +1207,6 @@ module Search = struct
let intro_tac info kont gl =
let open Proofview in
- let open Proofview.Notations in
let env = Goal.env gl in
let sigma = Goal.sigma gl in
let s = Sigma.to_evar_map sigma in
@@ -1254,7 +1244,6 @@ module Search = struct
let search_tac_gl ?st only_classes dep hints depth i sigma gls gl :
unit Proofview.tactic =
let open Proofview in
- let open Proofview.Notations in
if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then
Tacticals.New.tclZEROMSG (str"Not a subgoal for a class")
else
@@ -1614,9 +1603,11 @@ let not_evar c =
| Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
| _ -> Proofview.tclUNIT ()
-let is_ground c gl =
- if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
- else tclFAIL 0 (str"Not ground") gl
+let is_ground c =
+ let open Tacticals.New in
+ Proofview.tclEVARMAP >>= fun sigma ->
+ if Evarutil.is_ground_term sigma c then tclIDTAC
+ else tclFAIL 0 (str"Not ground")
let autoapply c i =
let open Proofview.Notations in
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index a38be5972f..c5731e3779 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -9,9 +9,7 @@
(** This files implements typeclasses eauto *)
open Names
-open Constr
open EConstr
-open Tacmach
val catchable : exn -> bool
@@ -33,7 +31,7 @@ val head_of_constr : Id.t -> constr -> unit Proofview.tactic
val not_evar : constr -> unit Proofview.tactic
-val is_ground : constr -> tactic
+val is_ground : constr -> unit Proofview.tactic
val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 63f923dfd3..fe44559ed8 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -20,7 +20,7 @@ module NamedDecl = Context.Named.Declaration
(* Absurd *)
let mk_absurd_proof t =
- let build_coq_not () = EConstr.of_constr (build_coq_not ()) in
+ let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ()) in
let id = Namegen.default_dependent_ident in
mkLambda (Names.Name id,mkApp(build_coq_not (),[|t|]),
mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
@@ -31,11 +31,11 @@ let absurd c =
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 Loc.ghost env sigma j in
+ let sigma, j = Coercion.inh_coerce_to_sort env sigma j in
let t = j.Environ.utj_val in
let tac =
Tacticals.New.tclTHENLIST [
- elim_type (EConstr.of_constr (build_coq_False ()));
+ elim_type (EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ()));
Simple.apply (mk_absurd_proof t)
] in
Sigma.Unsafe.of_pair (tac, sigma)
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 510b135b0a..2cf5a68298 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Term
open EConstr
open Misctypes
diff --git a/tactics/dnet.mli b/tactics/dnet.mli
index 9f29c60b60..565a916f8e 100644
--- a/tactics/dnet.mli
+++ b/tactics/dnet.mli
@@ -26,7 +26,7 @@
distincts, or you'll get unexpected behaviours.
Warning 2: This structure is perfect, i.e. the set of candidates
- returned is equal to the set of solutions. Beware of DeBruijn
+ returned is equal to the set of solutions. Beware of de Bruijn
shifts and sorts subtyping though (which makes the comparison not
symmetric, see term_dnet.ml).
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 8d1e0e507a..986f531397 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -62,7 +62,7 @@ let registered_e_assumption =
let first_goal gls =
let gl = gls.Evd.it and sig_0 = gls.Evd.sigma in
- if List.is_empty gl then error "first_goal";
+ if List.is_empty gl then user_err Pp.(str "first_goal");
{ Evd.it = List.hd gl; Evd.sigma = sig_0; }
(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
@@ -73,7 +73,7 @@ let apply_tac_list tac glls =
| (g1::rest) ->
let gl = apply_sig_tac sigr tac g1 in
repackage sigr (gl@rest)
- | _ -> error "apply_tac_list"
+ | _ -> user_err Pp.(str "apply_tac_list")
let one_step l gl =
[Proofview.V82.of_tactic Tactics.intro]
@@ -82,7 +82,7 @@ let one_step l gl =
@ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl))
let rec prolog l n gl =
- if n <= 0 then error "prolog - failure";
+ if n <= 0 then user_err Pp.(str "prolog - failure");
let prol = (prolog l (n-1)) in
(tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
@@ -331,8 +331,7 @@ let global_info_eauto = ref false
let _ =
Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "Debug Eauto";
Goptions.optkey = ["Debug";"Eauto"];
Goptions.optread = (fun () -> !global_debug_eauto);
@@ -340,8 +339,7 @@ let _ =
let _ =
Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "Info Eauto";
Goptions.optkey = ["Info";"Eauto"];
Goptions.optread = (fun () -> !global_info_eauto);
@@ -404,7 +402,7 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
s.tacres
with Not_found ->
pr_info_nop d;
- error "eauto: search failed"
+ user_err Pp.(str "eauto: search failed")
(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *)
(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *)
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index e2006ac1e3..c952f4e721 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -6,9 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Term
open EConstr
-open Proof_type
open Hints
open Tactypes
diff --git a/tactics/elim.ml b/tactics/elim.ml
index e37ec6bce2..855cb206fe 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -8,7 +8,6 @@
open Util
open Names
-open Term
open Termops
open EConstr
open Inductiveops
diff --git a/tactics/elim.mli b/tactics/elim.mli
index dc1af79ba0..fb7cc7b838 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Term
open EConstr
open Tacticals
open Misctypes
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index bac3980d2b..bda25d7f02 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -25,7 +25,6 @@ open Constr_matching
open Misctypes
open Tactypes
open Hipattern
-open Pretyping
open Proofview.Notations
open Tacmach.New
open Coqlib
@@ -67,9 +66,26 @@ let choose_noteq eqonleft =
else
left_with_bindings false Misctypes.NoBindings
-let mkBranches c1 c2 =
+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 ->
+ let env = Proofview.Goal.env gl in
+ let store = Proofview.Goal.extra gl in
+ Refine.refine ~unsafe:true { Sigma.run = 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 mkBranches (eqonleft,mk,c1,c2,typ) =
tclTHENLIST
- [generalize [c2];
+ [generalize_right mk typ c1 c2;
Simple.elim c1;
intros;
onLastHyp Simple.case;
@@ -90,8 +106,8 @@ let solveNoteqBranch side =
let make_eq () =
(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
-let build_coq_not () = EConstr.of_constr (build_coq_not ())
-let build_coq_sumbool () = EConstr.of_constr (build_coq_sumbool ())
+let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ())
+let build_coq_sumbool () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_sumbool ())
let mkDecideEqGoal eqonleft op rectype c1 c2 =
let equality = mkApp(make_eq(), [|rectype; c1; c2|]) in
@@ -145,15 +161,32 @@ let diseqCase hyps eqonleft =
open Proofview.Notations
-(* spiwack: a small wrapper around [Hipattern]. *)
+(* spiwack: a PatternMatchingFailure wrapper around [Hipattern]. *)
let match_eqdec sigma c =
- try Proofview.tclUNIT (match_eqdec sigma c)
+ try
+ let (eqonleft,_,c1,c2,ty) = match_eqdec sigma c in
+ let (op,eq1,noteq,eq2) =
+ match EConstr.kind sigma c with
+ | App (op,[|ty1;ty2|]) ->
+ let ty1, ty2 = if eqonleft then ty1, ty2 else ty2, ty1 in
+ (match EConstr.kind sigma ty1, EConstr.kind sigma ty2 with
+ | App (eq1,_), App (noteq,[|neq|]) ->
+ (match EConstr.kind sigma neq with
+ | App (eq2,_) -> op,eq1,noteq,eq2
+ | _ -> assert false)
+ | _ -> assert false)
+ | _ -> assert false in
+ let mk t x y =
+ let eq = mkApp (eq1,[|t;x;y|]) in
+ let neq = mkApp (noteq,[|mkApp (eq2,[|t;x;y|])|]) in
+ if eqonleft then mkApp (op,[|eq;neq|]) else mkApp (op,[|neq;eq|]) in
+ Proofview.tclUNIT (eqonleft,mk,c1,c2,ty)
with PatternMatchingFailure -> Proofview.tclZERO PatternMatchingFailure
(* /spiwack *)
-let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
+let rec solveArg hyps eqonleft mk largs rargs = match largs, rargs with
| [], [] ->
tclTHENLIST [
choose_eq eqonleft;
@@ -163,8 +196,8 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
| a1 :: largs, a2 :: rargs ->
Proofview.Goal.enter { enter = begin fun gl ->
let rectype = pf_unsafe_type_of gl a1 in
- let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
- let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in
+ let decide = mk rectype a1 a2 in
+ let tac hyp = solveArg (hyp :: hyps) eqonleft mk largs rargs in
let subtacs =
if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto]
else [diseqCase hyps eqonleft;eqCase tac;default_auto] in
@@ -178,13 +211,13 @@ let solveEqBranch rectype =
Proofview.Goal.enter { enter = begin fun gl ->
let concl = pf_concl gl in
let sigma = project gl in
- match_eqdec sigma concl >>= fun (eqonleft,op,lhs,rhs,_) ->
+ match_eqdec sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) ->
let (mib,mip) = Global.lookup_inductive rectype in
let nparams = mib.mind_nparams in
let getargs l = List.skipn nparams (snd (decompose_app sigma l)) in
let rargs = getargs rhs
and largs = getargs lhs in
- solveArg [] eqonleft op largs rargs
+ solveArg [] eqonleft mk largs rargs
end }
end
begin function (e, info) -> match e with
@@ -204,14 +237,14 @@ let decideGralEquality =
Proofview.Goal.enter { enter = begin fun gl ->
let concl = pf_concl gl in
let sigma = project gl in
- match_eqdec sigma concl >>= fun (eqonleft,_,c1,c2,typ) ->
+ match_eqdec sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) ->
let headtyp = hd_app sigma (pf_compute gl typ) in
begin match EConstr.kind sigma headtyp with
| Ind (mi,_) -> Proofview.tclUNIT mi
| _ -> tclZEROMSG (Pp.str"This decision procedure only works for inductive objects.")
end >>= fun rectype ->
(tclTHEN
- (mkBranches c1 c2)
+ (mkBranches data)
(tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
end }
end
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index b08456f2f1..bcd31cb7e7 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -103,7 +103,13 @@ let get_coq_eq ctx =
(Universes.fresh_inductive_instance (Global.env ()) eq) in
mkIndU eq, mkConstructUi (eq,1), ctx
with Not_found ->
- error "eq not found."
+ user_err Pp.(str "eq not found.")
+
+let univ_of_eq env eq =
+ let eq = EConstr.of_constr eq in
+ match kind_of_term (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with
+ | Prod (_,t,_) -> (match kind_of_term t with Sort (Type u) -> u | _ -> assert false)
+ | _ -> assert false
(**********************************************************************)
(* Check if an inductive type [ind] has the form *)
@@ -114,6 +120,8 @@ let get_coq_eq ctx =
(* in which case, a symmetry lemma is definable *)
(**********************************************************************)
+let error msg = user_err Pp.(str msg)
+
let get_sym_eq_data env (ind,u) =
let (mib,mip as specif) = lookup_mind_specif env ind in
if not (Int.equal (Array.length mib.mind_packets) 1) ||
@@ -761,7 +769,7 @@ let build_congr env (eq,refl,ctx) ind =
let ty = RelDecl.get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in
let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
let _,constrargs = decompose_app ccl in
- if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then
+ if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
error "Constructor must have no arguments";
let b = List.nth constrargs (i + mib.mind_nparams - 1) in
let varB = fresh env (Id.of_string "B") in
@@ -769,6 +777,7 @@ let build_congr env (eq,refl,ctx) ind =
let varf = fresh env (Id.of_string "f") in
let ci = make_case_info (Global.env()) ind RegularStyle in
let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in
+ let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in
let c =
my_it_mkLambda_or_LetIn paramsctxt
(mkNamedLambda varB (mkSort (Type uni))
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7ae7446c82..e6278943df 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -14,7 +14,6 @@ open Names
open Nameops
open Term
open Termops
-open Environ
open EConstr
open Vars
open Namegen
@@ -58,8 +57,7 @@ let discr_do_intro () =
open Goptions
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic introduction of hypotheses by discriminate";
optkey = ["Discriminate";"Introduction"];
optread = (fun () -> !discriminate_introduction);
@@ -73,8 +71,7 @@ let use_injection_pattern_l2r_order () =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "injection left-to-right pattern order and clear by default when with introduction pattern";
optkey = ["Injection";"L2R";"Pattern";"Order"];
optread = (fun () -> !injection_pattern_l2r_order) ;
@@ -88,8 +85,7 @@ let use_injection_in_context () =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "injection in context";
optkey = ["Structural";"Injection"];
optread = (fun () -> !injection_in_context) ;
@@ -97,9 +93,6 @@ let _ =
(* Rewriting tactics *)
-let tclNOTSAMEGOAL tac =
- Proofview.V82.tactic (Tacticals.tclNOTSAMEGOAL (Proofview.V82.of_tactic tac))
-
type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
@@ -171,7 +164,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
let (equiv, args) = decompose_app_vect sigma (Clenv.clenv_type eqclause) in
let arglen = Array.length args in
- let () = if arglen < 2 then error "The term provided is not an applied relation." in
+ let () = if arglen < 2 then user_err Pp.(str "The term provided is not an applied relation.") in
let c1 = args.(arglen - 2) in
let c2 = args.(arglen - 1) in
let try_occ (evd', c') =
@@ -268,6 +261,25 @@ let rewrite_elim with_evars frzevars cls c e =
general_elim_clause with_evars flags cls c e
end }
+let tclNOTSAMEGOAL tac =
+ let goal gl = Proofview.Goal.goal (Proofview.Goal.assume gl) in
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let sigma = project gl in
+ let ev = goal gl in
+ tac >>= fun () ->
+ Proofview.Goal.goals >>= fun gls ->
+ let check accu gl' =
+ gl' >>= fun gl' ->
+ let accu = accu || Goal.V82.same_goal sigma ev (project gl') (goal gl') in
+ Proofview.tclUNIT accu
+ in
+ Proofview.Monad.List.fold_left check false gls >>= fun has_same ->
+ if has_same then
+ tclZEROMSG (str"Tactic generated a subgoal identical to the original goal.")
+ else
+ Proofview.tclUNIT ()
+ end }
+
(* Ad hoc asymmetric general_elim_clause *)
let general_elim_clause with_evars frzevars cls rew elim =
let open Pretype_errors in
@@ -429,7 +441,7 @@ let adjust_rewriting_direction args lft2rgt =
(* equality to a constant, like in eq_true *)
(* more natural to see -> as the rewriting to the constant *)
if not lft2rgt then
- error "Rewriting non-symmetric equality not allowed from right-to-left.";
+ user_err Pp.(str "Rewriting non-symmetric equality not allowed from right-to-left.");
None
| _ ->
(* other equality *)
@@ -642,8 +654,8 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
| Some evd ->
let e = build_coq_eq () in
let sym = build_coq_eq_sym () in
- Tacticals.New.pf_constr_of_global sym (fun sym ->
- Tacticals.New.pf_constr_of_global e (fun e ->
+ Tacticals.New.pf_constr_of_global sym >>= fun sym ->
+ Tacticals.New.pf_constr_of_global e >>= fun e ->
let eq = applist (e, [t1;c1;c2]) in
tclTHENLAST
(replace_core clause l2r eq)
@@ -651,7 +663,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
[assumption;
tclTHEN (apply sym) assumption;
try_prove_eq
- ])))
+ ])
end }
let replace c1 c2 =
@@ -714,14 +726,13 @@ let keep_proof_equalities_for_injection = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "injection on prop arguments";
optkey = ["Keep";"Proof";"Equalities"];
optread = (fun () -> !keep_proof_equalities_for_injection) ;
optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
-let find_positions env sigma t1 t2 =
+let find_positions env sigma ~no_discr t1 t2 =
let project env sorts posn t1 t2 =
let ty1 = get_type_of env sigma t1 in
let s = get_sort_family_of env sigma ty1 in
@@ -752,7 +763,7 @@ let find_positions env sigma t1 t2 =
List.flatten
(List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn))
0 rargs1 rargs2)
- else if Sorts.List.mem InType sorts'
+ else if Sorts.List.mem InType sorts' && not no_discr
then (* see build_discriminator *)
raise (DiscrFound (List.rev posn,sp1,sp2))
else
@@ -776,13 +787,14 @@ let find_positions env sigma t1 t2 =
Inl (path,c1,c2)
let discriminable env sigma t1 t2 =
- match find_positions env sigma t1 t2 with
+ match find_positions env sigma ~no_discr:false t1 t2 with
| Inl _ -> true
| _ -> false
let injectable env sigma t1 t2 =
- match find_positions env sigma t1 t2 with
- | Inl _ | Inr [] | Inr [([],_,_)] -> false
+ match find_positions env sigma ~no_discr:true t1 t2 with
+ | Inl _ -> assert false
+ | Inr [] | Inr [([],_,_)] -> false
| Inr _ -> true
@@ -853,7 +865,7 @@ let descend_then env sigma head dirn =
let IndType (indf,_) =
try find_rectype env sigma (get_type_of env sigma head)
with Not_found ->
- error "Cannot project on an inductive type derived from a dependency." in
+ user_err Pp.(str "Cannot project on an inductive type derived from a dependency.") in
let indp,_ = (dest_ind_family indf) in
let ind, _ = check_privacy env indp in
let (mib,mip) = lookup_mind_specif env ind in
@@ -922,9 +934,9 @@ let build_selector env sigma dirn c ind special default =
let ci = make_case_info env ind RegularStyle in
mkCase (ci, p, c, Array.of_list brl)
-let build_coq_False () = EConstr.of_constr (build_coq_False ())
-let build_coq_True () = EConstr.of_constr (build_coq_True ())
-let build_coq_I () = EConstr.of_constr (build_coq_I ())
+let build_coq_False () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ())
+let build_coq_True () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_True ())
+let build_coq_I () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_I ())
let rec build_discriminator env sigma dirn c = function
| [] ->
@@ -1017,7 +1029,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- match find_positions env sigma t1 t2 with
+ match find_positions env sigma ~no_discr:false t1 t2 with
| Inr _ ->
tclZEROMSG (str"Not a discriminable equality.")
| Inl (cpath, (_,dirn), _) ->
@@ -1190,7 +1202,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in
dflt
with Evarconv.UnableToUnify _ ->
- error "Cannot solve a unification problem."
+ user_err Pp.(str "Cannot solve a unification problem.")
else
let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
| (_sigS,[a;p]) -> (a, p)
@@ -1207,7 +1219,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
let exist_term = EConstr.of_constr exist_term in
applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
else
- error "Cannot solve a unification problem."
+ user_err Pp.(str "Cannot solve a unification problem.")
| None ->
(* This at least happens if what has been detected as a
dependency is not one; use an evasive error message;
@@ -1215,7 +1227,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
tried in the first place in make_iterated_tuple instead
of approximatively computing the free rels; then
unsolved evars would mean not binding rel *)
- error "Cannot solve a unification problem."
+ user_err Pp.(str "Cannot solve a unification problem.")
in
let scf = sigrec_clausal_form siglen ty in
!evdref, Evarutil.nf_evar !evdref scf
@@ -1334,9 +1346,8 @@ let inject_if_homogenous_dependent_pair ty =
pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
- let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
- ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
- let inj2 = EConstr.of_constr inj2 in
+ let inj2 = EConstr.of_constr @@ Universes.constr_of_global @@
+ Coqlib.coq_reference "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
(* cut with the good equality and prove the requested goal *)
tclTHENLIST
@@ -1399,9 +1410,9 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
let env = eq_clause.env in
- match find_positions env sigma t1 t2 with
+ match find_positions env sigma ~no_discr:true t1 t2 with
| Inl _ ->
- tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")
+ assert false
| Inr [] ->
let suggestion =
if !keep_proof_equalities_for_injection then
@@ -1462,13 +1473,13 @@ let simpleInjClause with_evars = function
| Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq ~old:true with_evars clear_flag None)) c
let injConcl = injClause None false None
-let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id)))
+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 ->
let sigma = clause.evd in
let env = Proofview.Goal.env gl in
- match find_positions env sigma t1 t2 with
+ match find_positions env sigma ~no_discr:false t1 t2 with
| Inl (cpath, (_,dirn), _) ->
discr_positions env sigma u clause cpath dirn
| Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
@@ -1664,8 +1675,7 @@ let regular_subst_tactic = ref true
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "more regular behavior of tactic subst";
optkey = ["Regular";"Subst";"Tactic"];
optread = (fun () -> !regular_subst_tactic);
@@ -1876,7 +1886,7 @@ let cond_eq_term c t gl =
let rewrite_assumption_cond cond_eq_term cl =
let rec arec hyps gl = match hyps with
- | [] -> error "No such assumption."
+ | [] -> user_err Pp.(str "No such assumption.")
| hyp ::rest ->
let id = NamedDecl.get_id hyp in
begin
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 5467b4af25..b47be3bbc0 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -8,7 +8,6 @@
(*i*)
open Names
-open Term
open Evd
open EConstr
open Environ
@@ -97,7 +96,10 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic
val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic
val rewriteInConcl : bool -> constr -> unit Proofview.tactic
+(* Tells if tactic "discriminate" is applicable *)
val discriminable : env -> evar_map -> constr -> constr -> bool
+
+(* Tells if tactic "injection" is applicable *)
val injectable : env -> evar_map -> constr -> constr -> bool
(* Subst *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 77ed4330c1..48a7b3f75c 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-module CVars = Vars
-
open Pp
open Util
open CErrors
@@ -61,7 +59,7 @@ let head_constr_bound sigma t =
| _ -> raise Bound
let head_constr sigma c =
- try head_constr_bound sigma c with Bound -> error "Bound head variable."
+ try head_constr_bound sigma c with Bound -> user_err Pp.(str "Bound head variable.")
let decompose_app_bound sigma t =
let t = strip_outer_cast sigma t in
@@ -169,12 +167,11 @@ let write_warn_hint = function
| "Lax" -> warn_hint := `LAX
| "Warn" -> warn_hint := `WARN
| "Strict" -> warn_hint := `STRICT
-| _ -> error "Only the following flags are accepted: Lax, Warn, Strict."
+| _ -> user_err Pp.(str "Only the following flags are accepted: Lax, Warn, Strict.")
let _ =
Goptions.declare_string_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "behavior of non-imported hints";
Goptions.optkey = ["Loose"; "Hint"; "Behavior"];
Goptions.optread = read_warn_hint;
@@ -770,7 +767,7 @@ let rec nb_hyp sigma c = match EConstr.kind sigma c with
let try_head_pattern c =
try head_pattern_bound c
- with BoundPattern -> error "Bound head variable."
+ with BoundPattern -> user_err Pp.(str "Bound head variable.")
let with_uid c = { obj = c; uid = fresh_key () }
@@ -983,8 +980,8 @@ let get_db dbname =
let add_hint dbname hintlist =
let check (_, h) =
let () = if KNmap.mem h.code.uid !statustable then
- error "Conflicting hint keys. This can happen when including \
- twice the same module."
+ user_err Pp.(str "Conflicting hint keys. This can happen when including \
+ twice the same module.")
in
statustable := KNmap.add h.code.uid false !statustable
in
@@ -1160,7 +1157,7 @@ let add_resolves env sigma clist local dbnames =
(fun dbname ->
let r =
List.flatten (List.map (fun (pri, poly, hnf, path, gr) ->
- make_resolves env sigma (true,hnf,Flags.is_verbose())
+ make_resolves env sigma (true,hnf,not !Flags.quiet)
pri poly ~name:path gr) clist)
in
let hint = make_hint ~local dbname (AddHints r) in
@@ -1238,24 +1235,21 @@ let prepare_hint check (poly,local) env init (sigma,c) =
(* We re-abstract over uninstantiated evars and universes.
It is actually a bit stupid to generalize over evars since the first
thing make_resolves will do is to re-instantiate the products *)
- let sigma, subst = Evd.nf_univ_variables sigma in
+ let sigma, _ = Evd.nf_univ_variables sigma in
let c = Evarutil.nf_evar sigma c in
- let c = EConstr.Unsafe.to_constr c in
- let c = CVars.subst_univs_constr subst c in
- let c = EConstr.of_constr c in
let c = drop_extra_implicit_args sigma c in
let vars = ref (collect_vars sigma c) in
let subst = ref [] in
let rec find_next_evar c = match EConstr.kind sigma c with
| Evar (evk,args as ev) ->
(* We skip the test whether args is the identity or not *)
- let t = existential_type sigma ev in
+ let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
let t = List.fold_right (fun (e,id) c -> replace_term sigma e id c) !subst t in
if not (closed0 sigma c) then
- error "Hints with holes dependent on a bound variable not supported.";
+ user_err Pp.(str "Hints with holes dependent on a bound variable not supported.");
if occur_existential sigma t then
(* Not clever enough to construct dependency graph of evars *)
- error "Not clever enough to deal with evars dependent in other evars.";
+ user_err Pp.(str "Not clever enough to deal with evars dependent in other evars.");
raise (Found (c,t))
| _ -> EConstr.iter sigma find_next_evar c in
let rec iter c =
@@ -1282,7 +1276,7 @@ let interp_hints poly =
prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in
let fref r =
let gr = global_with_alias r in
- Dumpglob.add_glob (loc_of_reference r) gr;
+ Dumpglob.add_glob ?loc:(loc_of_reference r) gr;
gr in
let fr r =
evaluable_of_global_reference (Global.env()) (fref r)
@@ -1311,7 +1305,7 @@ let interp_hints poly =
let constr_hints_of_ind qid =
let ind = global_inductive_with_alias qid in
let mib,_ = Global.lookup_inductive ind in
- Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
+ Dumpglob.dump_reference ?loc:(fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
List.init (nconstructors ind)
(fun i -> let c = (ind,i+1) in
let gr = ConstructRef c in
@@ -1322,13 +1316,13 @@ let interp_hints poly =
let pat = Option.map fp patcom in
let l = match pat with None -> [] | Some (l, _) -> l in
let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
- let env = Genintern.({ genv = env; ltacvars }) in
+ let env = Genintern.({ (empty_glob_sign env) with ltacvars }) in
let _, tacexp = Genintern.generic_intern env tacexp in
HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
let add_hints local dbnames0 h =
if String.List.mem "nocore" dbnames0 then
- error "The hint database \"nocore\" is meant to stay empty.";
+ user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
let env = Global.env() in
let sigma = Evd.from_env env in
@@ -1435,7 +1429,7 @@ let pr_hints_db (name,db,hintlist) =
let pr_hint_list_for_head c =
let dbs = current_db () in
let validate (name, db) =
- let hints = List.map (fun v -> 0, v) (Hint_db.map_all Id.Pred.full c db) in
+ let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in
(name, db, hints)
in
let valid_dbs = List.map validate dbs in
@@ -1477,7 +1471,7 @@ let pr_applicable_hint () =
let pts = get_pftreestate () in
let glss = Proof.V82.subgoals pts in
match glss.Evd.it with
- | [] -> CErrors.error "No focused goal."
+ | [] -> CErrors.user_err Pp.(str "No focused goal.")
| g::_ ->
pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g)
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 467fd46d53..3a0339ff57 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -9,7 +9,6 @@
open Pp
open Util
open Names
-open Term
open EConstr
open Environ
open Globnames
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 851554b832..fd5eabe648 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -40,7 +40,6 @@ let mkmeta n = Nameops.make_ident "X" (Some n)
let meta1 = mkmeta 1
let meta2 = mkmeta 2
let meta3 = mkmeta 3
-let meta4 = mkmeta 4
let op2bool = function Some _ -> true | None -> false
@@ -253,16 +252,16 @@ open Decl_kinds
open Evar_kinds
let mkPattern c = snd (Patternops.pattern_of_glob_constr c)
-let mkGApp f args = GApp (Loc.ghost, f, args)
-let mkGHole =
- GHole (Loc.ghost, QuestionMark (Define false), Misctypes.IntroAnonymous, None)
-let mkGProd id c1 c2 =
- GProd (Loc.ghost, Name (Id.of_string id), Explicit, c1, c2)
-let mkGArrow c1 c2 =
- GProd (Loc.ghost, Anonymous, Explicit, c1, c2)
-let mkGVar id = GVar (Loc.ghost, Id.of_string id)
-let mkGPatVar id = GPatVar(Loc.ghost, (false, Id.of_string id))
-let mkGRef r = GRef (Loc.ghost, Lazy.force r, None)
+let mkGApp f args = CAst.make @@ GApp (f, args)
+let mkGHole = CAst.make @@
+ GHole (QuestionMark (Define false), Misctypes.IntroAnonymous, None)
+let mkGProd id c1 c2 = CAst.make @@
+ GProd (Name (Id.of_string id), Explicit, c1, c2)
+let mkGArrow c1 c2 = CAst.make @@
+ GProd (Anonymous, Explicit, c1, c2)
+let mkGVar id = CAst.make @@ GVar (Id.of_string id)
+let mkGPatVar id = CAst.make @@ GPatVar((false, Id.of_string id))
+let mkGRef r = CAst.make @@ GRef (Lazy.force r, None)
let mkGAppRef r args = mkGApp (mkGRef r) args
(** forall x : _, _ x x *)
@@ -461,7 +460,7 @@ let find_this_eq_data_decompose gl eqn =
let eq_args =
try extract_eq_args gl eq_args
with PatternMatchingFailure ->
- error "Don't know what to do with JMeq on arguments not of same type." in
+ user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in
(lbeq,u,eq_args)
let match_eq_nf gls eqn (ref, hetero) =
@@ -478,7 +477,7 @@ let dest_nf_eq gls eqn =
try
snd (first_match (match_eq_nf gls eqn) equalities)
with PatternMatchingFailure ->
- error "Not an equality."
+ user_err Pp.(str "Not an equality.")
(*** Sigma-types *)
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index dd09c3a4d7..82a3d47b59 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Term
open Evd
open EConstr
open Coqlib
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 904a17417a..b951e7ceba 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -13,7 +13,6 @@ open Names
open Nameops
open Term
open Termops
-open Environ
open EConstr
open Vars
open Namegen
@@ -283,9 +282,9 @@ let generalizeRewriteIntros as_mode tac depids id =
end }
let error_too_many_names pats =
- let loc = Loc.join_loc (fst (List.hd pats)) (fst (List.last pats)) in
+ let loc = Loc.merge_opt (fst (List.hd pats)) (fst (List.last pats)) in
Proofview.tclENV >>= fun env ->
- tclZEROMSG ~loc (
+ 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 ++
@@ -293,27 +292,27 @@ let error_too_many_names pats =
let get_names (allow_conj,issimple) (loc, pat as x) = match pat with
| IntroNaming IntroAnonymous | IntroForthcoming _ ->
- error "Anonymous pattern not allowed for inversion equations."
+ user_err Pp.(str "Anonymous pattern not allowed for inversion equations.")
| IntroNaming (IntroFresh _) ->
- error "Fresh pattern not allowed for inversion equations."
+ user_err Pp.(str "Fresh pattern not allowed for inversion equations.")
| IntroAction IntroWildcard ->
- error "Discarding pattern not allowed for inversion equations."
+ user_err Pp.(str "Discarding pattern not allowed for inversion equations.")
| IntroAction (IntroRewrite _) ->
- error "Rewriting pattern not allowed for inversion equations."
+ user_err Pp.(str "Rewriting pattern not allowed for inversion equations.")
| IntroAction (IntroOrAndPattern (IntroAndPattern [])) when allow_conj -> (None, [])
| IntroAction (IntroOrAndPattern (IntroAndPattern ((_,IntroNaming (IntroIdentifier id)) :: _ as l) | IntroOrPattern [(_,IntroNaming (IntroIdentifier id)) :: _ as l ]))
when allow_conj -> (Some id,l)
| IntroAction (IntroOrAndPattern (IntroAndPattern _)) ->
if issimple then
- error"Conjunctive patterns not allowed for simple inversion equations."
+ user_err Pp.(str"Conjunctive patterns not allowed for simple inversion equations.")
else
- error"Nested conjunctive patterns not allowed for inversion equations."
+ user_err Pp.(str"Nested conjunctive patterns not allowed for inversion equations.")
| IntroAction (IntroInjection l) ->
- error "Injection patterns not allowed for inversion equations."
+ user_err Pp.(str "Injection patterns not allowed for inversion equations.")
| IntroAction (IntroOrAndPattern (IntroOrPattern _)) ->
- error "Disjunctive patterns not allowed for inversion equations."
+ user_err Pp.(str "Disjunctive patterns not allowed for inversion equations.")
| IntroAction (IntroApplyOn (c,pat)) ->
- error "Apply patterns not allowed for inversion equations."
+ user_err Pp.(str "Apply patterns not allowed for inversion equations.")
| IntroNaming (IntroIdentifier id) ->
(Some id,[x])
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 446a62f6db..5835e763dd 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Term
open EConstr
open Misctypes
open Tactypes
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index daa962f1d6..83f3da30a9 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -260,22 +260,23 @@ let add_inversion_lemma_exn na com comsort bool tac =
(* Applying a given inversion lemma *)
(* ================================= *)
-let lemInv id c gls =
+let lemInv id c =
+ Proofview.Goal.enter { enter = begin fun gls ->
try
- let open Tacmach in
let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in
let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
- Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
+ Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false
with
| NoSuchBinding ->
user_err
- (hov 0 (pr_econstr_env (Refiner.pf_env gls) (Refiner.project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
+ (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
| UserError (a,b) ->
user_err ~hdr:"LemInv"
(str "Cannot refine current goal with the lemma " ++
- pr_leconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
+ pr_leconstr_env (pf_env gls) (project gls) c)
+ end }
-let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id
+let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id
let lemInvIn id c ids =
Proofview.Goal.enter { enter = begin fun gl ->
@@ -289,7 +290,7 @@ let lemInvIn id c ids =
else
(tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids))
in
- ((tclTHEN (tclTHEN (bring_hyps hyps) (Proofview.V82.tactic (lemInv id c)))
+ ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c))
(intros_replace_ids)))
end }
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 26d4ac994b..a343fc81a7 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Term
open EConstr
open Constrexpr
open Misctypes
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 90b7d6581a..c495b5ece2 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -51,10 +51,8 @@ let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
let tclFAIL = Refiner.tclFAIL
let tclFAIL_lazy = Refiner.tclFAIL_lazy
let tclDO = Refiner.tclDO
-let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
let tclPROGRESS = Refiner.tclPROGRESS
let tclSHOWHYPS = Refiner.tclSHOWHYPS
-let tclNOTSAMEGOAL = Refiner.tclNOTSAMEGOAL
let tclTHENTRY = Refiner.tclTHENTRY
let tclIFTHENELSE = Refiner.tclIFTHENELSE
let tclIFTHENSELSE = Refiner.tclIFTHENSELSE
@@ -71,7 +69,7 @@ let tclTHENSEQ = tclTHENLIST
let nthDecl m gl =
try List.nth (pf_hyps gl) (m-1)
- with Failure _ -> error "No such assumption."
+ with Failure _ -> user_err Pp.(str "No such assumption.")
let nthHypId m gl = nthDecl m gl |> NamedDecl.get_id
let nthHyp m gl = mkVar (nthHypId m gl)
@@ -82,7 +80,7 @@ let lastHyp gl = nthHyp 1 gl
let nLastDecls n gl =
try List.firstn n (pf_hyps gl)
- with Failure _ -> error "Not enough hypotheses in the goal."
+ with Failure _ -> user_err Pp.(str "Not enough hypotheses in the goal.")
let nLastHypsId n gl = List.map (NamedDecl.get_id) (nLastDecls n gl)
let nLastHyps n gl = List.map mkVar (nLastHypsId n gl)
@@ -171,23 +169,23 @@ let fix_empty_or_and_pattern nv l =
| IntroOrPattern [[]] -> IntroOrPattern (List.make nv [])
| _ -> l
-let check_or_and_pattern_size check_and loc names branchsigns =
+let check_or_and_pattern_size ?loc check_and names branchsigns =
let n = Array.length branchsigns in
let msg p1 p2 = strbrk "a conjunctive pattern made of " ++ int p1 ++ (if p1 == p2 then mt () else str " or " ++ int p2) ++ str " patterns" in
let err1 p1 p2 =
- user_err ~loc (str "Expects " ++ msg p1 p2 ++ str ".") in
+ user_err ?loc (str "Expects " ++ msg p1 p2 ++ str ".") in
let errn n =
- user_err ~loc (str "Expects a disjunctive pattern with " ++ int n
+ user_err ?loc (str "Expects a disjunctive pattern with " ++ int n
++ str " branches.") in
let err1' p1 p2 =
- user_err ~loc (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in
- let errforthcoming loc =
- user_err ~loc (strbrk "Unexpected non atomic pattern.") in
+ user_err ?loc (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in
+ let errforthcoming ?loc =
+ user_err ?loc (strbrk "Unexpected non atomic pattern.") in
match names with
| IntroAndPattern l ->
if not (Int.equal n 1) then errn n;
let l' = List.filter (function _,IntroForthcoming _ -> true | _,IntroNaming _ | _,IntroAction _ -> false) l in
- if l' != [] then errforthcoming (fst (List.hd l'));
+ if l' != [] then errforthcoming ?loc:(fst (List.hd l'));
if check_and then
let p1 = List.count (fun x -> x) branchsigns.(0) in
let p2 = List.length branchsigns.(0) in
@@ -195,7 +193,7 @@ let check_or_and_pattern_size check_and loc names branchsigns =
if not (Int.equal p p1 || Int.equal p p2) then err1 p1 p2;
if Int.equal p p1 then
IntroAndPattern
- (List.extend branchsigns.(0) (Loc.ghost,IntroNaming IntroAnonymous) l)
+ (List.extend branchsigns.(0) (Loc.tag @@ IntroNaming IntroAnonymous) l)
else
names
else
@@ -208,20 +206,20 @@ let check_or_and_pattern_size check_and loc names branchsigns =
err1' p1 p2 else errn n;
names
-let get_and_check_or_and_pattern_gen check_and loc names branchsigns =
- let names = check_or_and_pattern_size check_and loc names branchsigns in
+let get_and_check_or_and_pattern_gen ?loc check_and names branchsigns =
+ let names = check_or_and_pattern_size ?loc check_and names branchsigns in
match names with
| IntroAndPattern l -> [|l|]
| IntroOrPattern l -> Array.of_list l
-let get_and_check_or_and_pattern = get_and_check_or_and_pattern_gen true
+let get_and_check_or_and_pattern ?loc = get_and_check_or_and_pattern_gen ?loc true
let compute_induction_names_gen check_and branchletsigns = function
| None ->
Array.make (Array.length branchletsigns) []
| Some (loc,names) ->
let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in
- get_and_check_or_and_pattern_gen check_and loc names branchletsigns
+ get_and_check_or_and_pattern_gen check_and ?loc names branchletsigns
let compute_induction_names = compute_induction_names_gen true
@@ -492,7 +490,7 @@ module New = struct
| [] -> ()
| (evk,evi) :: _ ->
let (loc,_) = evi.Evd.evar_source in
- Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None
+ Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None
let tclWITHHOLES accept_unresolved_holes tac sigma =
tclEVARMAP >>= fun sigma_initial ->
@@ -535,11 +533,11 @@ module New = struct
let hyps = Proofview.Goal.hyps gl in
try
List.nth hyps (m-1)
- with Failure _ -> CErrors.error "No such assumption."
+ with Failure _ -> CErrors.user_err Pp.(str "No such assumption.")
let nLastDecls gl n =
try List.firstn n (Proofview.Goal.hyps gl)
- with Failure _ -> error "Not enough hypotheses in the goal."
+ with Failure _ -> CErrors.user_err Pp.(str "Not enough hypotheses in the goal.")
let nthHypId m gl =
(** We only use [id] *)
@@ -734,13 +732,11 @@ module New = struct
let case_nodep_then_using =
general_elim_then_using gl_make_case_nodep false
- let pf_constr_of_global ref tac =
- Proofview.Goal.enter { enter = begin fun gl ->
- let env = Proofview.Goal.env gl in
- let sigma = Tacmach.New.project gl in
- let (sigma, c) = Evd.fresh_global env sigma ref in
- let c = EConstr.of_constr c in
- Proofview.Unsafe.tclEVARS sigma <*> (tac c)
- end }
+ let pf_constr_of_global ref =
+ Proofview.tclEVARMAP >>= fun sigma ->
+ Proofview.tclENV >>= fun env ->
+ let (sigma, c) = Evd.fresh_global env sigma ref in
+ let c = EConstr.of_constr c in
+ Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c
end
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 3b90ec514a..96270f748e 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -44,10 +44,8 @@ val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : int -> std_ppcmds -> tactic
val tclFAIL_lazy : int -> std_ppcmds Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
-val tclWEAK_PROGRESS : tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclSHOWHYPS : tactic -> tactic
-val tclNOTSAMEGOAL : tactic -> tactic
val tclTHENTRY : tactic -> tactic -> tactic
val tclMAP : ('a -> tactic) -> 'a list -> tactic
@@ -116,7 +114,7 @@ type branch_assumptions = private {
error message if |pats| <> |branchsign|; extends them if no pattern is given
for let-ins in the case of a conjunctive pattern *)
val get_and_check_or_and_pattern :
- Loc.t -> delayed_open_constr or_and_intro_pattern_expr ->
+ ?loc:Loc.t -> delayed_open_constr or_and_intro_pattern_expr ->
bool list array -> intro_patterns array
(** Tolerate "[]" to mean a disjunctive pattern of any length *)
@@ -265,5 +263,5 @@ module New : sig
val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
- val pf_constr_of_global : Globnames.global_reference -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
+ val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic
end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e792585822..7e8cb4e632 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -53,8 +53,6 @@ module NamedDecl = Context.Named.Declaration
let inj_with_occurrences e = (AllOccurrences,e)
-let dloc = Loc.ghost
-
let typ_of env sigma c =
let open Retyping in
try get_type_of ~lax:true env (Sigma.to_evar_map sigma) c
@@ -72,8 +70,7 @@ let use_dependent_propositions_elimination () =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "dependent-propositions-elimination tactic";
optkey = ["Dependent";"Propositions";"Elimination"];
optread = (fun () -> !dependent_propositions_elimination) ;
@@ -81,8 +78,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "trigger bugged context matching compatibility";
optkey = ["Tactic";"Compat";"Context"];
optread = (fun () -> !Flags.tactic_context_compat) ;
@@ -90,7 +86,7 @@ let _ =
let apply_solve_class_goals = ref (false)
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = true;
+ Goptions.optdepr = true;
Goptions.optname =
"Perform typeclass resolution on apply-generated subgoals.";
Goptions.optkey = ["Typeclass";"Resolution";"After";"Apply"];
@@ -104,8 +100,7 @@ let use_clear_hyp_by_default () = !clear_hyp_by_default
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "default clearing of hypotheses after use";
optkey = ["Default";"Clearing";"Used";"Hypotheses"];
optread = (fun () -> !clear_hyp_by_default) ;
@@ -121,8 +116,7 @@ let accept_universal_lemma_under_conjunctions () =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "trivial unification in tactics applying under conjunctions";
optkey = ["Universal";"Lemma";"Under";"Conjunction"];
optread = (fun () -> !universal_lemma_under_conjunctions) ;
@@ -134,8 +128,7 @@ let shrink_abstract = ref true
let _ =
declare_bool_option
- { optsync = true;
- optdepr = true;
+ { optdepr = true;
optname = "shrinking of abstracted proofs";
optkey = ["Shrink"; "Abstract"];
optread = (fun () -> !shrink_abstract) ;
@@ -155,8 +148,7 @@ let use_bracketing_last_or_and_intro_pattern () =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "bracketing last or-and introduction pattern";
optkey = ["Bracketing";"Last";"Introduction";"Pattern"];
optread = (fun () -> !bracketing_last_or_and_intro_pattern);
@@ -203,6 +195,7 @@ let introduction ?(check=true) id =
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 ->
@@ -427,11 +420,11 @@ let default_id env sigma decl =
type name_flag =
| NamingAvoid of Id.t list
| NamingBasedOn of Id.t * Id.t list
- | NamingMustBe of Loc.t * Id.t
+ | NamingMustBe of Id.t Loc.located
let naming_of_name = function
| Anonymous -> NamingAvoid []
- | Name id -> NamingMustBe (dloc,id)
+ | Name id -> NamingMustBe (Loc.tag id)
let find_name mayrepl decl naming gl = match naming with
| NamingAvoid idl ->
@@ -445,7 +438,7 @@ let find_name mayrepl decl naming gl = match naming with
let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in
let id' = next_ident_away id ids_of_hyps in
if not mayrepl && not (Id.equal id' id) then
- user_err ~loc (pr_id id ++ str" is already used.");
+ user_err ?loc (pr_id id ++ str" is already used.");
id
(**************************************************************)
@@ -469,7 +462,7 @@ let assert_before_gen b naming t =
assert_before_then_gen b naming t (fun _ -> Proofview.tclUNIT ())
let assert_before na = assert_before_gen false (naming_of_name na)
-let assert_before_replacing id = assert_before_gen true (NamingMustBe (dloc,id))
+let assert_before_replacing id = assert_before_gen true (NamingMustBe (Loc.tag id))
let assert_after_then_gen b naming t tac =
let open Context.Rel.Declaration in
@@ -488,7 +481,7 @@ let assert_after_gen b naming t =
assert_after_then_gen b naming t (fun _ -> (Proofview.tclUNIT ()))
let assert_after na = assert_after_gen false (naming_of_name na)
-let assert_after_replacing id = assert_after_gen true (NamingMustBe (dloc,id))
+let assert_after_replacing id = assert_after_gen true (NamingMustBe (Loc.tag id))
(**************************************************************)
(* Fixpoints and CoFixpoints *)
@@ -512,6 +505,9 @@ let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast
else
let open Context.Rel.Declaration in
check_mutind (push_rel (LocalAssum (na, c1)) env) sigma (pred k) b
+| LetIn (na, c1, t, b) ->
+ let open Context.Rel.Declaration in
+ check_mutind (push_rel (LocalDef (na, c1, t)) env) sigma k b
| _ -> error "Not enough products."
(* Refine as a fixpoint *)
@@ -969,7 +965,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
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 (dloc,id)) MoveLast true false
+let intro_mustbe_force id = intro_gen (NamingMustBe (Loc.tag id)) MoveLast true false
let intro_using id = intro_gen (NamingBasedOn (id,[])) MoveLast false false
let intro_then = intro_then_gen (NamingAvoid []) MoveLast false false
@@ -979,7 +975,7 @@ let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false
let intro_move_avoid idopt avoid hto = match idopt with
| None -> intro_gen (NamingAvoid avoid) hto true false
- | Some id -> intro_gen (NamingMustBe (dloc,id)) hto true false
+ | Some id -> intro_gen (NamingMustBe (Loc.tag id)) hto true false
let intro_move idopt hto = intro_move_avoid idopt [] hto
@@ -1139,7 +1135,7 @@ let try_intros_until tac = function
let rec intros_move = function
| [] -> Proofview.tclUNIT ()
| (hyp,destopt) :: rest ->
- Tacticals.New.tclTHEN (intro_gen (NamingMustBe (dloc,hyp)) destopt false false)
+ Tacticals.New.tclTHEN (intro_gen (NamingMustBe (Loc.tag hyp)) destopt false false)
(intros_move rest)
let run_delayed env sigma c =
@@ -1291,7 +1287,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
error_uninstantiated_metas new_hyp_typ clenv;
let new_hyp_prf = clenv_value clenv in
let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in
- let naming = NamingMustBe (dloc,targetid) in
+ let naming = NamingMustBe (Loc.tag targetid) in
let with_clear = do_replace (Some id) naming in
Tacticals.New.tclTHEN
(Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
@@ -1736,7 +1732,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind :
with Redelimination ->
(* Last chance: if the head is a variable, apply may try
second order unification *)
- let info = Loc.add_loc info loc in
+ let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in
let tac =
if with_destruct then
descend_in_conjunctions []
@@ -1798,13 +1794,13 @@ let apply_with_delayed_bindings_gen b e l =
(one k f) (aux cbl)
in aux l
-let apply_with_bindings cb = apply_with_bindings_gen false false [None,(dloc,cb)]
+let apply_with_bindings cb = apply_with_bindings_gen false false [None,(Loc.tag cb)]
-let eapply_with_bindings cb = apply_with_bindings_gen false true [None,(dloc,cb)]
+let eapply_with_bindings cb = apply_with_bindings_gen false true [None,(Loc.tag cb)]
-let apply c = apply_with_bindings_gen false false [None,(dloc,(c,NoBindings))]
+let apply c = apply_with_bindings_gen false false [None,(Loc.tag (c,NoBindings))]
-let eapply c = apply_with_bindings_gen false true [None,(dloc,(c,NoBindings))]
+let eapply c = apply_with_bindings_gen false true [None,(Loc.tag (c,NoBindings))]
let apply_list = function
| c::l -> apply_with_bindings (c,ImplicitBindings l)
@@ -1840,8 +1836,8 @@ let progress_with_clause flags innerclause clause =
try List.find_map f ordered_metas
with Not_found -> raise UnableToApply
-let explain_unable_to_apply_lemma loc env sigma thm innerclause =
- user_err ~loc (hov 0
+let explain_unable_to_apply_lemma ?loc env sigma thm innerclause =
+ user_err ?loc (hov 0
(Pp.str "Unable to apply lemma of type" ++ brk(1,1) ++
Pp.quote (Printer.pr_leconstr_env env sigma thm) ++ spc() ++
str "on hypothesis of type" ++ brk(1,1) ++
@@ -1857,7 +1853,7 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
try aux (clenv_push_prod clause)
with NotExtensibleClause ->
match e with
- | UnableToApply -> explain_unable_to_apply_lemma loc env sigma thm innerclause
+ | UnableToApply -> explain_unable_to_apply_lemma ?loc env sigma thm innerclause
| _ -> iraise e'
in
aux (make_clenv_binding env sigma (d,thm) lbind)
@@ -2216,7 +2212,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
(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 (dloc,(cons,lbind)) in
+ let apply_tac = general_apply true false with_evars None (Loc.tag (cons,lbind)) in
let tac =
(Tacticals.New.tclTHENLIST
[
@@ -2283,7 +2279,7 @@ let error_unexpected_extra_pattern loc bound pat =
| IntroNaming (IntroIdentifier _) ->
"name", (String.plural nb " introduction pattern"), "no"
| _ -> "introduction pattern", "", "none" in
- user_err ~loc (str "Unexpected " ++ str s1 ++ str " (" ++
+ user_err ?loc (str "Unexpected " ++ str s1 ++ str " (" ++
(if Int.equal nb 0 then (str s3 ++ str s2) else
(str "at most " ++ int nb ++ str s2)) ++ spc () ++
str (if Int.equal nb 1 then "was" else "were") ++
@@ -2301,7 +2297,7 @@ let my_find_eq_data_decompose gl t =
-> None
| Constr_matching.PatternMatchingFailure -> None
-let intro_decomp_eq loc l thin tac id =
+let intro_decomp_eq ?loc l thin tac id =
Proofview.Goal.enter { enter = begin fun gl ->
let c = mkVar id in
let t = Tacmach.New.pf_unsafe_type_of gl c in
@@ -2309,13 +2305,13 @@ let intro_decomp_eq loc l thin tac id =
match my_find_eq_data_decompose gl t with
| Some (eq,u,eq_args) ->
!intro_decomp_eq_function
- (fun n -> tac ((dloc,id)::thin) (Some (true,n)) l)
+ (fun n -> tac ((Loc.tag id)::thin) (Some (true,n)) l)
(eq,t,eq_args) (c, t)
| None ->
Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
end }
-let intro_or_and_pattern loc with_evars bracketed ll thin tac id =
+let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
Proofview.Goal.enter { enter = begin fun gl ->
let c = mkVar id in
let t = Tacmach.New.pf_unsafe_type_of gl c in
@@ -2323,7 +2319,7 @@ let intro_or_and_pattern loc with_evars bracketed ll thin tac id =
let branchsigns = compute_constructor_signatures false ind in
let nv_with_let = Array.map List.length branchsigns in
let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
- let ll = get_and_check_or_and_pattern loc ll branchsigns in
+ let ll = get_and_check_or_and_pattern ?loc ll branchsigns in
Tacticals.New.tclTHENLASTn
(Tacticals.New.tclTHEN (simplest_ecase c) (clear [id]))
(Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
@@ -2372,8 +2368,8 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
Tacticals.New.tclTHENFIRST eqtac (tac thin)
end }
-let prepare_naming loc = function
- | IntroIdentifier id -> NamingMustBe (loc,id)
+let prepare_naming ?loc = function
+ | IntroIdentifier id -> NamingMustBe (Loc.tag ?loc id)
| IntroAnonymous -> NamingAvoid []
| IntroFresh id -> NamingBasedOn (id,[])
@@ -2392,6 +2388,29 @@ let rec explicit_intro_names = function
explicit_intro_names l
| [] -> []
+let rec check_name_unicity env ok seen = function
+| (_, IntroForthcoming _) :: l -> check_name_unicity env ok seen l
+| (loc, IntroNaming (IntroIdentifier id)) :: l ->
+ (try
+ ignore (if List.mem_f Id.equal id ok then raise Not_found else lookup_named id env);
+ user_err ?loc (pr_id id ++ str" is already used.")
+ with Not_found ->
+ if List.mem_f Id.equal id seen then
+ user_err ?loc (pr_id id ++ str" is used twice.")
+ else
+ check_name_unicity env ok (id::seen) l)
+| (_, IntroAction (IntroOrAndPattern l)) :: l' ->
+ let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in
+ List.iter (fun l -> check_name_unicity env ok seen (l@l')) ll
+| (_, IntroAction (IntroInjection l)) :: l' ->
+ check_name_unicity env ok seen (l@l')
+| (_, IntroAction (IntroApplyOn (c,pat))) :: l' ->
+ check_name_unicity env ok seen (pat::l')
+| (_, (IntroNaming (IntroAnonymous | IntroFresh _)
+ | IntroAction (IntroWildcard | IntroRewrite _))) :: l ->
+ check_name_unicity env ok seen l
+| [] -> ()
+
let wild_id = Id.of_string "_tmp"
let rec list_mem_assoc_right id = function
@@ -2415,7 +2434,7 @@ let make_tmp_naming avoid l = function
case of IntroFresh, we should use check_thin_clash_then anyway to
prevent the case of an IntroFresh precisely using the wild_id *)
| IntroWildcard -> NamingBasedOn (wild_id,avoid@explicit_intro_names l)
- | pat -> NamingAvoid(avoid@explicit_intro_names ((dloc,IntroAction pat)::l))
+ | pat -> NamingAvoid(avoid@explicit_intro_names ((Loc.tag @@ IntroAction pat)::l))
let fit_bound n = function
| None -> true
@@ -2451,7 +2470,7 @@ let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac =
| [] ->
(* Behave as IntroAnonymous *)
intro_patterns_core with_evars b avoid ids thin destopt bound n tac
- [dloc,IntroNaming IntroAnonymous]
+ [Loc.tag @@ IntroNaming IntroAnonymous]
| (loc,pat) :: l ->
if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else
match pat with
@@ -2463,7 +2482,7 @@ let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac =
| IntroAction pat ->
intro_then_gen (make_tmp_naming avoid l pat)
destopt true false
- (intro_pattern_action loc with_evars (b || not (List.is_empty l)) false
+ (intro_pattern_action ?loc with_evars (b || not (List.is_empty l)) false
pat thin destopt
(fun thin bound' -> intro_patterns_core with_evars b avoid ids thin destopt bound' 0
(fun ids thin ->
@@ -2488,21 +2507,21 @@ and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac
destopt true false
(fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)
-and intro_pattern_action loc with_evars b style pat thin destopt tac id =
+and intro_pattern_action ?loc with_evars b style pat thin destopt tac id =
match pat with
| IntroWildcard ->
- tac ((loc,id)::thin) None []
+ tac ((Loc.tag ?loc id)::thin) None []
| IntroOrAndPattern ll ->
- intro_or_and_pattern loc with_evars b ll thin tac id
+ intro_or_and_pattern ?loc with_evars b ll thin tac id
| IntroInjection l' ->
- intro_decomp_eq loc l' thin tac id
+ intro_decomp_eq ?loc l' thin tac id
| IntroRewrite l2r ->
rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None [])
| IntroApplyOn ((loc',f),(loc,pat)) ->
let naming,tac_ipat =
- prepare_intros_loc loc with_evars (IntroIdentifier id) destopt pat in
+ prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in
let doclear =
- if naming = NamingMustBe (loc,id) then
+ if naming = NamingMustBe (Loc.tag ?loc id) then
Proofview.tclUNIT () (* apply_in_once do a replacement *)
else
clear [id] in
@@ -2513,30 +2532,38 @@ and intro_pattern_action loc with_evars b style pat thin destopt tac id =
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 []])
-and prepare_intros_loc loc with_evars dft destopt = function
+and prepare_intros ?loc with_evars dft destopt = function
| IntroNaming ipat ->
- prepare_naming loc ipat,
+ prepare_naming ?loc ipat,
(fun id -> move_hyp id destopt)
| IntroAction ipat ->
- prepare_naming loc dft,
+ prepare_naming ?loc dft,
(let tac thin bound =
intro_patterns_core with_evars true [] [] thin destopt bound 0
(fun _ l -> clear_wildcards l) in
fun id ->
- intro_pattern_action loc with_evars true true ipat [] destopt tac id)
- | IntroForthcoming _ -> user_err ~loc
+ intro_pattern_action ?loc with_evars true true ipat [] destopt tac id)
+ | IntroForthcoming _ -> user_err ?loc
(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 ->
+ 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 }
+
let intro_patterns_bound_to with_evars n destopt =
- intro_patterns_core with_evars true [] [] [] destopt
- (Some (true,n)) 0 (fun _ l -> clear_wildcards l)
+ intro_patterns_head_core with_evars true destopt
+ (Some (true,n))
let intro_patterns_to with_evars destopt =
- intro_patterns_core with_evars (use_bracketing_last_or_and_intro_pattern ())
- [] [] [] destopt None 0 (fun _ l -> clear_wildcards l)
+ intro_patterns_head_core with_evars (use_bracketing_last_or_and_intro_pattern ())
+ destopt None
let intro_pattern_to with_evars destopt pat =
- intro_patterns_to with_evars destopt [dloc,pat]
+ intro_patterns_to with_evars destopt [Loc.tag pat]
let intro_patterns with_evars = intro_patterns_to with_evars MoveLast
@@ -2549,20 +2576,20 @@ let intros_patterns with_evars = function
(* Forward reasoning *)
(**************************)
-let prepare_intros with_evars dft destopt = function
- | None -> prepare_naming dloc dft, (fun _id -> Proofview.tclUNIT ())
- | Some (loc,ipat) -> prepare_intros_loc loc with_evars dft destopt ipat
+let prepare_intros_opt with_evars dft destopt = function
+ | None -> prepare_naming dft, (fun _id -> Proofview.tclUNIT ())
+ | Some (loc,ipat) -> prepare_intros ?loc with_evars dft destopt ipat
let ipat_of_name = function
| Anonymous -> None
- | Name id -> Some (dloc, IntroNaming (IntroIdentifier id))
+ | Name id -> Some (Loc.tag @@ IntroNaming (IntroIdentifier id))
let head_ident sigma c =
let c = fst (decompose_app sigma (snd (decompose_lam_assum sigma c))) in
if isVar sigma c then Some (destVar sigma c) else None
let assert_as first hd ipat t =
- let naming,tac = prepare_intros false IntroAnonymous MoveLast ipat in
+ let naming,tac = prepare_intros_opt false IntroAnonymous MoveLast ipat in
let repl = do_replace hd naming in
let tac = if repl then (fun id -> Proofview.tclUNIT ()) else tac in
if first then assert_before_then_gen repl naming t tac
@@ -2580,10 +2607,10 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
if with_evars then MoveLast (* evars would depend on the whole context *)
else get_previous_hyp_position id gl in
let naming,ipat_tac =
- prepare_intros with_evars (IntroIdentifier id) destopt ipat in
+ prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in
let lemmas_target, last_lemma_target =
let last,first = List.sep_last lemmas in
- List.map (fun lem -> (NamingMustBe (dloc,id),lem)) first, (naming,last)
+ List.map (fun lem -> (NamingMustBe (Loc.tag id),lem)) first, (naming,last)
in
(* We chain apply_in_once, ending with an intro pattern *)
List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id
@@ -2661,7 +2688,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
let tac =
Tacticals.New.tclTHENLIST
[ convert_concl_no_check newcl DEFAULTcast;
- intro_gen (NamingMustBe (dloc,id)) (decode_hyp lastlhyp) true false;
+ intro_gen (NamingMustBe (Loc.tag id)) (decode_hyp lastlhyp) true false;
Tacticals.New.tclMAP convert_hyp_no_check depdecls;
eq_tac ]
in
@@ -2694,7 +2721,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
| IntroFresh heq_base -> fresh_id_in_env [id] heq_base env
| IntroIdentifier id ->
if List.mem id (ids_of_named_context (named_context env)) then
- user_err ~loc (pr_id id ++ str" is already used.");
+ user_err ?loc (pr_id id ++ str" is already used.");
id in
let eqdata = build_coq_eq_data () in
let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
@@ -2811,20 +2838,18 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
mkProd_or_LetIn decl cl', sigma'
let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
- let env = Tacmach.pf_env gl in
- let ids = Tacmach.pf_ids_of_hyps gl in
- let sigma, t = Typing.type_of env sigma c in
- generalize_goal_gen env sigma ids i o t cl
-
-let new_generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
- let env = Tacmach.New.pf_env gl in
- let ids = Tacmach.New.pf_ids_of_hyps gl in
+ let open Tacmach.New in
+ let env = pf_env gl in
+ let ids = pf_ids_of_hyps gl in
let sigma, t = Typing.type_of env sigma c in
generalize_goal_gen env sigma ids i o t cl
-let old_generalize_dep ?(with_let=false) c gl =
+let generalize_dep ?(with_let=false) c =
+ let open Tacmach.New in
+ let open Tacticals.New in
+ Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let env = pf_env gl in
- let sign = pf_hyps gl in
+ let sign = Proofview.Goal.hyps gl in
let sigma = project gl in
let init_ids = ids_of_named_context (Global.named_context()) in
let seek (d:named_declaration) (toquant:named_context) =
@@ -2843,11 +2868,11 @@ let old_generalize_dep ?(with_let=false) c gl =
-> id::tothin
| _ -> tothin
in
- let cl' = it_mkNamedProd_or_LetIn (Tacmach.pf_concl gl) to_quantify in
+ let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
let body =
if with_let then
match EConstr.kind sigma c with
- | Var id -> id |> Tacmach.pf_get_hyp gl |> NamedDecl.get_value
+ | Var id -> id |> (fun id -> pf_get_hyp id gl) |> NamedDecl.get_value
| _ -> None
else None
in
@@ -2856,20 +2881,19 @@ let old_generalize_dep ?(with_let=false) c gl =
(** Check that the generalization is indeed well-typed *)
let (evd, _) = Typing.type_of env evd cl'' in
let args = Context.Named.to_instance mkVar to_quantify_rev in
- tclTHENLIST
- [tclEVARS evd;
- Proofview.V82.of_tactic (apply_type cl'' (if Option.is_empty body then c::args else args));
- Proofview.V82.of_tactic (clear (List.rev tothin'))]
- gl
-
-let generalize_dep ?(with_let = false) c =
- Proofview.V82.tactic (old_generalize_dep ~with_let c)
+ let tac =
+ tclTHEN
+ (apply_type cl'' (if Option.is_empty body then c::args else args))
+ (clear (List.rev tothin'))
+ in
+ Sigma.Unsafe.of_pair (tac, evd)
+ end }
(** *)
let generalize_gen_let lconstr = Proofview.Goal.s_enter { s_enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let newcl, evd =
- List.fold_right_i (new_generalize_goal gl) 0 lconstr
+ List.fold_right_i (generalize_goal gl) 0 lconstr
(Tacmach.New.pf_concl gl,Tacmach.New.project gl)
in
let (evd, _) = Typing.type_of env evd newcl in
@@ -2936,8 +2960,7 @@ let specialize (c,lbind) ipat =
let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
let sigma, term =
if lbind == NoBindings then
- let sigma = Typeclasses.resolve_typeclasses env sigma in
- sigma, nf_evar sigma c
+ sigma, c
else
let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma c) lbind in
let flags = { (default_unify_flags ()) with resolve_evars = true } in
@@ -2961,7 +2984,7 @@ let specialize (c,lbind) ipat =
| Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) ->
(* Like assert (id:=id args) but with the concept of specialization *)
let naming,tac =
- prepare_intros false (IntroIdentifier id) MoveLast ipat in
+ prepare_intros_opt false (IntroIdentifier id) MoveLast ipat in
let repl = do_replace (Some id) naming in
Tacticals.New.tclTHENFIRST
(assert_before_then_gen repl naming typ tac)
@@ -2975,7 +2998,7 @@ let specialize (c,lbind) ipat =
| Some (loc,ipat) ->
(* Like pose proof with extra support for "with" bindings *)
(* even though the "with" bindings forces full application *)
- let naming,tac = prepare_intros_loc loc false IntroAnonymous MoveLast ipat in
+ let naming,tac = prepare_intros ?loc false IntroAnonymous MoveLast ipat in
Tacticals.New.tclTHENFIRST
(assert_before_then_gen false naming typ tac)
(exact_no_check term)
@@ -3063,7 +3086,7 @@ let intropattern_of_name gl avoid = function
| Name id -> IntroNaming (IntroIdentifier (new_fresh_id avoid id gl))
let rec consume_pattern avoid na isdep gl = function
- | [] -> ((dloc, intropattern_of_name gl avoid na), [])
+ | [] -> ((Loc.tag @@ intropattern_of_name gl avoid na), [])
| (loc,IntroForthcoming true)::names when not isdep ->
consume_pattern avoid na isdep gl names
| (loc,IntroForthcoming _)::names as fullpat ->
@@ -3140,7 +3163,7 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
let (recpat,names) = match names with
| [loc,IntroNaming (IntroIdentifier id) as pat] ->
let id' = next_ident_away (add_prefix "IH" id) avoid in
- (pat, [dloc, IntroNaming (IntroIdentifier id')])
+ (pat, [Loc.tag @@ IntroNaming (IntroIdentifier id')])
| _ -> 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 ->
@@ -3498,12 +3521,11 @@ let error_ind_scheme s =
let glob c = EConstr.of_constr (Universes.constr_of_global c)
-let coq_eq = lazy (glob (Coqlib.build_coq_eq ()))
+let coq_eq = lazy (glob (Coqlib.build_coq_eq ()))
let coq_eq_refl = lazy (glob (Coqlib.build_coq_eq_refl ()))
-let coq_heq = lazy (EConstr.of_constr (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq"))
-let coq_heq_refl = lazy (EConstr.of_constr (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl"))
-
+let coq_heq = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq"))
+let coq_heq_refl = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl"))
let mkEq t x y =
mkApp (Lazy.force coq_eq, [| t; x; y |])
@@ -4191,6 +4213,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
let f (_,is_not_let,_,_) = is_not_let in
Array.map (fun (_,l) -> List.map f l) indsign in
let names = compute_induction_names branchletsigns names in
+ Array.iter (check_name_unicity env toclear []) names;
let tac =
(if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
(Tacticals.New.tclTHENLIST [
@@ -4469,7 +4492,7 @@ let induction_gen_l isrec with_evars elim names lc =
let lc = List.map (function
| (c,None) -> c
| (c,Some(loc,eqname)) ->
- user_err ~loc (str "Do not know what to do with " ++
+ user_err ?loc (str "Do not know what to do with " ++
Miscprint.pr_intro_pattern_naming eqname)) lc in
let rec atomize_list l =
match l with
@@ -4724,7 +4747,7 @@ let symmetry_red allowred =
| Some eq_data,_,_ ->
Tacticals.New.tclTHEN
(convert_concl_no_check concl DEFAULTcast)
- (Tacticals.New.pf_constr_of_global eq_data.sym apply)
+ (Tacticals.New.pf_constr_of_global eq_data.sym >>= apply)
| None,eq,eq_kind -> prove_symmetry eq eq_kind
end }
@@ -4820,8 +4843,8 @@ let transitivity_red allowred t =
Tacticals.New.tclTHEN
(convert_concl_no_check concl DEFAULTcast)
(match t with
- | None -> Tacticals.New.pf_constr_of_global eq_data.trans eapply
- | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t]))
+ | None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply
+ | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t])
| None,eq,eq_kind ->
match t with
| None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.")
@@ -4907,7 +4930,7 @@ let shrink_entry sign const =
} in
(const, args)
-let abstract_subproof id gk tac =
+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
@@ -4927,7 +4950,10 @@ let abstract_subproof id gk tac =
else (Context.Named.add d s1,s2))
global_sign (Context.Named.empty, empty_named_context_val) in
let id = next_global_ident_away id (pf_ids_of_hyps gl) in
- let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in
+ let concl = match goal_type with
+ | None -> Proofview.Goal.concl gl
+ | Some ty -> ty in
+ let concl = it_mkNamedProd_or_LetIn concl sign in
let concl =
try flush_and_check_evars !evdref concl
with Uninstantiated_evar _ ->
@@ -4957,8 +4983,8 @@ let abstract_subproof id gk tac =
else (const, List.rev (Context.Named.to_instance Constr.mkVar sign))
in
let args = List.map EConstr.of_constr args in
- let cd = Entries.DefinitionEntry const in
- let decl = (cd, IsProof Lemma) in
+ let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in
+ let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in
let cst () =
(** do not compute the implicit arguments, it may be costly *)
let () = Impargs.make_implicit_args false in
@@ -4976,18 +5002,21 @@ let abstract_subproof id gk tac =
Entries.(snd (Future.force const.const_entry_body)) in
let solve =
Proofview.tclEFFECTS effs <*>
- exact_no_check (applist (lem, args))
+ 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 }
+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)))
+
let anon_id = Id.of_string "anonymous"
-let tclABSTRACT name_op tac =
+let name_op_to_name name_op object_kind suffix =
let open Proof_global in
- let default_gk = (Global, false, Proof Theorem) in
- let s, gk = match name_op with
+ let default_gk = (Global, false, object_kind) in
+ match name_op with
| Some s ->
(try let _, gk, _ = current_proof_statement () in s, gk
with NoCurrentProof -> s, default_gk)
@@ -4995,9 +5024,13 @@ let tclABSTRACT name_op tac =
let name, gk =
try let name, gk, _ = current_proof_statement () in name, gk
with NoCurrentProof -> anon_id, default_gk in
- add_suffix name "_subproof", gk
- in
- abstract_subproof s gk tac
+ add_suffix name suffix, gk
+
+let tclABSTRACT ?(opaque=true) name_op tac =
+ let s, gk = if opaque
+ then name_op_to_name name_op (Proof Theorem) "_subproof"
+ else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
+ abstract_subproof ~opaque s gk tac
let unify ?(state=full_transparent_state) x y =
Proofview.Goal.s_enter { s_enter = begin fun gl ->
@@ -5026,24 +5059,20 @@ module Simple = struct
let intro x = intro_move (Some x) MoveLast
let apply c =
- apply_with_bindings_gen false false [None,(Loc.ghost,(c,NoBindings))]
+ apply_with_bindings_gen false false [None,(Loc.tag (c,NoBindings))]
let eapply c =
- apply_with_bindings_gen false true [None,(Loc.ghost,(c,NoBindings))]
+ apply_with_bindings_gen false true [None,(Loc.tag (c,NoBindings))]
let elim c = elim false None (c,NoBindings) None
let case c = general_case_analysis false None (c,NoBindings)
let apply_in id c =
- apply_in false false id [None,(Loc.ghost, (c, NoBindings))] None
+ apply_in false false id [None,(Loc.tag (c, NoBindings))] None
end
(** Tacticals defined directly in term of Proofview *)
module New = struct
- open Proofview.Notations
-
- let exact_proof c = exact_proof c
-
open Genredexpr
open Locus
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index ba4a9706de..07a8035427 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -401,7 +401,9 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -
val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
-val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
+val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
+
+val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic
val specialize_eqs : Id.t -> unit Proofview.tactic
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 2c863c42a6..726fd23b64 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -49,7 +49,7 @@ struct
| DNil
(* debug *)
- let pr_dconstr f : 'a t -> std_ppcmds = function
+ let _pr_dconstr f : 'a t -> std_ppcmds = function
| DRel -> str "*"
| DSort -> str "Sort"
| DRef _ -> str "Ref"
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 04:43:58 +0000