diff options
Diffstat (limited to 'tactics')
40 files changed, 252 insertions, 609 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index eec7a5f2a..3eea1a74f 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 diff --git a/tactics/auto.mli b/tactics/auto.mli index 59809331e..a835c1ed9 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 *) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index de98f6382..780de8978 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 44acf3c01..96c08d58d 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 b101b3a9f..8e50c977e 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 a48c866da..861c9b625 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 b8860d3a5..9f6624889 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) -> @@ -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; @@ -1404,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, @@ -1529,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 -> @@ -1579,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 d8a1d2ab8..9ba69a058 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 3386f972e..c285f21e7 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 diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 59f8a328e..2b3a94758 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 73afc2eac..17ff94ec9 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 92c84fc9a..647bbd6bc 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 785d2f515..dc310c542 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 diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 8f847737f..e161d8882 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 b5668dfff..003b069b6 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 0930f9a92..d6b67e5ba 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 e427adb15..6bd4866c6 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 50b052f23..ece4124b8 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 8764ef085..b0deeed17 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 2d22710b2..1e898d427 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 d7667668e..45926551b 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 90ae67c6c..4749aebd9 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 96a53a8b1..236db1dcc 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,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/equality.mli b/tactics/equality.mli index 65da2e7dc..c0be917a0 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 10cd7e1f6..f3e0619a2 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 diff --git a/tactics/hints.mli b/tactics/hints.mli index cbf204981..1811150c2 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 2bb9be66b..a59046a67 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 01d916053..0697d0f19 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 diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index bc2fea2bd..b960a845c 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 d73595a2f..0eb4e47ae 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 5435b63ce..280efdaec 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 diff --git a/tactics/inv.mli b/tactics/inv.mli index 828cf7a04..c63d57af5 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 197b3030d..655283c20 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 f221b1fd9..2337a7901 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 0cc0001c1..789cc35ee 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 diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index a3bc4707e..f0ebac780 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 diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 61ca3e319..b99a45103 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 @@ -644,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 @@ -1686,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 @@ -1777,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/tactics/tactics.mli b/tactics/tactics.mli index 100ddf17f..1c3b75e91 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 @@ -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 -> diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 7567cfa30..753c608ad 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 db7da18ba..2c748f9c9 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 |