diff options
26 files changed, 53 insertions, 627 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 6e76d04e7..da798a238 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -492,26 +492,6 @@ control on the triggering of instances. For example, forcing a constant to explicitely appear in the pattern will make it never apply on a goal where there is a hole in that place. -\subsection{\tt Set Typeclasses Legacy Resolution} -\optindex{Typeclasses Legacy Resolution} -\emph{Deprecated since 8.7} - -This option (off by default) uses the 8.5 implementation of resolution. -Use for compatibility purposes only (porting and debugging). - -\subsection{\tt Set Typeclasses Module Eta} -\optindex{Typeclasses Modulo Eta} -\emph{Deprecated since 8.7} - -This option allows eta-conversion for functions and records during -unification of type-classes. This option is unsupported since 8.6 with -{\tt Typeclasses Filtered Unification} set, but still affects the -default unification strategy, and the one used in {\tt Legacy - Resolution} mode. It is \emph{unset} by default. If {\tt Typeclasses - Filtered Unification} is set, this has no effect and unification will -find solutions up-to eta conversion. Note however that syntactic -pattern-matching is not up-to eta. - \subsection{\tt Set Typeclasses Limit Intros} \optindex{Typeclasses Limit Intros} @@ -525,13 +505,6 @@ invertibility status of the product introduction rule, resulting in potentially more expensive proof-search (i.e. more useless backtracking). -\subsection{\tt Set Typeclass Resolution After Apply} -\optindex{Typeclass Resolution After Apply} -\emph{Deprecated since 8.6} - -This option (off by default in Coq 8.6 and 8.5) controls the resolution -of typeclass subgoals generated by the {\tt apply} tactic. - \subsection{\tt Set Typeclass Resolution For Conversion} \optindex{Typeclass Resolution For Conversion} diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 30724759d..600471123 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -127,7 +127,6 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}. \optindex{Boolean Equality Schemes} \optindex{Elimination Schemes} \optindex{Nonrecursive Elimination Schemes} -\optindex{Record Elimination Schemes} \optindex{Case Analysis Schemes} \optindex{Decidable Equality Schemes} \optindex{Rewriting Schemes} @@ -144,7 +143,6 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic declaration of the induction principles. It can be activated with the command {\tt Set Nonrecursive Elimination Schemes}. It can be deactivated again with {\tt Unset Nonrecursive Elimination Schemes}. -{\tt Record Elimination Schemes} is a deprecated alias of {\tt Nonrecursive Elimination Schemes}. In addition, the {\tt Case Analysis Schemes} flag governs the generation of case analysis lemmas for inductive types, i.e. corresponding to the diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 6dca314b4..40ba43b6c 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -4589,7 +4589,6 @@ incompatibilities. \end{Variants} \optindex{Intuition Negation Unfolding} -\optindex{Intuition Iff Unfolding} Some aspects of the tactic {\tt intuition} can be controlled using options. To avoid that inner negations which do not @@ -4609,17 +4608,6 @@ To do that all negations of the goal are unfolded even inner ones To avoid that inner occurrence of {\tt iff} which do not need to be unfolded are unfolded (this is the default), use: -\begin{quote} -{\tt Unset Intuition Iff Unfolding} -\end{quote} - -To do that all negations of the goal are unfolded even inner ones -(this is the default), use: - -\begin{quote} -{\tt Set Intuition Iff Unfolding} -\end{quote} - % En attente d'un moyen de valoriser les fichiers de demos %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v} diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index d0f31cd42..a51c09ca4 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -65,11 +65,6 @@ let assoc_flags ist : tauto_flags = (* Whether inner not are unfolded *) let negation_unfolding = ref true -(* Whether inner iff are unfolded *) -let iff_unfolding = ref false - -let unfold_iff () = !iff_unfolding - open Goptions let _ = declare_bool_option @@ -79,14 +74,6 @@ let _ = optread = (fun () -> !negation_unfolding); optwrite = (:=) negation_unfolding } -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "unfolding of iff in intuition"; - optkey = ["Intuition";"Iff";"Unfolding"]; - optread = (fun () -> !iff_unfolding); - optwrite = (:=) iff_unfolding } - (** Base tactics *) let idtac = Proofview.tclUNIT () @@ -202,16 +189,13 @@ let make_unfold name = let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in (Locus.AllOccurrences, ArgArg (EvalConstRef const, None)) -let u_iff = make_unfold "iff" let u_not = make_unfold "not" let reduction_not_iff _ ist = let make_reduce c = TacAtom (Loc.tag @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in - let tac = match !negation_unfolding, unfold_iff () with - | true, true -> make_reduce [u_not; u_iff] - | true, false -> make_reduce [u_not] - | false, true -> make_reduce [u_iff] - | false, false -> TacId [] + let tac = match !negation_unfolding with + | true -> make_reduce [u_not] + | false -> TacId [] in eval_tactic_ist ist tac diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 9783bc61d..7f5f2f63d 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -138,7 +138,7 @@ type ssrclseq = InGoal | InHyps type 'tac ssrhint = bool * 'tac option list type 'tac fwdbinders = - bool * (ssrhpats * ((ssrfwdfmt * ssrterm) * 'tac ssrhint)) + bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)) type clause = (ssrclear * ((ssrhyp_or_id * string) * @@ -157,13 +157,15 @@ type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option) open Ssrmatching_plugin open Ssrmatching + +type 'a ssrcasearg = ssripat option * ('a * ssripats) +type 'a ssrmovearg = ssrview * 'a ssrcasearg + type ssrdgens = { dgens : (ssrdocc * cpattern) list; gens : (ssrdocc * cpattern) list; clr : ssrclear } -type ssrcasearg = ssripat option * (ssrdgens * ssripats) -type ssrmovearg = ssrview * ssrcasearg -type ssragens = ((ssrhyps option * occ) * ssrterm) list list * ssrclear -type ssrapplyarg = ssrterm list * (ssragens * ssripats) +type 'a ssragens = (ssrdocc * 'a) list list * ssrclear +type ssrapplyarg = ssrterm list * (ssrterm ssragens * ssripats) (* OOP : these are general shortcuts *) type gist = Tacintern.glob_sign diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli index 6243e5e68..694ecfa37 100644 --- a/plugins/ssr/ssrbwd.mli +++ b/plugins/ssr/ssrbwd.mli @@ -13,4 +13,4 @@ open Proofview val apply_top_tac : unit tactic -val inner_ssrapplytac : ssrterm list -> ssragens -> ist -> unit tactic +val inner_ssrapplytac : ssrterm list -> ssrterm ssragens -> ist -> unit tactic diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 71cde0ca1..00c971237 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -143,18 +143,6 @@ let newssrcongrtac arg ist gl = (** 7. Rewriting tactics (rewrite, unlock) *) -(** Coq rewrite compatibility flag *) - - -let _ = - let ssr_strict_match = ref false in - Goptions.declare_bool_option - { Goptions.optname = "strict redex matching"; - Goptions.optkey = ["Match"; "Strict"]; - Goptions.optread = (fun () -> !ssr_strict_match); - Goptions.optdepr = true; (* noop *) - Goptions.optwrite = (fun b -> ssr_strict_match := b) } - (** Rewrite rules *) type ssrwkind = RWred of ssrsimpl | RWdef | RWeq diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli index b8716c0c4..89cba4be7 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -29,11 +29,11 @@ val tclIPATssr : ssripats -> unit Proofview.tactic [tac E: gens => ipats] where [E] is injected into [ipats] (at the right place) and [gens] are generalized before calling [tac] *) -val ssrmovetac : ssrmovearg -> unit Proofview.tactic +val ssrmovetac : ssrdgens ssrmovearg -> unit Proofview.tactic val ssrsmovetac : unit Proofview.tactic -val ssrelimtac : ssrmovearg -> unit Proofview.tactic +val ssrelimtac : ssrdgens ssrmovearg -> unit Proofview.tactic val ssrselimtoptac : unit Proofview.tactic -val ssrcasetac : ssrmovearg -> unit Proofview.tactic +val ssrcasetac : ssrdgens ssrmovearg -> unit Proofview.tactic val ssrscasetoptac : unit Proofview.tactic (* The implementation of abstract: is half here, for the [[: var ]] diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index a52248614..130550388 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -20,3 +20,16 @@ val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c -> val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type +(* Parsing witnesses, needed to serialize ssreflect syntax *) +open Ssrmatching_plugin +open Ssrmatching +open Ssrast +open Ssrequality + +val wit_ssrrwargs : ssrrwarg list Genarg.uniform_genarg_type +val wit_ssrclauses : clauses Genarg.uniform_genarg_type +val wit_ssrcasearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type +val wit_ssrmovearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type +val wit_ssrapplyarg : ssrapplyarg Genarg.uniform_genarg_type +val wit_ssrhavefwdwbinders : + (Tacexpr.raw_tactic_expr fwdbinders, Tacexpr.glob_tactic_expr fwdbinders, Tacinterp.Value.t fwdbinders) Genarg.genarg_type diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5bc93f1fa..f4269a2c5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -250,20 +250,6 @@ let unify_r2l x = x let sort_eqns = unify_r2l *) -let global_pattern_unification_flag = ref true - -open Goptions - -(* Compatibility option introduced and activated in Coq 8.4 *) - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "pattern-unification for existential variables in tactics"; - optkey = ["Tactic";"Pattern";"Unification"]; - optread = (fun () -> !global_pattern_unification_flag); - optwrite = (:=) global_pattern_unification_flag } - type core_unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; (* What this flag controls was activated with all constants transparent, *) @@ -287,12 +273,10 @@ type core_unify_flags = { use_pattern_unification : bool; (* This solves pattern "?n x1 ... xn = t" when the xi are distinct rels *) - (* This says if pattern unification is tried; can be overwritten with *) - (* option "Set Tactic Pattern Unification" *) + (* This says if pattern unification is tried *) use_meta_bound_pattern_unification : bool; - (* This is implied by use_pattern_unification (though deactivated *) - (* by unsetting Tactic Pattern Unification); has no particular *) + (* This is implied by use_pattern_unification; has no particular *) (* reasons to be set differently than use_pattern_unification *) (* except for compatibility of "auto". *) (* This was on for all tactics, including auto, since Sep 2006 for 8.1 *) @@ -473,10 +457,10 @@ let set_flags_for_type flags = { flags with } let use_evars_pattern_unification flags = - !global_pattern_unification_flag && flags.use_pattern_unification + flags.use_pattern_unification let use_metas_pattern_unification sigma flags nb l = - !global_pattern_unification_flag && flags.use_pattern_unification + flags.use_pattern_unification || flags.use_meta_bound_pattern_unification && Array.for_all (fun c -> isRel sigma c && destRel sigma c <= nb) l diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 4c91f3f61..9f6624889 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; @@ -1406,13 +1018,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 +1137,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 +1182,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/equality.ml b/tactics/equality.ml index f15a64fc8..236db1dcc 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -69,20 +69,10 @@ let _ = 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 diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 20519dd98..b99a45103 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -61,16 +61,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 @@ -1689,22 +1679,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 +1754,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 diff --git a/test-suite/bugs/closed/3481.v b/test-suite/bugs/closed/3481.v index 89d476dcb..38f03b166 100644 --- a/test-suite/bugs/closed/3481.v +++ b/test-suite/bugs/closed/3481.v @@ -3,7 +3,7 @@ Set Implicit Arguments. Require Import Logic. Module NonPrim. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Record prodwithlet (A B : Type) : Type := pair' { fst : A; fst' := fst; snd : B }. @@ -21,7 +21,7 @@ End NonPrim. Global Set Universe Polymorphism. Global Set Asymmetric Patterns. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Local Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index 5adc48215..1f0f3b0da 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -69,26 +69,6 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) refine (P _ _) end; unfold Basics.flip. Focus 2. - Set Typeclasses Debug. - Set Typeclasses Legacy Resolution. - apply reflexivity. - (* Debug: 1.1: apply @IsPointed_catOP on -(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0)) -Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0)) -Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x)) -Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails) -Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities -Debug: Backtracking after apply @Equivalence_Reflexive -Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails) -Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails) -Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred) -*) - Undo. Unset Typeclasses Legacy Resolution. - Test Typeclasses Unique Solutions. - Test Typeclasses Unique Instances. - Show Existentials. - Set Typeclasses Debug Verbosity 2. - Set Printing All. (* As in 8.5, allow a shelved subgoal to remain *) apply reflexivity. diff --git a/test-suite/bugs/closed/3520.v b/test-suite/bugs/closed/3520.v index c981207e6..ea122e521 100644 --- a/test-suite/bugs/closed/3520.v +++ b/test-suite/bugs/closed/3520.v @@ -3,7 +3,7 @@ Set Primitive Projections. Record foo (A : Type) := { bar : Type ; baz := Set; bad : baz = bar }. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Record notprim : Prop := { irrel : True; relevant : nat }. diff --git a/test-suite/bugs/closed/3662.v b/test-suite/bugs/closed/3662.v index bd53389b4..b8754bce9 100644 --- a/test-suite/bugs/closed/3662.v +++ b/test-suite/bugs/closed/3662.v @@ -1,6 +1,6 @@ Set Primitive Projections. Set Implicit Arguments. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Record prod A B := pair { fst : A ; snd : B }. Definition f : Set -> Type := fun x => x. diff --git a/test-suite/bugs/closed/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v index 017780c1f..f69c71a02 100644 --- a/test-suite/bugs/closed/HoTT_coq_077.v +++ b/test-suite/bugs/closed/HoTT_coq_077.v @@ -3,7 +3,7 @@ Set Implicit Arguments. Require Import Logic. Set Asymmetric Patterns. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/closed/HoTT_coq_104.v b/test-suite/bugs/closed/HoTT_coq_104.v index 5bb7fa8c1..a6ff78d12 100644 --- a/test-suite/bugs/closed/HoTT_coq_104.v +++ b/test-suite/bugs/closed/HoTT_coq_104.v @@ -4,7 +4,7 @@ Require Import Logic. Global Set Universe Polymorphism. Global Set Asymmetric Patterns. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Local Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/opened/3926.v b/test-suite/bugs/opened/3926.v deleted file mode 100644 index cfad76357..000000000 --- a/test-suite/bugs/opened/3926.v +++ /dev/null @@ -1,30 +0,0 @@ -Notation compose := (fun g f x => g (f x)). -Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. -Open Scope function_scope. -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. -Arguments idpath {A a} , [A] a. -Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end. -Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }. -Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. -Local Open Scope equiv_scope. -Axiom eisretr : forall {A B} (f : A -> B) `{IsEquiv A B f} x, f (f^-1 x) = x. -Generalizable Variables A B C f g. -Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000 - := Build_IsEquiv A C (compose g f) (compose f^-1 g^-1). -Definition isequiv_homotopic {A B} (f : A -> B) {g : A -> B} `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g - := Build_IsEquiv _ _ g (f ^-1). -Global Instance isequiv_inverse {A B} (f : A -> B) `{IsEquiv A B f} : IsEquiv f^-1 | 10000 - := Build_IsEquiv B A f^-1 f. -Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C} - `{IsEquiv A B f} `{IsEquiv A C (g o f)} - : IsEquiv g. -Proof. - Unset Typeclasses Modulo Eta. - exact (isequiv_homotopic (compose (compose g f) f^-1) - (fun b => ap g (eisretr f b))) || fail "too early". - Undo. - Set Typeclasses Modulo Eta. - Set Typeclasses Dependency Order. - Set Typeclasses Debug. - Fail exact (isequiv_homotopic (compose (compose g f) f^-1) - (fun b => ap g (eisretr f b))). diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 893d75b77..5b1482fd5 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -200,3 +200,9 @@ Module NonRecLetIn. (fun n b c => f_equal (Rec n) eq_refl) 0 (Rec 0 (Base 1)). End NonRecLetIn. + +(* Test treatment of let-in in the definition of Records *) +(* Should fail with "Sort expected" *) + +Fail Inductive foo (T : Type) : let T := Type in T := + { r : forall x : T, x = x }. diff --git a/test-suite/success/letproj.v b/test-suite/success/letproj.v index a183be622..de2857b43 100644 --- a/test-suite/success/letproj.v +++ b/test-suite/success/letproj.v @@ -1,5 +1,5 @@ Set Primitive Projections. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Record Foo (A : Type) := { bar : A -> A; baz : A }. Definition test (A : Type) (f : Foo A) := diff --git a/test-suite/success/old_typeclass.v b/test-suite/success/old_typeclass.v deleted file mode 100644 index 01e35810b..000000000 --- a/test-suite/success/old_typeclass.v +++ /dev/null @@ -1,13 +0,0 @@ -Require Import Setoid Coq.Classes.Morphisms. -Set Typeclasses Legacy Resolution. - -Declare Instance and_Proper_eq: Proper (Logic.eq ==> Logic.eq ==> Logic.eq) and. - -Axiom In : Prop. -Axiom union_spec : In <-> True. - -Lemma foo : In /\ True. -Proof. -progress rewrite union_spec. -repeat constructor. -Qed. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 576bdbf71..31a1608c4 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -1,5 +1,5 @@ Set Primitive Projections. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Module Prim. Record F := { a : nat; b : a = a }. diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 779926a7d..41c44b126 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -61,13 +61,6 @@ let _ = optkey = ["Nonrecursive";"Elimination";"Schemes"]; optread = (fun () -> !bifinite_elim_flag) ; optwrite = (fun b -> bifinite_elim_flag := b) } -let _ = - declare_bool_option - { optdepr = true; (* compatibility 2014-09-03*) - optname = "automatic declaration of induction schemes for non-recursive types"; - optkey = ["Record";"Elimination";"Schemes"]; - optread = (fun () -> !bifinite_elim_flag) ; - optwrite = (fun b -> bifinite_elim_flag := b) } let case_flag = ref false let _ = diff --git a/vernac/record.ml b/vernac/record.ml index 1991a8640..e21f53f55 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -124,7 +124,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = match t with | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in - let sred = Reductionops.whd_all env sigma s in + let sred = Reductionops.whd_allnolet env sigma s in (match EConstr.kind sigma sred with | Sort s' -> let s' = EConstr.ESorts.kind sigma s' in |