diff options
Diffstat (limited to 'tactics')
55 files changed, 324 insertions, 217 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 86e6a92a22..9b0a323078 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/abstract.mli b/tactics/abstract.mli index 779e46cd49..5c936ff9d6 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 1dde820075..5b06088518 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -303,7 +303,9 @@ let hintmap_of sigma secvars hdc concl = | None -> Hint_db.map_none ~secvars | Some hdc -> if occur_existential sigma concl then - Hint_db.map_existential sigma ~secvars hdc concl + (fun db -> match Hint_db.map_existential sigma ~secvars hdc concl db with + | ModeMatch l -> l + | ModeMismatch -> []) else Hint_db.map_auto sigma ~secvars hdc concl let exists_evaluable_reference env = function @@ -366,11 +368,14 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl = let st = Hint_db.transparent_state db in let flags, l = let l = - match hdc with None -> Hint_db.map_none ~secvars db + match hdc with + | None -> Hint_db.map_none ~secvars db | Some hdc -> if TransparentState.is_empty st then Hint_db.map_auto sigma ~secvars hdc concl db - else Hint_db.map_existential sigma ~secvars hdc concl db + else match Hint_db.map_existential sigma ~secvars hdc concl db with + | ModeMatch l -> l + | ModeMismatch -> [] in auto_flags_of_state st, l in List.map (fun x -> (Some flags,x)) l) (local_db::db_list) diff --git a/tactics/auto.mli b/tactics/auto.mli index 5ae63be539..33deefd0bd 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 1bbcca8827..ac83acd726 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 6df2ea9b12..8f7a1c8fcf 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index ae3aea5788..6e6af42010 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index d80fa49cc1..4358e5a8d9 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index e3f2f18b44..92d56d2904 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -189,7 +189,7 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' = Proofview.Goal.enter begin fun gls -> let resolve = try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls) - with e -> Proofview.tclZERO e + with e when noncritical e -> Proofview.tclZERO e in resolve >>= fun clenv' -> Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv' end @@ -234,9 +234,8 @@ let unify_resolve_refine poly flags gl clenv = match fst ie with | Evarconv.UnableToUnify _ -> Tacticals.New.tclZEROMSG (str "Unable to unify") - | e when CErrors.noncritical e -> - Tacticals.New.tclZEROMSG (str "Unexpected error") - | _ -> Exninfo.iraise ie) + | e -> + Tacticals.New.tclZEROMSG (str "Unexpected error")) (** Dealing with goals of the form A -> B and hints of the form C -> A -> B. @@ -309,12 +308,12 @@ let shelve_dependencies gls = let hintmap_of sigma hdc secvars concl = match hdc with - | None -> fun db -> Hint_db.map_none ~secvars db + | None -> fun db -> ModeMatch (Hint_db.map_none ~secvars db) | Some hdc -> fun db -> - if Hint_db.use_dn db then (* Using dnet *) - Hint_db.map_eauto sigma ~secvars hdc concl db - else Hint_db.map_existential sigma ~secvars hdc concl db + if Hint_db.use_dn db then (* Using dnet *) + Hint_db.map_eauto sigma ~secvars hdc concl db + else Hint_db.map_existential sigma ~secvars hdc concl db (** Hack to properly solve dependent evars that are typeclasses *) let rec e_trivial_fail_db only_classes db_list local_db secvars = @@ -362,15 +361,6 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm | _ -> AllowAll with e when CErrors.noncritical e -> AllowAll in - let hint_of_db = hintmap_of sigma hdc secvars concl in - let hintl = - List.map_append - (fun db -> - let tacs = hint_of_db db in - let flags = auto_unif_flags ~allowed_evars (Hint_db.transparent_state db) in - List.map (fun x -> (flags, x)) tacs) - (local_db::db_list) - in let tac_of_hint = fun (flags, {pri = b; pat = p; poly = poly; code = t; secvars; name = name}) -> let tac = function @@ -428,26 +418,47 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm match repr_hint t with | Extern _ -> (tac, b, true, name, lazy (pr_hint env sigma t ++ pp)) | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp)) - in List.map tac_of_hint hintl + in + let hint_of_db = hintmap_of sigma hdc secvars concl in + let hintl = List.map_filter (fun db -> match hint_of_db db with + | ModeMatch l -> Some (db, l) + | ModeMismatch -> None) + (local_db :: db_list) + in + (* In case there is a mode mismatch in all the databases we get stuck. + Otherwise we consider the hints that match. + Recall the local database uses the union of all the modes in the other databases. *) + if List.is_empty hintl then ModeMismatch + else + let hintl = + CList.map_append + (fun (db, tacs) -> + let flags = auto_unif_flags ~allowed_evars (Hint_db.transparent_state db) in + List.map (fun x -> (flags, x)) tacs) + hintl + in + ModeMatch (List.map tac_of_hint hintl) and e_trivial_resolve db_list local_db secvars only_classes env sigma concl = let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in try - e_my_find_search db_list local_db secvars hd true only_classes env sigma concl + (match e_my_find_search db_list local_db secvars hd true only_classes env sigma concl with + | ModeMatch l -> l + | ModeMismatch -> []) with Not_found -> [] let e_possible_resolve db_list local_db secvars only_classes env sigma concl = let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in try e_my_find_search db_list local_db secvars hd false only_classes env sigma concl - with Not_found -> [] + with Not_found -> ModeMatch [] let cut_of_hints h = List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h let catchable = function | Refiner.FailError _ -> true - | e -> Logic.catchable_exception e + | e -> Logic.catchable_exception e [@@ocaml.warning "-3"] let pr_depth l = let rec fmt elts = @@ -606,6 +617,7 @@ module Search = struct (** In the proof engine failures are represented as exceptions *) exception ReachedLimitEx exception NoApplicableEx + exception StuckClass (** ReachedLimitEx has priority over NoApplicableEx to handle iterative deepening: it should fail when no hints are applicable, @@ -644,8 +656,11 @@ module Search = struct (if backtrack then str" with backtracking" else str" without backtracking")); let secvars = compute_secvars gl in - let poss = - e_possible_resolve hints info.search_hints secvars info.search_only_classes env sigma concl in + match e_possible_resolve hints info.search_hints secvars + info.search_only_classes env sigma concl with + | ModeMismatch -> + Proofview.tclZERO StuckClass + | ModeMatch poss -> (* If no goal depends on the solution of this one or the instances are irrelevant/assumed to be unique, then we don't need to backtrack, as long as no evar appears in the goal @@ -769,9 +784,7 @@ module Search = struct (with_shelf tac >>= fun s -> let i = !idx in incr idx; result s i None) (fun e' -> - if CErrors.noncritical (fst e') then - (pr_error e'; aux (merge_exceptions e e') tl) - else Exninfo.iraise e') + (pr_error e'; aux (merge_exceptions e e') tl)) and aux e = function | x :: xs -> onetac e x xs | [] -> @@ -783,6 +796,7 @@ module Search = struct str" possibilities"); match e with | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx + | (StuckClass,ie) -> Proofview.tclZERO ~info:ie StuckClass | (_,ie) -> Proofview.tclZERO ~info:ie NoApplicableEx in if backtrack then aux (NoApplicableEx,Exninfo.null) poss @@ -841,11 +855,21 @@ module Search = struct begin fun gl -> search_tac_gl mst only_classes dep hints depth (succ i) sigma gls gl end in + let tac_or_stuck sigma gls i = + Proofview.tclOR + (tac sigma gls i) + (function (StuckClass, _) -> + if !typeclasses_debug > 1 then + Feedback.msg_debug + Pp.(str "Proof search got stuck on a constraint, postponing it."); + Proofview.tclUNIT () + | (e, ie) -> Proofview.tclZERO ~info:ie e) + 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))) + (tclDISPATCH (List.init j (fun i -> tac_or_stuck sigma gls i))) let fix_iterative t = let rec aux depth = @@ -864,7 +888,7 @@ module Search = struct | (e,ie) -> Proofview.tclZERO ~info:ie e) in aux 1 - let eauto_tac mst ?(unique=false) + let eauto_tac_stuck mst ?(unique=false) ~only_classes ?strategy ~depth ~dep hints = let open Proofview in let tac = @@ -902,6 +926,37 @@ module Search = struct Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac else tac in + let rec fixpoint step laststuck = + tac <*> + Proofview.tclEVARMAP >>= fun sigma -> + Proofview.Unsafe.tclGETGOALS >>= fun stuck -> + begin + if !typeclasses_debug > 0 then + Feedback.msg_debug Pp.(str "Finished run " ++ int step ++ str " of resolution."); + let stuck = List.map Proofview_monad.drop_state stuck in + let stuckset = Evar.Set.of_list stuck in + let () = + if !typeclasses_debug > 1 then + if Evar.Set.cardinal stuckset > 0 then + Feedback.msg_debug Pp.(str "Stuck goals after resolution: " ++ fnl () ++ + Pp.prlist_with_sep spc (fun ev -> Printer.pr_goal {it = ev; sigma}) stuck) + else Feedback.msg_debug Pp.(str "No stuck goals after resolution.") + in + if Evar.Set.is_empty stuckset then tclUNIT () + else if Evar.Set.equal laststuck stuckset then + begin + if !typeclasses_debug > 1 then Feedback.msg_debug Pp.(str "No progress made."); + tclUNIT () + end + else begin + assert(Evar.Set.subset stuckset laststuck); + (* Progress was made *) + if !typeclasses_debug > 1 then + Feedback.msg_debug Pp.(str "Progress made, restarting resolution on stuck goals."); + fixpoint (succ step) stuckset + end + end + in with_shelf numgoals >>= fun (initshelf, i) -> (if !typeclasses_debug > 1 then Feedback.msg_debug (str"Starting resolution with " ++ int i ++ @@ -910,24 +965,28 @@ module Search = struct (if only_classes then str " in only_classes mode" else str " in regular mode") ++ match depth with None -> str ", unbounded" | Some i -> str ", with depth limit " ++ int i)); - tac + Proofview.Unsafe.tclGETGOALS >>= fun gls -> + let gls = CList.map Proofview.drop_state gls in + fixpoint 1 (Evar.Set.of_list gls) let eauto_tac mst ?unique ~only_classes ?strategy ~depth ~dep hints = - Hints.wrap_hint_warning @@ eauto_tac mst ?unique ~only_classes ?strategy ~depth ~dep hints + Hints.wrap_hint_warning @@ eauto_tac_stuck mst ?unique ~only_classes ?strategy ~depth ~dep hints let run_on_evars env evm p tac = match evars_to_goals p evm with | None -> None (* This happens only because there's no evar having p *) | Some (goals, nongoals) -> - let goals = + let goalsl = if !typeclasses_dependency_order then top_sort evm goals else Evar.Set.elements goals in + let tac = tac <*> Proofview.Unsafe.tclGETGOALS >>= + fun stuck -> Proofview.shelve_goals (List.map Proofview_monad.drop_state stuck) in let evm = Evd.set_typeclass_evars evm Evar.Set.empty in let fgoals = Evd.save_future_goals evm in let _, pv = Proofview.init evm [] in - let pv = Proofview.unshelve goals pv in + let pv = Proofview.unshelve goalsl pv in try (* Instance may try to call this before a proof is set up! Thus, give_me_the_proof will fail. Beware! *) @@ -938,35 +997,35 @@ module Search = struct * with | Proof_global.NoCurrentProof -> *) Id.of_string "instance", false in - let (), pv', (unsafe, shelved, gaveup), _ = - Proofview.apply ~name ~poly env tac pv - in - if not (List.is_empty gaveup) then - CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals."); - if Proofview.finished pv' then + let finish pv' shelved = let evm' = Proofview.return pv' in - assert(Evd.fold_undefined (fun ev _ acc -> - let okev = Evd.mem evm ev || List.mem ev shelved in - if not okev then - Feedback.msg_debug - (str "leaking evar " ++ int (Evar.repr ev) ++ - spc () ++ pr_ev evm' ev); - acc && okev) evm' true); + assert(Evd.fold_undefined (fun ev _ acc -> + let okev = Evd.mem evm ev || List.mem ev shelved in + if not okev then + Feedback.msg_debug + (str "leaking evar " ++ int (Evar.repr ev) ++ + spc () ++ pr_ev evm' ev); + acc && okev) evm' true); let fgoals = Evd.shelve_on_future_goals shelved fgoals in let evm' = Evd.restore_future_goals evm' fgoals in let nongoals' = Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with | Some ev' -> Evar.Set.add ev acc - | None -> acc) nongoals (Evd.get_typeclass_evars evm') + | None -> acc) (Evar.Set.union goals nongoals) (Evd.get_typeclass_evars evm') in let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in let evm' = Evd.set_typeclass_evars evm' nongoals' in - Some evm' - else raise Not_found + Some evm' + in + let (), pv', (unsafe, shelved, gaveup), _ = Proofview.apply ~name ~poly env tac pv in + if not (List.is_empty gaveup) then + CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals."); + if Proofview.finished pv' then finish pv' shelved + else raise Not_found with Logic_monad.TacticFailure _ -> raise Not_found let evars_eauto env evd depth only_classes unique dep mst hints p = - let eauto_tac = eauto_tac mst ~unique ~only_classes ~depth ~dep:(unique || dep) hints in + let eauto_tac = eauto_tac_stuck mst ~unique ~only_classes ~depth ~dep:(unique || dep) hints in let res = run_on_evars env evd p eauto_tac in match res with | None -> evd @@ -996,7 +1055,11 @@ let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full) let modes = List.map Hint_db.modes dbs in let modes = List.fold_left (GlobRef.Map.union (fun _ m1 m2 -> Some (m1@m2))) GlobRef.Map.empty modes in let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in - Search.eauto_tac (modes,st) ~only_classes ?strategy ~depth ~dep:true dbs + Proofview.tclIGNORE + (Search.eauto_tac (modes,st) ~only_classes ?strategy ~depth ~dep:true dbs) + (* Stuck goals can remain here, we could shelve them, but this way + the user can use `solve [typeclasses eauto]` to check there are + no stuck goals remaining, or use [typeclasses eauto; shelve] himself. *) (** We compute dependencies via a union-find algorithm. Beware of the imperative effects on the partition structure, diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index dc94e6a6fb..e26338436d 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,6 +16,7 @@ open EConstr val typeclasses_db : string val catchable : exn -> bool +[@@ocaml.deprecated "Use instead CErrors.noncritical, or the exact name of the exception that matters in the corresponding case."] val set_typeclasses_debug : bool -> unit val get_typeclasses_debug : unit -> bool @@ -66,4 +67,6 @@ module Search : sig -> Hints.hint_db list (** The list of hint databases to use *) -> unit Proofview.tactic + (** Note: there might be stuck goals due to mode declarations + remaining even in case of success of the tactic. *) end diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index c7b6998c8c..d6be714dd9 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index cd05d47193..62e8307fc7 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/declare.ml b/tactics/declare.ml index 5655bdfd4d..de3c731d9b 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/declare.mli b/tactics/declare.mli index 00c1e31717..f87d08fc8b 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/declareScheme.ml b/tactics/declareScheme.ml index 5f4626fcb2..84fa1ee508 100644 --- a/tactics/declareScheme.ml +++ b/tactics/declareScheme.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/declareScheme.mli b/tactics/declareScheme.mli index f2ae5e41c8..5a771009bd 100644 --- a/tactics/declareScheme.mli +++ b/tactics/declareScheme.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/dnet.ml b/tactics/dnet.ml index 389329c19f..b7ebec21d8 100644 --- a/tactics/dnet.ml +++ b/tactics/dnet.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/dnet.mli b/tactics/dnet.mli index a79afb4bf6..3f044708cb 100644 --- a/tactics/dnet.mli +++ b/tactics/dnet.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index aca6b4734a..a89e5ef19a 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -124,7 +124,10 @@ let hintmap_of sigma secvars hdc concl = | None -> fun db -> Hint_db.map_none ~secvars db | Some hdc -> if occur_existential sigma concl then - (fun db -> Hint_db.map_existential sigma ~secvars hdc concl db) + (fun db -> + match Hint_db.map_existential sigma ~secvars hdc concl db with + | ModeMatch l -> l + | ModeMismatch -> []) else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db) (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) diff --git a/tactics/eauto.mli b/tactics/eauto.mli index f9347b7b0f..e6f2c1a8e2 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/elim.ml b/tactics/elim.ml index 379a8d5401..5d8698916f 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/elim.mli b/tactics/elim.mli index 42449be779..e89855a050 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 6cdb24965d..910e042e7a 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index 8e167b171c..eb8e4bf782 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index a82b26f428..6fbd29def9 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/eqdecide.mli b/tactics/eqdecide.mli index cd2039ba56..a53b8644a8 100644 --- a/tactics/eqdecide.mli +++ b/tactics/eqdecide.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 1df56be0be..98da61781e 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index fd4221f7c0..d1038f2655 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 7393454ba9..49645d82a4 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -563,7 +563,7 @@ let apply_special_clear_request clear_flag f = let (sigma, (c, bl)) = f env sigma in apply_clear_request clear_flag (use_clear_hyp_by_default ()) c with - e when catchable_exception e -> tclIDTAC + e when noncritical e -> tclIDTAC end type multi = @@ -1627,10 +1627,9 @@ let try_rewrite tac = Proofview.tclORELSE tac begin function (e, info) -> match e with | Constr_matching.PatternMatchingFailure -> tclZEROMSG (str "Not a primitive equality here.") - | e when catchable_exception e -> + | e -> tclZEROMSG (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.") - | e -> Proofview.tclZERO ~info e end let cutSubstClause l2r eqn cls = diff --git a/tactics/equality.mli b/tactics/equality.mli index a9ccadf53a..e252eeab28 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/genredexpr.ml b/tactics/genredexpr.ml index a65f515ce6..1f6b04c1d3 100644 --- a/tactics/genredexpr.ml +++ b/tactics/genredexpr.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 731792e34e..a907b9e783 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -499,6 +499,10 @@ let rec subst_hints_path subst hp = type hint_db_name = string +type 'a with_mode = + | ModeMatch of 'a + | ModeMismatch + module Hint_db : sig type t @@ -507,9 +511,9 @@ val find : GlobRef.t -> t -> search_entry val map_none : secvars:Id.Pred.t -> t -> full_hint list val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list val map_existential : evar_map -> secvars:Id.Pred.t -> - (GlobRef.t * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode val map_eauto : evar_map -> secvars:Id.Pred.t -> - (GlobRef.t * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode val map_auto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list val add_one : env -> evar_map -> hint_entry -> t -> t @@ -528,7 +532,6 @@ val add_modes : hint_mode array list GlobRef.Map.t -> t -> t val modes : t -> hint_mode array list GlobRef.Map.t val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a - end = struct @@ -618,8 +621,8 @@ struct let map_existential sigma ~secvars (k,args) concl db = let se = find k db in if matches_modes sigma args se.sentry_mode then - merge_entry secvars db se.sentry_nopat se.sentry_pat - else merge_entry secvars db [] [] + ModeMatch (merge_entry secvars db se.sentry_nopat se.sentry_pat) + else ModeMismatch (* [c] contains an existential *) let map_eauto sigma ~secvars (k,args) concl db = @@ -627,8 +630,8 @@ struct if matches_modes sigma args se.sentry_mode then let st = if db.use_dn then Some db.hintdb_state else None in let pat = lookup_tacs sigma concl st se in - merge_entry secvars db [] pat - else merge_entry secvars db [] [] + ModeMatch (merge_entry secvars db [] pat) + else ModeMismatch let is_exact = function | Give_exact _ -> true @@ -923,7 +926,7 @@ let make_resolve_hyp env sigma decl = (c, NamedDecl.get_type decl, Univ.ContextSet.empty)] with | Failure _ -> [] - | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp.") + | e when noncritical e -> anomaly (Pp.str "make_resolve_hyp.") (* REM : in most cases hintname = id *) @@ -1028,7 +1031,7 @@ let remove_hint dbname grs = type hint_action = | CreateDB of bool * TransparentState.t | AddTransparency of evaluable_global_reference hints_transparency_target * bool - | AddHints of hint_entry list + | AddHints of { superglobal : bool; hints : hint_entry list } | RemoveHints of GlobRef.t list | AddCut of hints_path | AddMode of GlobRef.t * hint_mode array @@ -1054,14 +1057,21 @@ let load_autohint _ (kn, h) = match h.hint_action with | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty ~name st b) | AddTransparency (grs, b) -> add_transparency name grs b - | AddHints hints -> add_hint name hints + | AddHints { superglobal; hints } -> + if superglobal then add_hint name hints | RemoveHints grs -> remove_hint name grs | AddCut path -> add_cut name path | AddMode (l, m) -> add_mode name l m let open_autohint i (kn, h) = if Int.equal i 1 then match h.hint_action with - | AddHints hints -> + | AddHints { superglobal; hints } -> + let () = + if not superglobal then + (* Import-bound hints must be declared when not imported yet *) + let filter (_, h) = not @@ KNmap.mem h.code.uid !statustable in + add_hint h.hint_name (List.filter filter hints) + in let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in List.iter add hints | _ -> () @@ -1130,9 +1140,9 @@ let subst_autohint (subst, obj) = else HintsReferences grs' in if target' == target then obj.hint_action else AddTransparency (target', b) - | AddHints hintlist -> - let hintlist' = List.Smart.map subst_hint hintlist in - if hintlist' == hintlist then obj.hint_action else AddHints hintlist' + | AddHints { superglobal; hints } -> + let hints' = List.Smart.map subst_hint hints in + if hints' == hints then obj.hint_action else AddHints { superglobal; hints = hints' } | RemoveHints grs -> let grs' = List.Smart.map (subst_global_reference subst) grs in if grs == grs' then obj.hint_action else RemoveHints grs' @@ -1147,7 +1157,7 @@ let subst_autohint (subst, obj) = let classify_autohint obj = match obj.hint_action with - | AddHints [] -> Dispose + | AddHints { hints = [] } -> Dispose | _ -> if obj.hint_local then Dispose else Substitute obj let inAutoHint : hint_obj -> obj = @@ -1179,7 +1189,13 @@ let remove_hints local dbnames grs = (**************************************************************************) (* The "Hint" vernacular command *) (**************************************************************************) -let add_resolves env sigma clist local dbnames = + +let check_no_export ~local ~superglobal () = + (* TODO: implement export for these entries *) + if not local && not superglobal then + CErrors.user_err Pp.(str "This command does not support the \"export\" attribute") + +let add_resolves env sigma clist ~local ~superglobal dbnames = List.iter (fun dbname -> let r = @@ -1187,25 +1203,27 @@ let add_resolves env sigma clist local dbnames = make_resolves env sigma (true,hnf,not !Flags.quiet) pri ~poly ~name:path gr) clist) in - let hint = make_hint ~local dbname (AddHints r) in + let hint = make_hint ~local dbname (AddHints { superglobal; hints = r }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_unfolds l local dbnames = +let add_unfolds l ~local ~superglobal dbnames = List.iter (fun dbname -> - let hint = make_hint ~local dbname (AddHints (List.map make_unfold l)) in + let hint = make_hint ~local dbname (AddHints { superglobal; hints = List.map make_unfold l }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_cuts l local dbnames = +let add_cuts l ~local ~superglobal dbnames = + let () = check_no_export ~local ~superglobal () in List.iter (fun dbname -> let hint = make_hint ~local dbname (AddCut l) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_mode l m local dbnames = +let add_mode l m ~local ~superglobal dbnames = + let () = check_no_export ~local ~superglobal () in List.iter (fun dbname -> let m' = make_mode l m in @@ -1213,30 +1231,31 @@ let add_mode l m local dbnames = Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_transparency l b local dbnames = +let add_transparency l b ~local ~superglobal dbnames = + let () = check_no_export ~local ~superglobal () in List.iter (fun dbname -> let hint = make_hint ~local dbname (AddTransparency (l, b)) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_extern info tacast local dbname = +let add_extern info tacast ~local ~superglobal dbname = let pat = match info.hint_pattern with | None -> None | Some (_, pat) -> Some pat in let hint = make_hint ~local dbname - (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in + (AddHints { superglobal; hints = [make_extern (Option.get info.hint_priority) pat tacast] }) in Lib.add_anonymous_leaf (inAutoHint hint) -let add_externs info tacast local dbnames = - List.iter (add_extern info tacast local) dbnames +let add_externs info tacast ~local ~superglobal dbnames = + List.iter (add_extern info tacast ~local ~superglobal) dbnames -let add_trivials env sigma l local dbnames = +let add_trivials env sigma l ~local ~superglobal dbnames = List.iter (fun dbname -> let l = List.map (fun (name, poly, c) -> make_trivial env sigma poly ~name c) l in - let hint = make_hint ~local dbname (AddHints l) in + let hint = make_hint ~local dbname (AddHints { superglobal; hints = l }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames @@ -1400,22 +1419,27 @@ let interp_hints ~poly = let _, tacexp = Genintern.generic_intern env tacexp in HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp) -let add_hints ~local dbnames h = +let add_hints ~locality dbnames h = + let local, superglobal = match locality with + | Goptions.OptDefault | Goptions.OptGlobal -> false, true + | Goptions.OptExport -> false, false + | Goptions.OptLocal -> true, false + in if String.List.mem "nocore" dbnames then user_err Pp.(str "The hint database \"nocore\" is meant to stay empty."); assert (not (List.is_empty dbnames)); let env = Global.env() in let sigma = Evd.from_env env in match h with - | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames - | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames - | HintsCutEntry lhints -> add_cuts lhints local dbnames - | HintsModeEntry (l,m) -> add_mode l m local dbnames - | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames + | HintsResolveEntry lhints -> add_resolves env sigma lhints ~local ~superglobal dbnames + | HintsImmediateEntry lhints -> add_trivials env sigma lhints ~local ~superglobal dbnames + | HintsCutEntry lhints -> add_cuts lhints ~local ~superglobal dbnames + | HintsModeEntry (l,m) -> add_mode l m ~local ~superglobal dbnames + | HintsUnfoldEntry lhints -> add_unfolds lhints ~local ~superglobal dbnames | HintsTransparencyEntry (lhints, b) -> - add_transparency lhints b local dbnames + add_transparency lhints b ~local ~superglobal dbnames | HintsExternEntry (info, tacexp) -> - add_externs info tacexp local dbnames + add_externs info tacexp ~local ~superglobal dbnames let expand_constructor_hints env sigma lems = List.map_append (fun (evd,lem) -> @@ -1519,7 +1543,9 @@ let pr_hint_term env sigma cl = let fn = try let hdc = decompose_app_bound sigma cl in if occur_existential sigma cl then - Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl + (fun db -> match Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl db with + | ModeMatch l -> l + | ModeMismatch -> []) else Hint_db.map_auto sigma ~secvars:Id.Pred.full hdc cl with Bound -> Hint_db.map_none ~secvars:Id.Pred.full in diff --git a/tactics/hints.mli b/tactics/hints.mli index 7bb17489bf..9e11931247 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -125,6 +125,10 @@ val glob_hints_path_atom : val glob_hints_path : Libnames.qualid hints_path_gen -> GlobRef.t hints_path_gen +type 'a with_mode = + | ModeMatch of 'a + | ModeMismatch + module Hint_db : sig type t @@ -140,16 +144,20 @@ module Hint_db : val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the - arguments, _not_ using the discrimination net. *) + arguments, _not_ using the discrimination net. + Returns a [ModeMismatch] if there are declared modes and none matches. + *) val map_existential : evar_map -> secvars:Id.Pred.t -> - (GlobRef.t * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode (** All hints associated to the reference, respecting modes if evars appear in the - arguments and using the discrimination net. *) - val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list + arguments and using the discrimination net. + Returns a [ModeMismatch] if there are declared modes and none matches. *) + val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode - (** All hints associated to the reference, respecting modes if evars appear in the - arguments. *) + (** All hints associated to the reference. + Precondition: no evars should appear in the arguments, so no modes + are checked. *) val map_auto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list @@ -211,7 +219,7 @@ val current_pure_db : unit -> hint_db list val interp_hints : poly:bool -> hints_expr -> hints_entry -val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit +val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit val prepare_hint : bool (* Check no remaining evars *) -> env -> evar_map -> evar_map * constr -> (constr * Univ.ContextSet.t) diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 5404404af5..76b1c94759 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 0000f81d3f..0a1a0b9312 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 517ccfaf53..8336fae02f 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index d886fb67d3..dad2036c64 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/inv.ml b/tactics/inv.ml index 4239fc8bc0..4b94dd0e72 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/inv.mli b/tactics/inv.mli index a053b18eed..e62b2734ca 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index def4af1ae8..5a8ec404ee 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 41f83d3888..5a5de7b58f 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index a7ba12bb1f..438892e75e 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli index a2e742c0d7..3cf3a13262 100644 --- a/tactics/pfedit.mli +++ b/tactics/pfedit.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index 4c470519d6..7d59a18494 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index 9161eae82f..8c1bc0def1 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index a30c877435..250c80d9a5 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli index a7e39fb7b4..d43785218f 100644 --- a/tactics/redexpr.mli +++ b/tactics/redexpr.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/redops.ml b/tactics/redops.ml index 86ed8f8899..bc846681c9 100644 --- a/tactics/redops.ml +++ b/tactics/redops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/redops.mli b/tactics/redops.mli index 964e80e5ab..fe64c9b032 100644 --- a/tactics/redops.mli +++ b/tactics/redops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 58d2097dea..8f6844079b 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 5fde6d2178..9ec558f1ad 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ef50c56dc4..30ca024a2f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -853,7 +853,7 @@ let change_on_subterm ~check cv_pb deep t where env sigma c = let sigma = if !mayneedglobalcheck then begin try fst (Typing.type_of env sigma c) - with e when catchable_exception e -> + with e when noncritical e -> error "Replacement would lead to an ill-typed term." end else sigma in @@ -1313,7 +1313,7 @@ let cut c = (* Backward compat: ensure that [c] is well-typed. Plus we need to know the relevance *) match Typing.sort_of env sigma c with - | exception e when Pretype_errors.precatchable_exception e -> + | exception e when noncritical e -> Tacticals.New.tclZEROMSG (str "Not a proposition or a type.") | sigma, s -> let r = Sorts.relevance_of_sort s in @@ -1717,7 +1717,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars if n<0 then error "Applied theorem does not have enough premises."; let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause ~with_evars ~flags - with exn when catchable_exception exn -> + with exn when noncritical exn -> Proofview.tclZERO exn in let rec try_red_apply thm_ty (exn0, info) = @@ -1818,7 +1818,7 @@ let apply_list = function let find_matching_clause unifier clause = let rec find clause = try unifier clause - with e when catchable_exception e -> + with e when noncritical e -> try find (clenv_push_prod clause) with NotExtensibleClause -> failwith "Cannot apply" in find clause @@ -4486,7 +4486,7 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ = error "Need a fully applied argument."; (* We lose the possibility of coercions in with-bindings *) pose_all_metas_as_evars env indclause.evd (clenv_value indclause) - with e when catchable_exception e -> + with e when noncritical e -> try find_clause (try_red_product env sigma typ) with Redelimination -> raise e in find_clause typ @@ -5041,7 +5041,7 @@ let unify ?(state=TransparentState.full) x y = in let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in Proofview.Unsafe.tclEVARS sigma - with e when CErrors.noncritical e -> + with e when noncritical e -> Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None))) end diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 308399c5db..c84ba17f23 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 7f2a6f94b5..553eb903fa 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli index 625a97fdb9..bfbb59f72c 100644 --- a/tactics/term_dnet.mli +++ b/tactics/term_dnet.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |