aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml14
-rw-r--r--tactics/class_tactics.ml416
-rw-r--r--tactics/eqschemes.ml12
-rw-r--r--tactics/equality.ml32
-rw-r--r--tactics/hipattern.ml4
-rw-r--r--tactics/ind_tables.ml4
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/tactics.ml107
8 files changed, 41 insertions, 550 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 3eea1a74fd..0c0d9bcfc4 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -42,9 +42,9 @@ let compute_secvars gl =
open Unification
-let auto_core_unif_flags_of st1 st2 useeager = {
+let auto_core_unif_flags_of st1 st2 = {
modulo_conv_on_closed_terms = Some st1;
- use_metas_eagerly_in_conv_on_closed_terms = useeager;
+ use_metas_eagerly_in_conv_on_closed_terms = false;
use_evars_eagerly_in_conv_on_closed_terms = false;
modulo_delta = st2;
modulo_delta_types = full_transparent_state;
@@ -57,8 +57,8 @@ let auto_core_unif_flags_of st1 st2 useeager = {
modulo_eta = true;
}
-let auto_unif_flags_of st1 st2 useeager =
- let flags = auto_core_unif_flags_of st1 st2 useeager in {
+let auto_unif_flags_of st1 st2 =
+ let flags = auto_core_unif_flags_of st1 st2 in {
core_unify_flags = flags;
merge_unify_flags = flags;
subterm_unify_flags = { flags with modulo_delta = empty_transparent_state };
@@ -67,7 +67,7 @@ let auto_unif_flags_of st1 st2 useeager =
}
let auto_unif_flags =
- auto_unif_flags_of full_transparent_state empty_transparent_state false
+ auto_unif_flags_of full_transparent_state empty_transparent_state
(* Try unification with the precompiled clause, then use registered Apply *)
@@ -291,10 +291,10 @@ let tclTRY_dbg d tac =
de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
let flags_of_state st =
- auto_unif_flags_of st st false
+ auto_unif_flags_of st st
let auto_flags_of_state st =
- auto_unif_flags_of full_transparent_state st false
+ auto_unif_flags_of full_transparent_state st
let hintmap_of sigma secvars hdc concl =
match hdc with
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 4c91f3f61f..0260460e64 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -20,7 +20,6 @@ open Names
open Term
open Termops
open EConstr
-open Proof_type
open Tacmach
open Tactics
open Clenv
@@ -28,7 +27,6 @@ open Typeclasses
open Globnames
open Evd
open Locus
-open Misctypes
open Proofview.Notations
open Hints
@@ -41,10 +39,6 @@ module NamedDecl = Context.Named.Declaration
let typeclasses_debug = ref 0
let typeclasses_depth = ref None
-let typeclasses_modulo_eta = ref false
-let set_typeclasses_modulo_eta d = (:=) typeclasses_modulo_eta d
-let get_typeclasses_modulo_eta () = !typeclasses_modulo_eta
-
(** When this flag is enabled, the resolution of type classes tries to avoid
useless introductions. This is no longer useful since we have eta, but is
here for compatibility purposes. Another compatibility issues is that the
@@ -71,13 +65,6 @@ let set_typeclasses_filtered_unification d =
let get_typeclasses_filtered_unification () =
!typeclasses_filtered_unification
-(** [typeclasses_legacy_resolution] falls back to the 8.5 resolution algorithm,
- instead of the 8.6 one which uses the native backtracking facilities of the
- proof engine. *)
-let typeclasses_legacy_resolution = ref false
-let set_typeclasses_legacy_resolution d = (:=) typeclasses_legacy_resolution d
-let get_typeclasses_legacy_resolution () = !typeclasses_legacy_resolution
-
let set_typeclasses_debug d = (:=) typeclasses_debug (if d then 1 else 0)
let get_typeclasses_debug () = if !typeclasses_debug > 0 then true else false
@@ -94,14 +81,6 @@ open Goptions
let _ =
declare_bool_option
- { optdepr = true; (* remove in 8.8 *)
- optname = "do typeclass search modulo eta conversion";
- optkey = ["Typeclasses";"Modulo";"Eta"];
- optread = get_typeclasses_modulo_eta;
- optwrite = set_typeclasses_modulo_eta; }
-
-let _ =
- declare_bool_option
{ optdepr = false;
optname = "do typeclass search avoiding eta-expansions " ^
" in proof terms (expensive)";
@@ -127,14 +106,6 @@ let _ =
let _ =
declare_bool_option
- { optdepr = true; (* remove in 8.8 *)
- optname = "compat";
- optkey = ["Typeclasses";"Legacy";"Resolution"];
- optread = get_typeclasses_legacy_resolution;
- optwrite = set_typeclasses_legacy_resolution; }
-
-let _ =
- declare_bool_option
{ optdepr = false;
optname = "compat";
optkey = ["Typeclasses";"Filtered";"Unification"];
@@ -199,7 +170,7 @@ let auto_core_unif_flags st freeze = {
frozen_evars = freeze;
restrict_conv_on_strict_subterms = false; (* ? *)
modulo_betaiota = true;
- modulo_eta = !typeclasses_modulo_eta;
+ modulo_eta = false;
}
let auto_unif_flags freeze st =
@@ -426,9 +397,6 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
else
let tac =
with_prods nprods poly (term,cl) (unify_resolve poly flags) in
- if get_typeclasses_legacy_resolution () then
- Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
- else
Proofview.tclBIND (Proofview.with_shelf tac)
(fun (gls, ()) -> shelve_dependencies gls)
| ERes_pf (term,cl) ->
@@ -441,9 +409,6 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
else
let tac =
with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
- if get_typeclasses_legacy_resolution () then
- Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
- else
Proofview.tclBIND (Proofview.with_shelf tac)
(fun (gls, ()) -> shelve_dependencies gls)
| Give_exact (c,clenv) ->
@@ -618,359 +583,6 @@ let make_hints g st only_classes sign =
([]) sign
in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true)
-(** <= 8.5 resolution *)
-module V85 = struct
-
- type autoinfo = { hints : hint_db; is_evar: existential_key option;
- only_classes: bool; unique : bool;
- auto_depth: int list; auto_last_tac: Pp.t Lazy.t;
- auto_path : global_reference option list;
- auto_cut : hints_path }
- type autogoal = goal * autoinfo
- type failure = NotApplicable | ReachedLimit
- type 'ans fk = failure -> 'ans
- type ('a,'ans) sk = 'a -> 'ans fk -> 'ans
- type 'a tac = { skft : 'ans. ('a,'ans) sk -> 'ans fk -> autogoal sigma -> 'ans }
-
- type auto_result = autogoal list sigma
-
- type atac = auto_result tac
-
- (* Some utility types to avoid the need of -rectypes *)
-
- type 'a optionk =
- | Nonek
- | Somek of 'a * 'a optionk fk
-
- type ('a,'b) optionk2 =
- | Nonek2 of failure
- | Somek2 of 'a * 'b * ('a,'b) optionk2 fk
-
- let pf_filtered_hyps gls =
- Goal.V82.hyps gls.Evd.sigma (sig_it gls)
-
- let make_autogoal_hints =
- let cache = Summary.ref ~name:"make_autogoal_hints_cache"
- (true, Environ.empty_named_context_val,
- Hint_db.empty full_transparent_state true)
- in
- fun only_classes ?(st=full_transparent_state) g ->
- let sign = pf_filtered_hyps g in
- let (onlyc, sign', cached_hints) = !cache in
- if onlyc == only_classes &&
- (sign == sign' || Environ.eq_named_context_val sign sign')
- && Hint_db.transparent_state cached_hints == st
- then
- cached_hints
- else
- let hints = make_hints g st only_classes (EConstr.named_context_of_val sign)
- in
- cache := (only_classes, sign, hints); hints
-
- let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac =
- { skft = fun sk fk {it = gl,hints; sigma=s;} ->
- let res = try Some (tac {it=gl; sigma=s;})
- with e when catchable e -> None in
- match res with
- | Some gls -> sk (f gls hints) fk
- | None -> fk NotApplicable }
-
- let intro_tac : atac =
- let tac {it = gls; sigma = s} info =
- let gls' =
- List.map (fun g' ->
- let env = Goal.V82.env s g' in
- let context = EConstr.named_context_of_val (Goal.V82.hyps s g') in
- let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints)
- (true,false,false) info.only_classes empty_hint_info (List.hd context) in
- let ldb = Hint_db.add_list env s hint info.hints in
- (g', { info with is_evar = None; hints = ldb;
- auto_last_tac = lazy (str"intro") })) gls
- in {it = gls'; sigma = s;}
- in
- lift_tactic (Proofview.V82.of_tactic Tactics.intro) tac
-
- let normevars_tac : atac =
- { skft = fun sk fk {it = (gl, info); sigma = s;} ->
- let gl', sigma' = Goal.V82.nf_evar s gl in
- let info' = { info with auto_last_tac = lazy (str"normevars") } in
- sk {it = [gl', info']; sigma = sigma';} fk }
-
- let merge_failures x y =
- match x, y with
- | _, ReachedLimit
- | ReachedLimit, _ -> ReachedLimit
- | NotApplicable, NotApplicable -> NotApplicable
-
- let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
- { skft = fun sk fk gls -> x.skft sk
- (fun f -> y.skft sk (fun f' -> fk (merge_failures f f')) gls) gls }
-
- let or_else_tac (x : 'a tac) (y : failure -> 'a tac) : 'a tac =
- { skft = fun sk fk gls -> x.skft sk
- (fun f -> (y f).skft sk fk gls) gls }
-
- let needs_backtrack env evd oev concl =
- if Option.is_empty oev || is_Prop env evd concl then
- occur_existential evd concl
- else true
-
- let hints_tac hints sk fk {it = gl,info; sigma = s} =
- let env = Goal.V82.env s gl in
- let concl = Goal.V82.concl s gl in
- let tacgl = {it = gl; sigma = s;} in
- let secvars = secvars_of_hyps (Environ.named_context_of_val (Goal.V82.hyps s gl)) in
- let poss = e_possible_resolve hints info.hints secvars info.only_classes env s concl in
- let unique = is_unique env s concl in
- let rec aux i foundone = function
- | (tac, _, extern, name, pp) :: tl ->
- let derivs = path_derivate info.auto_cut name in
- let res =
- try
- if path_matches derivs [] then None
- else Some (Proofview.V82.of_tactic tac tacgl)
- with e when catchable e -> None
- in
- (match res with
- | None -> aux i foundone tl
- | Some {it = gls; sigma = s';} ->
- if !typeclasses_debug > 0 then
- Feedback.msg_debug
- (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
- ++ str" on" ++ spc () ++ pr_ev s gl);
- let sgls =
- evars_to_goals
- (fun evm ev evi ->
- if Typeclasses.is_resolvable evi && not (Evd.is_undefined s ev) &&
- (not info.only_classes || Typeclasses.is_class_evar evm evi)
- then Typeclasses.mark_unresolvable evi, true
- else evi, false) s'
- in
- let newgls, s' =
- let gls' = List.map (fun g -> (None, g)) gls in
- match sgls with
- | None -> gls', s'
- | Some (evgls, s') ->
- if not !typeclasses_dependency_order then
- (gls' @ List.map (fun (ev,_) -> (Some ev, ev)) (Evar.Map.bindings evgls), s')
- else
- (* Reorder with dependent subgoals. *)
- let evm = List.fold_left
- (fun acc g -> Evar.Map.add g (Evd.find_undefined s' g) acc) evgls gls in
- let gls = top_sort s' evm in
- (List.map (fun ev -> Some ev, ev) gls, s')
- in
- let reindex g =
- let open Goal.V82 in
- extern && not (Environ.eq_named_context_val
- (hyps s' g) (hyps s' gl))
- in
- let gl' j (evar, g) =
- let hints' =
- if reindex g then
- make_autogoal_hints
- info.only_classes
- ~st:(Hint_db.transparent_state info.hints)
- {it = g; sigma = s';}
- else info.hints
- in
- { info with
- auto_depth = j :: i :: info.auto_depth;
- auto_last_tac = pp;
- is_evar = evar;
- hints = hints';
- auto_cut = derivs }
- in
- let gls' = List.map_i (fun i g -> snd g, gl' i g) 1 newgls in
- let glsv = {it = gls'; sigma = s';} in
- let fk' =
- (fun e ->
- let do_backtrack =
- if unique then occur_existential tacgl.sigma concl
- else if info.unique then true
- else if List.is_empty gls' then
- needs_backtrack env tacgl.sigma info.is_evar concl
- else true
- in
- let e' = match foundone with None -> e
- | Some e' -> merge_failures e e' in
- if !typeclasses_debug > 0 then
- Feedback.msg_debug
- ((if do_backtrack then str"Backtracking after "
- else str "Not backtracking after ")
- ++ Lazy.force pp);
- if do_backtrack then aux (succ i) (Some e') tl
- else fk e')
- in
- sk glsv fk')
- | [] ->
- if foundone == None && !typeclasses_debug > 0 then
- Feedback.msg_debug
- (pr_depth info.auto_depth ++ str": no match for " ++
- Printer.pr_econstr_env (Goal.V82.env s gl) s concl ++
- spc () ++ str ", " ++ int (List.length poss) ++
- str" possibilities");
- match foundone with
- | Some e -> fk e
- | None -> fk NotApplicable
- in aux 1 None poss
-
- let hints_tac hints =
- { skft = fun sk fk gls -> hints_tac hints sk fk gls }
-
- let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
- let rec aux s (acc : autogoal list list) fk = function
- | (gl,info) :: gls ->
- Control.check_for_interrupt ();
- (match info.is_evar with
- | Some ev when Evd.is_defined s ev -> aux s acc fk gls
- | _ ->
- second.skft
- (fun {it=gls';sigma=s'} fk' ->
- let fk'' =
- if not info.unique && List.is_empty gls' &&
- not (needs_backtrack (Goal.V82.env s gl) s
- info.is_evar (Goal.V82.concl s gl))
- then fk
- else fk'
- in
- aux s' (gls'::acc) fk'' gls)
- fk {it = (gl,info); sigma = s; })
- | [] -> Somek2 (List.rev acc, s, fk)
- in fun {it = gls; sigma = s; } fk ->
- let rec aux' = function
- | Nonek2 e -> fk e
- | Somek2 (res, s', fk') ->
- let goals' = List.concat res in
- sk {it = goals'; sigma = s'; } (fun e -> aux' (fk' e))
- in aux' (aux s [] (fun e -> Nonek2 e) gls)
-
- let then_tac (first : atac) (second : atac) : atac =
- { skft = fun sk fk -> first.skft (then_list second sk) fk }
-
- let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option =
- t.skft (fun x _ -> Some x) (fun _ -> None) gl
-
- type run_list_res = auto_result optionk
-
- let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res =
- (then_list t (fun x fk -> Somek (x, fk)))
- gl
- (fun _ -> Nonek)
-
- let fail_tac reason : atac =
- { skft = fun sk fk _ -> fk reason }
-
- let rec fix (t : 'a tac) : 'a tac =
- then_tac t { skft = fun sk fk -> (fix t).skft sk fk }
-
- let rec fix_limit limit (t : 'a tac) : 'a tac =
- if Int.equal limit 0 then fail_tac ReachedLimit
- else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk }
-
- let fix_iterative t =
- let rec aux depth =
- or_else_tac (fix_limit depth t)
- (function
- | NotApplicable as e -> fail_tac e
- | ReachedLimit -> aux (succ depth))
- in aux 1
-
- let fix_iterative_limit limit (t : 'a tac) : 'a tac =
- let rec aux depth =
- if Int.equal limit depth then fail_tac ReachedLimit
- else or_tac (fix_limit depth t)
- { skft = fun sk fk -> (aux (succ depth)).skft sk fk }
- in aux 1
-
- let make_autogoal ?(only_classes=true) ?(unique=false) ?(st=full_transparent_state)
- cut ev g =
- let hints = make_autogoal_hints only_classes ~st g in
- (g.it, { hints = hints ; is_evar = ev; unique = unique;
- only_classes = only_classes; auto_depth = [];
- auto_last_tac = lazy (str"none");
- auto_path = []; auto_cut = cut })
-
-
- let make_autogoals ?(only_classes=true) ?(unique=false)
- ?(st=full_transparent_state) hints gs evm' =
- let cut = cut_of_hints hints in
- let gl i g =
- let (gl, auto) = make_autogoal ~only_classes ~unique
- ~st cut (Some g) {it = g; sigma = evm'; } in
- (gl, { auto with auto_depth = [i]})
- in { it = List.map_i gl 1 gs; sigma = evm' }
-
- let get_result r =
- match r with
- | Nonek -> None
- | Somek (gls, fk) -> Some (gls.sigma,fk)
-
- let run_on_evars ?(only_classes=true) ?(unique=false) ?(st=full_transparent_state)
- p evm hints tac =
- match evars_to_goals p evm with
- | None -> None (* This happens only because there's no evar having p *)
- | Some (goals, evm') ->
- let goals =
- if !typeclasses_dependency_order then
- top_sort evm' goals
- else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals)
- in
- let res = run_list_tac tac p goals
- (make_autogoals ~only_classes ~unique ~st hints goals evm') in
- match get_result res with
- | None -> raise Not_found
- | Some (evm', fk) ->
- Some (evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm, fk)
-
- let eauto_tac hints =
- then_tac normevars_tac (or_tac (hints_tac hints) intro_tac)
-
- let eauto_tac strategy depth hints =
- match strategy with
- | Bfs ->
- begin match depth with
- | None -> fix_iterative (eauto_tac hints)
- | Some depth -> fix_iterative_limit depth (eauto_tac hints) end
- | Dfs ->
- match depth with
- | None -> fix (eauto_tac hints)
- | Some depth -> fix_limit depth (eauto_tac hints)
-
- let real_eauto ?depth strategy unique st hints p evd =
- let res =
- run_on_evars ~st ~unique p evd hints (eauto_tac strategy depth hints)
- in
- match res with
- | None -> evd
- | Some (evd', fk) ->
- if unique then
- (match get_result (fk NotApplicable) with
- | Some (evd'', fk') -> user_err Pp.(str "Typeclass resolution gives multiple solutions")
- | None -> evd')
- else evd'
-
- let resolve_all_evars_once debug depth unique p evd =
- let db = searchtable_map typeclasses_db in
- let strategy = if get_typeclasses_iterative_deepening () then Bfs else Dfs in
- real_eauto ?depth strategy unique (Hint_db.transparent_state db) [db] p evd
-
- let eauto85 ?(only_classes=true) ?st ?strategy depth hints g =
- let strategy =
- match strategy with
- | None -> if get_typeclasses_iterative_deepening () then Bfs else Dfs
- | Some s -> s
- in
- let gl = { it = make_autogoal ~only_classes ?st
- (cut_of_hints hints) None g; sigma = project g; } in
- match run_tac (eauto_tac strategy depth hints) gl with
- | None -> raise Not_found
- | Some {it = goals; sigma = s; } ->
- {it = List.map fst goals; sigma = s;}
-
-end
-
-(** 8.6 resolution *)
module Search = struct
type autoinfo =
{ search_depth : int list;
@@ -1354,14 +966,15 @@ module Search = struct
top_sort evm' goals
else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals)
in
- let fgoals = Evd.future_goals evm in
- let pgoal = Evd.principal_future_goal evm in
+ let fgoals = Evd.save_future_goals evm in
let _, pv = Proofview.init evm' [] in
let pv = Proofview.unshelve goals pv in
try
let (), pv', (unsafe, shelved, gaveup), _ =
Proofview.apply env tac pv
in
+ if not (List.is_empty gaveup) then
+ CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals.");
if Proofview.finished pv' then
let evm' = Proofview.return pv' in
assert(Evd.fold_undefined (fun ev _ acc ->
@@ -1371,7 +984,8 @@ module Search = struct
(str "leaking evar " ++ int (Evar.repr ev) ++
spc () ++ pr_ev evm' ev);
acc && okev) evm' true);
- let evm' = Evd.restore_future_goals evm' (shelved @ fgoals) pgoal in
+ let fgoals = Evd.shelve_on_future_goals shelved fgoals in
+ let evm' = Evd.restore_future_goals evm' fgoals in
let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in
Some evm'
else raise Not_found
@@ -1406,13 +1020,7 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
in
let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in
- if get_typeclasses_legacy_resolution () then
- Proofview.V82.tactic
- (fun gl ->
- try V85.eauto85 depth ~only_classes ~st ?strategy dbs gl
- with Not_found ->
- Refiner.tclFAIL 0 (str"Proof search failed") gl)
- else Search.eauto_tac ~st ~only_classes ?strategy ~depth ~dep:true dbs
+ Search.eauto_tac ~st ~only_classes ?strategy ~depth ~dep:true dbs
(** We compute dependencies via a union-find algorithm.
Beware of the imperative effects on the partition structure,
@@ -1531,12 +1139,7 @@ let resolve_all_evars debug depth unique env p oevd do_split fail =
| comp :: comps ->
let p = select_and_update_evars p oevd (in_comp comp) in
try
- let evd' =
- if get_typeclasses_legacy_resolution () then
- V85.resolve_all_evars_once debug depth unique p evd
- else
- Search.typeclasses_resolve env evd debug depth unique p
- in
+ let evd' = Search.typeclasses_resolve env evd debug depth unique p in
if has_undefined p oevd evd' then raise Unresolved;
docomp evd' comps
with Unresolved | Not_found ->
@@ -1581,9 +1184,6 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
let st = Hint_db.transparent_state hints in
let depth = get_typeclasses_depth () in
let gls' =
- if get_typeclasses_legacy_resolution () then
- V85.eauto85 depth ~st [hints] gls
- else
try
Proofview.V82.of_tactic
(Search.eauto_tac ~st ~only_classes:true ~depth [hints] ~dep:true) gls
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 45926551b4..477de6452e 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -214,7 +214,7 @@ let build_sym_scheme env ind =
rel_vect (2*nrealargs+2) nrealargs])),
mkRel 1 (* varH *),
[|cstr (nrealargs+1)|]))))
- in c, Evd.evar_universe_context_of ctx
+ in c, UState.of_context_set ctx
let sym_scheme_kind =
declare_individual_scheme_object "_sym_internal"
@@ -285,7 +285,7 @@ let build_sym_involutive_scheme env ind =
mkRel 1|])),
mkRel 1 (* varH *),
[|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
- in (c, Evd.evar_universe_context_of ctx), eff
+ in (c, UState.of_context_set ctx), eff
let sym_involutive_scheme_kind =
declare_individual_scheme_object "_sym_involutive"
@@ -439,7 +439,7 @@ let build_l2r_rew_scheme dep env ind kind =
[|main_body|])
else
main_body))))))
- in (c, Evd.evar_universe_context_of ctx),
+ in (c, UState.of_context_set ctx),
Safe_typing.concat_private eff' eff
(**********************************************************************)
@@ -528,7 +528,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
(if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s)
(mkNamedLambda varHC applied_PC'
(mkVar varHC))|])))))
- in c, Evd.evar_universe_context_of ctx
+ in c, UState.of_context_set ctx
(**********************************************************************)
(* Build the right-to-left rewriting lemma for hypotheses associated *)
@@ -601,7 +601,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
lift (nrealargs+3) applied_PC,
mkRel 1)|]),
[|mkVar varHC|]))))))
- in c, Evd.evar_universe_context_of ctx
+ in c, UState.of_context_set ctx
(**********************************************************************)
(* This function "repairs" the non-dependent r2l forward rewriting *)
@@ -808,7 +808,7 @@ let build_congr env (eq,refl,ctx) ind =
[|mkApp (refl,
[|mkVar varB;
mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|]))))))
- in c, Evd.evar_universe_context_of ctx
+ in c, UState.of_context_set ctx
let congr_scheme_kind = declare_individual_scheme_object "_congr"
(fun _ ind ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f15a64fc8e..98f627f211 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -56,33 +56,12 @@ type inj_flags = {
injection_pattern_l2r_order : bool;
}
-let discriminate_introduction = ref true
-
-let discr_do_intro () = !discriminate_introduction
-
open Goptions
-let _ =
- declare_bool_option
- { optdepr = true; (* remove in 8.8 *)
- optname = "automatic introduction of hypotheses by discriminate";
- optkey = ["Discriminate";"Introduction"];
- optread = (fun () -> !discriminate_introduction);
- optwrite = (:=) discriminate_introduction }
-
-let injection_pattern_l2r_order = ref true
let use_injection_pattern_l2r_order = function
- | None -> !injection_pattern_l2r_order
+ | None -> true
| Some flags -> flags.injection_pattern_l2r_order
-let _ =
- declare_bool_option
- { optdepr = true; (* remove in 8.8 *)
- 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) ;
- optwrite = (fun b -> injection_pattern_l2r_order := b) }
-
let injection_in_context = ref false
let use_injection_in_context = function
@@ -1090,13 +1069,10 @@ let discrClause with_evars = onClause (discrSimpleClause with_evars)
let discrEverywhere with_evars =
tclTHEN (Proofview.tclUNIT ())
(* Delay the interpretation of side-effect *)
- (if discr_do_intro () then
- (tclTHEN
- (tclREPEAT introf)
- (tryAllHyps
+ (tclTHEN
+ (tclREPEAT introf)
+ (tryAllHyps
(fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
- else (* <= 8.2 compat *)
- tryAllHypsAndConcl (discrSimpleClause with_evars))
let discr_tac with_evars = function
| None -> discrEverywhere with_evars
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index a59046a678..b012a7ecd1 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -511,10 +511,10 @@ let coq_eqdec ~sum ~rev =
mkPattern (mkGAppRef sum args)
)
-(** { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } *)
+(** [{ ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 }] *)
let coq_eqdec_inf_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:false
-(** { ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 } *)
+(** [{ ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 }] *)
let coq_eqdec_inf_rev_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:true
(** %coq_or_ref (?X2 = ?X3 :> ?X1) (~ ?X2 = ?X3 :> ?X1) *)
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index b960a845ce..62ead57f38 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -122,8 +122,8 @@ let compute_name internal id =
let define internal id c p univs =
let fd = declare_constant ~internal in
let id = compute_name internal id in
- let ctx = Evd.normalize_evar_universe_context univs in
- let c = Universes.subst_opt_univs_constr (Evd.evar_universe_context_subst ctx) c in
+ let ctx = UState.minimize univs in
+ let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in
let univs =
if p then Polymorphic_const_entry (UState.context ctx)
else Monomorphic_const_entry (UState.context_set ctx)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 655283c204..a4cdc1592a 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -218,7 +218,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
end in
let avoid = ref Id.Set.empty in
let _,_,_,_,sigma = Proof.proof pf in
- let sigma = Evd.nf_constraints sigma in
+ let sigma = Evd.minimize_universes sigma in
let rec fill_holes c =
match EConstr.kind sigma c with
| Evar (e,args) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 20519dd986..12aef852d0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -15,7 +15,6 @@ open CErrors
open Util
open Names
open Nameops
-open Term
open Constr
open Termops
open Environ
@@ -61,16 +60,6 @@ let typ_of env sigma c =
open Goptions
-let apply_solve_class_goals = ref false
-
-let _ =
- declare_bool_option
- { optdepr = true; (* remove in 8.8 *)
- optname = "Perform typeclass resolution on apply-generated subgoals.";
- optkey = ["Typeclass";"Resolution";"After";"Apply"];
- optread = (fun () -> !apply_solve_class_goals);
- optwrite = (fun a -> apply_solve_class_goals := a); }
-
let clear_hyp_by_default = ref false
let use_clear_hyp_by_default () = !clear_hyp_by_default
@@ -99,18 +88,6 @@ let _ =
optread = (fun () -> !universal_lemma_under_conjunctions) ;
optwrite = (fun b -> universal_lemma_under_conjunctions := b) }
-(* Shrinking of abstract proofs. *)
-
-let shrink_abstract = ref true
-
-let _ =
- declare_bool_option
- { optdepr = true; (* remove in 8.8 *)
- optname = "shrinking of abstracted proofs";
- optkey = ["Shrink"; "Abstract"];
- optread = (fun () -> !shrink_abstract) ;
- optwrite = (fun b -> shrink_abstract := b) }
-
(* The following boolean governs what "intros []" do on examples such
as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]";
if false, it behaves as "intro H; case H; clear H" for fresh H.
@@ -410,12 +387,11 @@ let find_name mayrepl decl naming gl = match naming with
new_fresh_id idl (default_id env sigma decl) gl
| NamingBasedOn (id,idl) -> new_fresh_id idl id gl
| NamingMustBe (loc,id) ->
- (* When name is given, we allow to hide a global name *)
- let ids_of_hyps = Tacmach.New.pf_ids_set_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 (Id.print id ++ str" is already used.");
- id
+ (* When name is given, we allow to hide a global name *)
+ let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in
+ if not mayrepl && Id.Set.mem id ids_of_hyps then
+ user_err ?loc (Id.print id ++ str" is already used.");
+ id
(**************************************************************)
(* Computing position of hypotheses for replacing *)
@@ -1349,46 +1325,6 @@ let index_of_ind_arg sigma t =
| None -> error "Could not find inductive argument of elimination scheme."
in aux None 0 t
-let enforce_prop_bound_names rename tac =
- let open Context.Rel.Declaration in
- match rename with
- | Some (isrec,nn) when Namegen.use_h_based_elimination_names () ->
- (* Rename dependent arguments in Prop with name "H" *)
- (* so as to avoid having hypothesis such as "t:True", "n:~A" when calling *)
- (* elim or induction with schemes built by Indrec.build_induction_scheme *)
- let rec aux env sigma i t =
- if i = 0 then t else match EConstr.kind sigma t with
- | Prod (Name _ as na,t,t') ->
- let very_standard = true in
- let na =
- if Retyping.get_sort_family_of env sigma t = InProp then
- (* "very_standard" says that we should have "H" names only, but
- this would break compatibility even more... *)
- let s = match Namegen.head_name sigma t with
- | Some id when not very_standard -> Id.to_string id
- | _ -> "" in
- Name (add_suffix Namegen.default_prop_ident s)
- else
- na in
- mkProd (na,t,aux (push_rel (LocalAssum (na,t)) env) sigma (i-1) t')
- | Prod (Anonymous,t,t') ->
- mkProd (Anonymous,t,aux (push_rel (LocalAssum (Anonymous,t)) env) sigma (i-1) t')
- | LetIn (na,c,t,t') ->
- mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t')
- | _ -> assert false in
- let rename_branch i =
- Proofview.Goal.enter begin fun gl ->
- let env = Proofview.Goal.env gl in
- let sigma = Tacmach.New.project gl in
- let t = Proofview.Goal.concl gl in
- change_concl (aux env sigma i t)
- end in
- (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
- tac
- (Array.map rename_branch nn)
- | _ ->
- tac
-
let rec contract_letin_in_lam_header sigma c =
match EConstr.kind sigma c with
| Lambda (x,t,c) -> mkLambda (x,t,contract_letin_in_lam_header sigma c)
@@ -1409,7 +1345,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
(str "The type of elimination clause is not well-formed."))
in
let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
- enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags)
+ Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags
end
(*
@@ -1689,22 +1625,6 @@ let descend_in_conjunctions avoid tac (err, info) c =
(* Resolution tactics *)
(****************************************************)
-let solve_remaining_apply_goals =
- Proofview.Goal.enter begin fun gl ->
- let evd = Proofview.Goal.sigma gl in
- if !apply_solve_class_goals then
- try
- let env = Proofview.Goal.env gl in
- let concl = Proofview.Goal.concl gl in
- if Typeclasses.is_class_type evd concl then
- let evd', c' = Typeclasses.resolve_one_typeclass env evd concl in
- Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd')
- (Refine.refine ~typecheck:false (fun h -> (h,c')))
- else Proofview.tclUNIT ()
- with Not_found -> Proofview.tclUNIT ()
- else Proofview.tclUNIT ()
- end
-
let tclORELSEOPT t k =
Proofview.tclORELSE t
(fun e -> match k e with
@@ -1780,11 +1700,9 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind :
| _ -> None)
end
in
- Tacticals.New.tclTHENLIST [
- try_main_apply with_destruct c;
- solve_remaining_apply_goals;
- apply_clear_request clear_flag (use_clear_hyp_by_default ()) c
- ]
+ Tacticals.New.tclTHEN
+ (try_main_apply with_destruct c)
+ (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
end
let rec apply_with_bindings_gen b e = function
@@ -4249,7 +4167,7 @@ let induction_tac with_evars params indvars elim =
let elimclause' = recolle_clenv i params indvars elimclause gl in
(* one last resolution (useless?) *)
let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
- enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved)
+ Clenvtac.clenv_refine with_evars resolved
end
(* Apply induction "in place" taking into account dependent
@@ -5014,10 +4932,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
let (_, info) = CErrors.push src in
iraise (e, info)
in
- let const, args =
- if !shrink_abstract then shrink_entry sign const
- else (const, List.rev (Context.Named.to_instance Constr.mkVar sign))
- in
+ let const, args = shrink_entry sign const in
let args = List.map EConstr.of_constr args 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 04:10:07 +0000