diff options
Diffstat (limited to 'tactics')
40 files changed, 326 insertions, 724 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index e7e21b5f4b..3eea1a74fd 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) module CVars = Vars @@ -32,7 +34,7 @@ open Hints let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l let compute_secvars gl = - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in secvars_of_hyps hyps (* tell auto not to reuse already instantiated metas in unification (for @@ -316,7 +318,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let nf c = Evarutil.nf_evar sigma c in - let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in + let decl = Tacmach.New.pf_last_hyp gl in let hyp = Context.Named.Declaration.map_constr nf decl in let hintl = make_resolve_hyp env sigma hyp in trivial_fail_db dbg mod_delta db_list diff --git a/tactics/auto.mli b/tactics/auto.mli index b9cd4932ca..a835c1ed95 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This files implements auto and related automation tactics *) @@ -16,14 +18,14 @@ open Decl_kinds open Hints open Tactypes -val compute_secvars : 'a Proofview.Goal.t -> Id.Pred.t +val compute_secvars : Proofview.Goal.t -> Id.Pred.t val default_search_depth : int ref val auto_flags_of_state : transparent_state -> Unification.unify_flags val connect_hint_clenv : polymorphic -> raw_hint -> clausenv -> - 'a Proofview.Goal.t -> clausenv * constr + Proofview.Goal.t -> clausenv * constr (** Try unification with the precompiled clause, then use registered Apply *) val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index de98f63823..780de89786 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Equality diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 44acf3c018..96c08d58d7 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This files implements the autorewrite tactic. *) diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index b101b3a9f5..8e50c977e7 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index a48c866daf..861c9b6250 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pattern diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index cfadfc5353..9f66248897 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* TODO: @@ -18,7 +20,6 @@ open Names open Term open Termops open EConstr -open Proof_type open Tacmach open Tactics open Clenv @@ -26,7 +27,6 @@ open Typeclasses open Globnames open Evd open Locus -open Misctypes open Proofview.Notations open Hints @@ -39,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 @@ -69,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 @@ -92,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)"; @@ -125,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"]; @@ -197,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 = @@ -424,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) -> @@ -439,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) -> @@ -581,7 +548,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = (fun (path,info,c) -> let info = { info with Vernacexpr.hint_pattern = - Option.map (Constrintern.intern_constr_pattern env) + Option.map (Constrintern.intern_constr_pattern env sigma) info.Vernacexpr.hint_pattern } in make_resolves env sigma ~name:(PathHints path) @@ -616,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; @@ -996,7 +610,7 @@ module Search = struct Hint_db.transparent_state cached_hints == st then cached_hints else - let hints = make_hints {it = Goal.goal (Proofview.Goal.assume g); sigma = project g} + let hints = make_hints {it = Goal.goal g; sigma = project g} st only_classes sign in autogoal_cache := (cwd, only_classes, sign, hints); hints @@ -1041,7 +655,6 @@ module Search = struct let fail_if_nonclass info = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let sigma = Proofview.Goal.sigma gl in if is_class_type sigma (Proofview.Goal.concl gl) then Proofview.tclUNIT () @@ -1089,7 +702,7 @@ module Search = struct pr_depth (idx :: info.search_depth) ++ str": " ++ Lazy.force pp ++ (if !foundone != true then - str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal (Proofview.Goal.assume gl)) + str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal gl) else mt ()) in let msg = @@ -1110,7 +723,7 @@ module Search = struct if !typeclasses_debug > 0 then Feedback.msg_debug (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++ - pr_ev sigma' (Proofview.Goal.goal (Proofview.Goal.assume gl'))); + pr_ev sigma' (Proofview.Goal.goal gl')); let eq c1 c2 = EConstr.eq_constr sigma' c1 c2 in let hints' = if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl)) @@ -1119,7 +732,7 @@ module Search = struct make_autogoal_hints info.search_only_classes ~st gl' else info.search_hints in - let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal (Proofview.Goal.assume gl')) gls in + let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal gl') gls in let info' = { search_depth = succ j :: i :: info.search_depth; last_tac = pp; @@ -1132,11 +745,12 @@ module Search = struct let rec result (shelf, ()) i k = foundone := true; Proofview.Unsafe.tclGETGOALS >>= fun gls -> + let gls = CList.map Proofview.drop_state gls in let j = List.length gls in (if !typeclasses_debug > 0 then Feedback.msg_debug (pr_depth (i :: info.search_depth) ++ str": " ++ Lazy.force pp - ++ str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal (Proofview.Goal.assume gl)) + ++ str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal gl) ++ str", " ++ int j ++ str" subgoal(s)" ++ (Option.cata (fun k -> str " in addition to the first " ++ int k) (mt()) k))); @@ -1180,7 +794,7 @@ module Search = struct (if List.is_empty goals then tclUNIT () else let sigma' = mark_unresolvables sigma goals in - with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS goals) >>= + with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state goals)) >>= fun s -> result s i (Some (Option.default 0 k + j))) end in with_shelf res >>= fun (sh, ()) -> @@ -1261,7 +875,7 @@ module Search = struct 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 - let dep = dep || Proofview.unifiable sigma (Goal.goal (Proofview.Goal.assume gl)) gls in + let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in search_tac hints depth 1 info @@ -1273,6 +887,7 @@ module Search = struct search_tac_gl ~st only_classes dep hints depth (succ i) sigma gls gl end in Proofview.Unsafe.tclGETGOALS >>= fun gls -> + let gls = CList.map Proofview.drop_state gls in Proofview.tclEVARMAP >>= fun sigma -> let j = List.length gls in (tclDISPATCH (List.init j (fun i -> tac sigma gls i))) @@ -1403,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, @@ -1528,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 -> @@ -1578,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/class_tactics.mli b/tactics/class_tactics.mli index d8a1d2ab85..9ba69a0584 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This files implements typeclasses eauto *) diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 5e2006ccc8..c285f21e77 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Term @@ -44,8 +46,6 @@ let absurd c = absurd c (* Contradiction *) -let use_negated_unit_or_eq_type () = Flags.version_strictly_greater Flags.V8_5 - (** [f] does not assume its argument to be [nf_evar]-ed. *) let filter_hyp f tac = let rec seek = function @@ -53,7 +53,7 @@ let filter_hyp f tac = | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d) | _::rest -> seek rest in Proofview.Goal.enter begin fun gl -> - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in seek hyps end @@ -71,9 +71,7 @@ let contradiction_context = simplest_elim (mkVar id) else match EConstr.kind sigma typ with | Prod (na,t,u) when is_empty_type sigma u -> - let is_unit_or_eq = - if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type sigma t - else None in + let is_unit_or_eq = match_with_unit_or_eq_type sigma t in Tacticals.New.tclORELSE (match is_unit_or_eq with | Some _ -> @@ -98,7 +96,7 @@ let contradiction_context = end) | _ -> seek_neg rest in - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in seek_neg hyps end diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 59f8a328ea..2b3a947586 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open EConstr diff --git a/tactics/dnet.ml b/tactics/dnet.ml index 73afc2eac2..17ff94ec9c 100644 --- a/tactics/dnet.ml +++ b/tactics/dnet.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Generic dnet implementation over non-recursive types *) diff --git a/tactics/dnet.mli b/tactics/dnet.mli index 92c84fc9ad..647bbd6bcb 100644 --- a/tactics/dnet.mli +++ b/tactics/dnet.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Generic discrimination net implementation over recursive diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 6ea6155e0d..dc310c542d 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -32,7 +34,7 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state let e_give_exact ?(flags=eauto_unif_flags) c = Proofview.Goal.enter begin fun gl -> let t1 = Tacmach.New.pf_unsafe_type_of gl c in - let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in + let t2 = Tacmach.New.pf_concl gl in let sigma = Tacmach.New.project gl in if occur_existential sigma t1 || occur_existential sigma t2 then Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 8f847737fe..e161d88824 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open EConstr diff --git a/tactics/elim.ml b/tactics/elim.ml index b5668dfff0..003b069b6e 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/tactics/elim.mli b/tactics/elim.mli index 0930f9a92a..d6b67e5ba6 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index e427adb15d..6bd4866c61 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Hugo Herbelin from contents related to inductive schemes diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index 50b052f23b..ece4124b8b 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Ind_tables diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 8764ef085d..b0deeed17e 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (************************************************************************) diff --git a/tactics/eqdecide.mli b/tactics/eqdecide.mli index 2d22710b2c..1e898d427b 100644 --- a/tactics/eqdecide.mli +++ b/tactics/eqdecide.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (************************************************************************) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index d7667668e8..45926551b4 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* File created by Hugo Herbelin, Nov 2009 *) diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index 90ae67c6cf..4749aebd96 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file builds schemes relative to equality inductive types *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 450d684364..236db1dcc1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) module CVars = Vars @@ -67,24 +69,14 @@ 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 - | None -> !injection_in_context && Flags.version_strictly_greater Flags.V8_5 + | None -> !injection_in_context | Some flags -> flags.injection_in_context let _ = @@ -266,7 +258,7 @@ let rewrite_elim with_evars frzevars cls c e = end let tclNOTSAMEGOAL tac = - let goal gl = Proofview.Goal.goal (Proofview.Goal.assume gl) in + let goal gl = Proofview.Goal.goal gl in Proofview.Goal.nf_enter begin fun gl -> let sigma = project gl in let ev = goal gl in @@ -324,7 +316,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim = in let typ = match cls with | None -> pf_concl gl - | Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl) + | Some id -> pf_get_hyp_typ id gl in let cs = instantiate_lemma typ in if firstonly then tclFIRST (List.map try_clause cs) @@ -533,7 +525,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl = let rec do_hyps_atleastonce = function | [] -> tclZEROMSG (Pp.str"Nothing to rewrite.") | id :: l -> - tclIFTHENTRYELSEMUST + tclIFTHENFIRSTTRYELSEMUST (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars) (do_hyps_atleastonce l) in @@ -549,7 +541,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl = end in if cl.concl_occs == NoOccurrences then do_hyps else - tclIFTHENTRYELSEMUST + tclIFTHENFIRSTTRYELSEMUST (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars) do_hyps @@ -970,7 +962,7 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function let gen_absurdity id = Proofview.Goal.enter begin fun gl -> let sigma = project gl in - let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in + let hyp_typ = pf_get_hyp_typ id gl in if is_empty_type sigma hyp_typ then simplest_elim (mkVar id) @@ -1443,7 +1435,7 @@ let get_previous_hyp_position id gl = let hyp = Context.Named.Declaration.get_id d in if Id.equal hyp id then dest else aux (MoveAfter hyp) right in - aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) + aux MoveLast (Proofview.Goal.hyps gl) let injEq flags ?(old=false) with_evars clear_flag ipats = (* Decide which compatibility mode to use *) @@ -1484,7 +1476,7 @@ let simpleInjClause flags with_evars = function | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq flags ~old:true with_evars clear_flag None)) c let injConcl flags = injClause flags None false None -let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent (Loc.tag id))) +let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent CAst.(make id))) let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause = Proofview.Goal.enter begin fun gl -> @@ -1716,8 +1708,8 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in + let concl = Proofview.Goal.concl gl in (* The set of hypotheses using x *) let dephyps = List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) -> @@ -1749,7 +1741,6 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = let subst_one_var dep_proof_ok x = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let decl = pf_get_hyp x gl in (* If x has a body, simply replace x with body and clear x *) if is_local_def decl then tclTHEN (unfold_body x) (clear [x]) else @@ -1790,7 +1781,6 @@ let subst_all ?(flags=default_subst_tactic_flags) () = (* First step: find hypotheses to treat in linear time *) let find_equations gl = - let gl = Proofview.Goal.assume gl in let env = Proofview.Goal.env gl in let sigma = project gl in let find_eq_data_decompose = find_eq_data_decompose gl in @@ -1816,7 +1806,6 @@ let subst_all ?(flags=default_subst_tactic_flags) () = (* Second step: treat equations *) let process hyp = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let sigma = project gl in let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in diff --git a/tactics/equality.mli b/tactics/equality.mli index 65da2e7dc0..c0be917a08 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) diff --git a/tactics/hints.ml b/tactics/hints.ml index 7f9b5ef34e..f3e0619a2d 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -1270,7 +1272,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = let interp_hints poly = fun h -> - let env = (Global.env()) in + let env = Global.env () in let sigma = Evd.from_env env in let f poly c = let evd,c = Constrintern.interp_open_constr env sigma c in @@ -1279,9 +1281,7 @@ let interp_hints poly = let gr = global_with_alias r in Dumpglob.add_glob ?loc:(loc_of_reference r) gr; gr in - let fr r = - evaluable_of_global_reference (Global.env()) (fref r) - in + let fr r = evaluable_of_global_reference env (fref r) in let fi c = match c with | HintsReference c -> @@ -1289,7 +1289,7 @@ let interp_hints poly = (PathHints [gr], poly, IsGlobRef gr) | HintsConstr c -> (PathAny, poly, f poly c) in - let fp = Constrintern.intern_constr_pattern (Global.env()) in + let fp = Constrintern.intern_constr_pattern env sigma in let fres (info, b, r) = let path, poly, gr = fi r in let info = { info with hint_pattern = Option.map fp info.hint_pattern } in diff --git a/tactics/hints.mli b/tactics/hints.mli index cbf204981e..1811150c2a 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 2bb9be66ba..a59046a678 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 237ed42d55..0697d0f19c 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -120,11 +122,11 @@ val match_with_equation: (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *) -val find_eq_data_decompose : 'a Proofview.Goal.t -> constr -> +val find_eq_data_decompose : Proofview.Goal.t -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** Idem but fails with an error message instead of PatternMatchingFailure *) -val find_this_eq_data_decompose : 'a Proofview.Goal.t -> constr -> +val find_this_eq_data_decompose : Proofview.Goal.t -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** A variant that returns more informative structure on the equality found *) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index bc2fea2bd5..b960a845ce 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* File created by Vincent Siles, Oct 2007, extended into a generic diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index d73595a2f8..0eb4e47aeb 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/tactics/inv.ml b/tactics/inv.ml index cb0bbfd0e7..280efdaece 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -353,7 +355,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = Proofview.Goal.enter begin fun gl -> let sigma = project gl in (** We only look at the type of hypothesis "id" *) - let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in + let hyp = pf_nf_evar gl (pf_get_hyp_typ id gl) in let (t,t1,t2) = dest_nf_eq (pf_env gl) sigma hyp in match (EConstr.kind sigma t1, EConstr.kind sigma t2) with | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 diff --git a/tactics/inv.mli b/tactics/inv.mli index 828cf7a044..c63d57af54 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 197b3030d9..655283c204 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/tactics/leminv.mli b/tactics/leminv.mli index f221b1fd9a..2337a79016 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index cea6ccc303..789cc35ee7 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -408,8 +410,14 @@ module New = struct Proofview.tclIFCATCH t1 (fun () -> tclDISPATCH (Array.to_list a)) (fun _ -> t3) + let tclIFTHENFIRSTELSE t1 t2 t3 = + Proofview.tclIFCATCH t1 + (fun () -> tclEXTEND [t2] (tclUNIT ()) []) + (fun _ -> t3) let tclIFTHENTRYELSEMUST t1 t2 = tclIFTHENELSE t1 (tclTRY t2) t2 + let tclIFTHENFIRSTTRYELSEMUST t1 t2 = + tclIFTHENFIRSTELSE t1 (tclTRY t2) t2 (* Try the first tactic that does not fail in a list of tactics *) let rec tclFIRST = function @@ -540,7 +548,6 @@ module New = struct let nthHypId m gl = (** We only use [id] *) - let gl = Proofview.Goal.assume gl in nthDecl m gl |> NamedDecl.get_id let nthHyp m gl = mkVar (nthHypId m gl) @@ -572,7 +579,7 @@ module New = struct let afterHyp id tac = Proofview.Goal.enter begin fun gl -> - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in let rem, _ = List.split_when (NamedDecl.get_id %> Id.equal id) hyps in tac rem end @@ -658,12 +665,12 @@ module New = struct let elimination_sort_of_goal gl = (** Retyping will expand evars anyway. *) - let c = Proofview.Goal.concl (Goal.assume gl) in + let c = Proofview.Goal.concl gl in pf_apply Retyping.get_sort_family_of gl c let elimination_sort_of_hyp id gl = (** Retyping will expand evars anyway. *) - let c = pf_get_hyp_typ id (Goal.assume gl) in + let c = pf_get_hyp_typ id gl in pf_apply Retyping.get_sort_family_of gl c let elimination_sort_of_clause id gl = match id with diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 55c519e24d..f0ebac780e 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -210,6 +212,7 @@ module New : sig val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic val tclIFTHENTRYELSEMUST : unit tactic -> unit tactic -> unit tactic + val tclIFTHENFIRSTTRYELSEMUST : unit tactic -> unit tactic -> unit tactic val tclDO : int -> unit tactic -> unit tactic val tclREPEAT : unit tactic -> unit tactic @@ -225,7 +228,7 @@ module New : sig val tclTIMEOUT : int -> unit tactic -> unit tactic val tclTIME : string option -> 'a tactic -> 'a tactic - val nLastDecls : 'a Proofview.Goal.t -> int -> named_context + val nLastDecls : Proofview.Goal.t -> int -> named_context val ifOnHyp : (Id.t * types -> bool) -> (Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) -> @@ -236,7 +239,7 @@ module New : sig val onLastHyp : (constr -> unit tactic) -> unit tactic val onLastDecl : (named_declaration -> unit tactic) -> unit tactic - val onHyps : ([ `LZ ] Proofview.Goal.t -> named_context) -> + val onHyps : (Proofview.Goal.t -> named_context) -> (named_context -> unit tactic) -> unit tactic val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic @@ -244,9 +247,9 @@ module New : sig val tryAllHypsAndConcl : (Id.t option -> unit tactic) -> unit tactic val onClause : (Id.t option -> unit tactic) -> clause -> unit tactic - val elimination_sort_of_goal : 'a Proofview.Goal.t -> Sorts.family - val elimination_sort_of_hyp : Id.t -> 'a Proofview.Goal.t -> Sorts.family - val elimination_sort_of_clause : Id.t option -> 'a Proofview.Goal.t -> Sorts.family + val elimination_sort_of_goal : Proofview.Goal.t -> Sorts.family + val elimination_sort_of_hyp : Id.t -> Proofview.Goal.t -> Sorts.family + val elimination_sort_of_clause : Id.t option -> Proofview.Goal.t -> Sorts.family val elimination_then : (branch_args -> unit Proofview.tactic) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9fded04dbe..b99a451030 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) module CVars = Vars @@ -59,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 @@ -151,7 +143,6 @@ let unsafe_intro env store decl b = let introduction ?(check=true) id = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let hyps = named_context_val (Proofview.Goal.env gl) in @@ -258,7 +249,6 @@ let clear_gen fail = function Proofview.Goal.enter begin fun gl -> let ids = List.fold_right Id.Set.add ids Id.Set.empty in (** clear_hyps_in_evi does not require nf terms *) - let gl = Proofview.Goal.assume gl in let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in @@ -322,7 +312,6 @@ let rename_hyp repl = | None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping") | Some (src, dst) -> Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in @@ -647,7 +636,8 @@ let cofix ido = match ido with (* Reduction and conversion tactics *) (**************************************************************) -type tactic_reduction = env -> evar_map -> constr -> constr +type tactic_reduction = Reductionops.reduction_function +type e_tactic_reduction = Reductionops.e_reduction_function let pf_reduce_decl redfun where decl gl = let open Context.Named.Declaration in @@ -814,7 +804,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm let e_change_in_hyp redfun (id,where) = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let hyp = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in + let hyp = Tacmach.New.pf_get_hyp id gl in let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (convert_hyp c) @@ -981,7 +971,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Tacmach.New.pf_env gl in - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let concl = Proofview.Goal.concl gl in match EConstr.kind sigma concl with | Prod (name,t,u) when not dep_flag || not (noccurn sigma 1 u) -> let name = find_name false (LocalAssum (name,t)) name_flag gl in @@ -1052,7 +1042,7 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = let intro_replacing id = Proofview.Goal.enter begin fun gl -> let env, sigma = Proofview.Goal.(env gl, sigma gl) in - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in let next_hyp = get_next_hyp_position env sigma id hyps in Tacticals.New.tclTHENLIST [ clear_for_replacing [id]; @@ -1073,7 +1063,7 @@ let intros_possibly_replacing ids = let suboptimal = true in Proofview.Goal.enter begin fun gl -> let env, sigma = Proofview.Goal.(env gl, sigma gl) in - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.New.tclTHEN (Tacticals.New.tclMAP (fun id -> @@ -1087,7 +1077,7 @@ let intros_possibly_replacing ids = (* This version assumes that replacement is actually possible *) let intros_replacing ids = Proofview.Goal.enter begin fun gl -> - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in let env, sigma = Proofview.Goal.(env gl, sigma gl) in let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.New.tclTHEN @@ -1150,7 +1140,7 @@ let intros_until_n = intros_until_n_gen true let tclCHECKVAR id = Proofview.Goal.enter begin fun gl -> - let _ = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in + let _ = Tacmach.New.pf_get_hyp id gl in Proofview.tclUNIT () end @@ -1193,7 +1183,7 @@ let onOpenInductionArg env sigma tac = function let sigma = Tacmach.New.project gl in tac clear_flag (sigma,(c,NoBindings)) end)) - | clear_flag,ElimOnIdent (_,id) -> + | clear_flag,ElimOnIdent {CAst.v=id} -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) @@ -1209,7 +1199,7 @@ let onInductionArg tac = function Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp (fun c -> tac clear_flag (c,NoBindings))) - | clear_flag,ElimOnIdent (_,id) -> + | clear_flag,ElimOnIdent {CAst.v=id} -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) @@ -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 @@ -1973,7 +1945,7 @@ let exact_check c = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in (** We do not need to normalize the goal because we just check convertibility *) - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let sigma, ct = Typing.type_of env sigma c in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) @@ -1982,7 +1954,7 @@ let exact_check c = let cast_no_check cast c = Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let concl = Proofview.Goal.concl gl in exact_no_check (mkCast (c, cast, concl)) end @@ -1994,7 +1966,6 @@ let exact_proof c = Proofview.Goal.enter begin fun gl -> Refine.refine ~typecheck:false begin fun sigma -> let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (pf_concl gl) in - let c = EConstr.of_constr c in let sigma = Evd.merge_universe_context sigma ctx in (sigma, c) end @@ -2066,7 +2037,7 @@ let clear_body ids = let open Context.Named.Declaration in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let ctx = named_context env in let map = function @@ -2157,11 +2128,11 @@ let keep hyps = and [a1..an:A1..An(a1..an-1)] such that the goal is [G(a1..an)], this generalizes [hyps |- goal] into [hyps |- T] *) -let apply_type newcl args = +let apply_type ~typecheck newcl args = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in - Refine.refine ~typecheck:false begin fun sigma -> + Refine.refine ~typecheck begin fun sigma -> let newcl = nf_betaiota env sigma newcl (* As in former Logic.refine *) in let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true ~store newcl in @@ -2191,7 +2162,6 @@ let bring_hyps hyps = let revert hyps = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in (bring_hyps ctx) <*> (clear hyps) end @@ -2619,7 +2589,7 @@ 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 ( let env, sigma = Proofview.Goal.(env gl, sigma gl) in - get_previous_hyp_position env sigma id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) + get_previous_hyp_position env sigma id (Proofview.Goal.hyps gl) ) in let naming,ipat_tac = prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in @@ -2893,7 +2863,7 @@ let generalize_dep ?(with_let=false) c = let args = Context.Named.to_instance mkVar to_quantify_rev in tclTHENLIST [ Proofview.Unsafe.tclEVARS evd; - apply_type cl'' (if Option.is_empty body then c::args else args); + apply_type ~typecheck:false cl'' (if Option.is_empty body then c::args else args); clear (List.rev tothin')] end @@ -2907,13 +2877,12 @@ let generalize_gen_let lconstr = Proofview.Goal.enter begin fun gl -> let (evd, _) = Typing.type_of env evd newcl in let map ((_, c, b),_) = if Option.is_empty b then Some c else None in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) - (apply_type newcl (List.map_filter map lconstr)) + (apply_type ~typecheck:false newcl (List.map_filter map lconstr)) end let new_generalize_gen_let lconstr = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let ids = Tacmach.New.pf_ids_of_hyps gl in @@ -3063,7 +3032,7 @@ let unfold_body x = let open Context.Named.Declaration in Proofview.Goal.enter begin fun gl -> (** We normalize the given hypothesis immediately. *) - let env = Proofview.Goal.env (Proofview.Goal.assume gl) in + let env = Proofview.Goal.env gl in let xval = match Environ.lookup_named x env with | LocalAssum _ -> user_err ~hdr:"unfold_body" (Id.print x ++ str" is not a defined hypothesis.") @@ -3274,7 +3243,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in + let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in let typ0 = reduce_to_quantified_ref indref tmptyp0 in let prods, indtyp = decompose_prod_assum sigma typ0 in @@ -4272,7 +4241,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let deps_cstr = List.fold_left (fun a decl -> if NamedDecl.is_local_assum decl then (mkVar (NamedDecl.get_id decl))::a else a) [] deps in - let (sigma, isrec, elim, indsign) = get_eliminator elim dep s (Proofview.Goal.assume gl) in + let (sigma, isrec, elim, indsign) = get_eliminator elim dep s gl in let branchletsigns = let f (_,is_not_let,_,_) = is_not_let in Array.map (fun (_,l) -> List.map f l) indsign in @@ -4282,7 +4251,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) (Tacticals.New.tclTHENLIST [ (* Generalize dependent hyps (but not args) *) - if deps = [] then Proofview.tclUNIT () else apply_type tmpcl deps_cstr; + if deps = [] then Proofview.tclUNIT () else apply_type ~typecheck:false tmpcl deps_cstr; (* side-conditions in elim (resp case) schemes come last (resp first) *) induct_tac elim; Tacticals.New.tclMAP expand_hyp toclear; @@ -4297,7 +4266,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps = Proofview.Goal.enter begin fun gl -> - let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in + let elim_info = find_induction_type isrec elim hyp0 gl in atomize_param_of_ind_then elim_info hyp0 (fun indvars -> apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names (fun elim -> induction_tac with_evars [] [hyp0] elim)) @@ -4667,30 +4636,6 @@ let destruct ev clr c l e = induction_gen clr false ev e ((Evd.empty,(c,NoBindings)),(None,l)) None -(* The registered tactic, which calls the default elimination - * if no elimination constant is provided. *) - -(* Induction tactics *) - -(* This was Induction before 6.3 (induction only in quantified premisses) *) -let simple_induct_id s = Tacticals.New.tclTHEN (intros_until_id s) (Tacticals.New.onLastHyp simplest_elim) -let simple_induct_nodep n = Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp simplest_elim) - -let simple_induct = function - | NamedHyp id -> simple_induct_id id - | AnonHyp n -> simple_induct_nodep n - -(* Destruction tactics *) - -let simple_destruct_id s = - (Tacticals.New.tclTHEN (intros_until_id s) (Tacticals.New.onLastHyp simplest_case)) -let simple_destruct_nodep n = - (Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp simplest_case)) - -let simple_destruct = function - | NamedHyp id -> simple_destruct_id id - | AnonHyp n -> simple_destruct_nodep n - (* * Eliminations giving the type instead of the proof. * These tactics use the default elimination constant and @@ -5151,16 +5096,10 @@ module New = struct open Locus let reduce_after_refine = - let onhyps = - (** We reduced everywhere in the hyps before 8.6 *) - if Flags.version_compare !Flags.compat_version Flags.V8_5 == 0 - then None - else Some [] - in reduce (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true; rZeta=false;rDelta=false;rConst=[]}) - {onhyps; concl_occs=AllOccurrences } + {onhyps = Some []; concl_occs = AllOccurrences } let refine ~typecheck c = Refine.refine ~typecheck c <*> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 83fc655f1c..1c3b75e91c 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Loc @@ -30,7 +32,7 @@ open Ltac_pretype (** {6 General functions. } *) -val is_quantified_hypothesis : Id.t -> 'a Proofview.Goal.t -> bool +val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) @@ -76,7 +78,7 @@ val intros : unit Proofview.tactic (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in the conclusion of goal [g], up to head-reduction if [b] is [true] *) val depth_of_quantified_hypothesis : - bool -> quantified_hypothesis -> 'a Proofview.Goal.t -> int + bool -> quantified_hypothesis -> Proofview.Goal.t -> int val intros_until : quantified_hypothesis -> unit Proofview.tactic @@ -130,7 +132,8 @@ val exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic (** {6 Reduction tactics. } *) -type tactic_reduction = env -> evar_map -> constr -> constr +type tactic_reduction = Reductionops.reduction_function +type e_tactic_reduction = Reductionops.e_reduction_function type change_arg = patvar_map -> evar_map -> evar_map * constr @@ -138,6 +141,7 @@ val make_change_arg : constr -> change_arg val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic val reduct_in_concl : tactic_reduction * cast_kind -> unit Proofview.tactic +val e_reduct_in_concl : check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic val change_in_concl : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic val change_concl : constr -> unit Proofview.tactic val change_in_hyp : (occurrences * constr_pattern) option -> change_arg -> @@ -185,7 +189,7 @@ val revert : Id.t list -> unit Proofview.tactic (** {6 Resolution tactics. } *) -val apply_type : constr -> constr list -> unit Proofview.tactic +val apply_type : typecheck:bool -> constr -> constr list -> unit Proofview.tactic val bring_hyps : named_context -> unit Proofview.tactic val apply : constr -> unit Proofview.tactic @@ -280,8 +284,6 @@ val simplest_elim : constr -> unit Proofview.tactic val elim : evars_flag -> clear_flag -> constr with_bindings -> constr with_bindings option -> unit Proofview.tactic -val simple_induct : quantified_hypothesis -> unit Proofview.tactic - val induction : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option -> constr with_bindings option -> unit Proofview.tactic @@ -290,7 +292,6 @@ val induction : evars_flag -> clear_flag -> constr -> or_and_intro_pattern optio val general_case_analysis : evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic val simplest_case : constr -> unit Proofview.tactic -val simple_destruct : quantified_hypothesis -> unit Proofview.tactic val destruct : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option -> constr with_bindings option -> unit Proofview.tactic diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 7567cfa304..753c608ada 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli index db7da18ba9..2c748f9c93 100644 --- a/tactics/term_dnet.mli +++ b/tactics/term_dnet.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr |