diff options
Diffstat (limited to 'tactics')
55 files changed, 753 insertions, 630 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 1e18028e7b..e85d94cd72 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 *) @@ -91,14 +91,14 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in let ectx = Evd.evar_universe_context sigma in let (const, safe, ectx) = - try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ectx secsign concl solve_tac + try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ~uctx:ectx ~sign:secsign concl solve_tac with Logic_monad.TacticFailure e as src -> (* if the tactic [tac] fails, it reports a [TacticFailure e], which is an error irrelevant to the proof system (in fact it means that [e] comes from [tac] failing to yield enough success). Hence it reraises [e]. *) - let (_, info) = CErrors.push src in - iraise (e, info) + let (_, info) = Exninfo.capture src in + Exninfo.iraise (e, info) in let body, effs = Future.force const.Declare.proof_entry_body in (* We drop the side-effects from the entry, they already exist in the ambient environment *) 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 9c1a975330..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 *) @@ -177,7 +177,6 @@ let global_info_auto = ref false let add_option ls refe = Goptions.(declare_bool_option { optdepr = false; - optname = String.concat " " ls; optkey = ls; optread = (fun () -> !refe); optwrite = (:=) refe }) @@ -304,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 @@ -367,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 cd6f445503..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 *) @@ -238,7 +238,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = in try let others,(c1,c2) = split_last_two args in - let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in + let ty1, ty2 = Retyping.get_type_of env eqclause.evd c1, Retyping.get_type_of env eqclause.evd c2 in (* XXX: It looks like mk_clenv_from_env should be fixed instead? *) let open EConstr in let hyp_ty = Unsafe.to_constr ty in @@ -261,7 +261,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = | None -> None let find_applied_relation ?loc metas env sigma c left2right = - let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in + let ctype = Retyping.get_type_of env sigma (EConstr.of_constr c) in match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> 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 f8cb8870ea..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 *) @@ -83,8 +83,6 @@ open Goptions let () = declare_bool_option { optdepr = false; - optname = "do typeclass search avoiding eta-expansions " ^ - " in proof terms (expensive)"; optkey = ["Typeclasses";"Limit";"Intros"]; optread = get_typeclasses_limit_intros; optwrite = set_typeclasses_limit_intros; } @@ -92,7 +90,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "during typeclass resolution, solve instances according to their dependency order"; optkey = ["Typeclasses";"Dependency";"Order"]; optread = get_typeclasses_dependency_order; optwrite = set_typeclasses_dependency_order; } @@ -100,7 +97,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "use iterative deepening strategy"; optkey = ["Typeclasses";"Iterative";"Deepening"]; optread = get_typeclasses_iterative_deepening; optwrite = set_typeclasses_iterative_deepening; } @@ -108,7 +104,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "compat"; optkey = ["Typeclasses";"Filtered";"Unification"]; optread = get_typeclasses_filtered_unification; optwrite = set_typeclasses_filtered_unification; } @@ -116,7 +111,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "debug output for typeclasses proof search"; optkey = ["Typeclasses";"Debug"]; optread = get_typeclasses_debug; optwrite = set_typeclasses_debug; } @@ -124,7 +118,6 @@ let () = let _ = declare_int_option { optdepr = false; - optname = "verbosity of debug output for typeclasses proof search"; optkey = ["Typeclasses";"Debug";"Verbosity"]; optread = get_typeclasses_verbose; optwrite = set_typeclasses_verbose; } @@ -132,7 +125,6 @@ let _ = let () = declare_int_option { optdepr = false; - optname = "depth for typeclasses proof search"; optkey = ["Typeclasses";"Depth"]; optread = get_typeclasses_depth; optwrite = set_typeclasses_depth; } @@ -197,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 @@ -242,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") - | _ -> 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. @@ -317,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 = @@ -370,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 @@ -436,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 = @@ -536,9 +539,10 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = let hints = build_subclasses ~check:false env sigma (GlobRef.VarRef id) empty_hint_info in (List.map_append (fun (path,info,c) -> + let h = IsConstr (EConstr.of_constr c,Univ.ContextSet.empty) [@ocaml.warning "-3"] in make_resolves env sigma ~name:(PathHints path) (true,false,not !Flags.quiet) info ~poly:false - (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty))) + h) hints) else [] in @@ -613,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, @@ -651,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 @@ -776,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 iraise e') + (pr_error e'; aux (merge_exceptions e e') tl)) and aux e = function | x :: xs -> onetac e x xs | [] -> @@ -790,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 @@ -848,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 = @@ -871,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 = @@ -909,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 ++ @@ -917,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! *) @@ -945,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 @@ -1003,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, @@ -1202,10 +1258,9 @@ let autoapply c i = in let flags = auto_unif_flags (Hints.Hint_db.transparent_state hintdb) in - let cty = Tacmach.New.pf_unsafe_type_of gl c in + let cty = Tacmach.New.pf_get_type_of gl c in let ce = mk_clenv_from gl (c,cty) in - unify_e_resolve false flags gl - ((c,cty,Univ.ContextSet.empty),0,ce) <*> + unify_e_resolve false flags gl ((c,cty,Univ.ContextSet.empty),0,ce) <*> Proofview.tclEVARMAP >>= (fun sigma -> let sigma = Typeclasses.make_unresolvables (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in 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 1f5a6380fd..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 *) @@ -110,8 +110,7 @@ let contradiction_term (c,lbind as cl) = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let type_of = Tacmach.New.pf_unsafe_type_of gl in - let typ = type_of c in + let typ = Tacmach.New.pf_get_type_of gl c in let _, ccl = splay_prod env sigma typ in if is_empty_type env sigma ccl then Tacticals.New.tclTHEN 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 da4de3df77..5e6f78be6f 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 *) @@ -24,10 +24,11 @@ exception AlreadyDeclared of (string option * Id.t) let _ = CErrors.register_handler (function | AlreadyDeclared (kind, id) -> - seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind - ; Id.print id; str " already exists."] + Some + (seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind + ; Id.print id; str " already exists."]) | _ -> - raise CErrors.Unhandled) + None) module NamedDecl = Context.Named.Declaration @@ -130,8 +131,8 @@ let dummy_constant cst = { let classify_constant cst = Substitute (dummy_constant cst) -let (inConstant : constant_obj -> obj) = - declare_object { (default_object "CONSTANT") with +let (objConstant : constant_obj Libobject.Dyn.tag) = + declare_object_full { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; open_function = open_constant; @@ -139,6 +140,8 @@ let (inConstant : constant_obj -> obj) = subst_function = ident_subst_function; discharge_function = discharge_constant } +let inConstant v = Libobject.Dyn.Easy.inj v objConstant + let update_tables c = Impargs.declare_constant_implicits c; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c) @@ -158,6 +161,18 @@ let register_side_effect (c, role) = | None -> () | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|] +let get_roles export eff = + let map c = + let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in + (c, role) + in + List.map map export + +let export_side_effects eff = + let export = Global.export_private_constants eff.Evd.seff_private in + let export = get_roles export eff in + List.iter register_side_effect export + let record_aux env s_ty s_bo = let open Environ in let in_ty = keep_hyps env s_ty in @@ -276,13 +291,6 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo opaque_entry_universes = univs; } -let get_roles export eff = - let map c = - let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in - (c, role) - in - List.map map export - let feedback_axiom () = Feedback.(feedback AddedAxiom) let is_unsafe_typing_flags () = @@ -291,37 +299,36 @@ let is_unsafe_typing_flags () = let define_constant ~name cd = (* Logically define the constant and its subproofs, no libobject tampering *) - let export, decl, unsafe = match cd with - | DefinitionEntry de -> - (* We deal with side effects *) - if not de.proof_entry_opaque then - (* This globally defines the side-effects in the environment. *) - let body, eff = Future.force de.proof_entry_body in - let body, export = Global.export_private_constants (body, eff.Evd.seff_private) in - let export = get_roles export eff in - let de = { de with proof_entry_body = Future.from_val (body, ()) } in - let cd = Entries.DefinitionEntry (cast_proof_entry de) in - export, ConstantEntry cd, false - else - let map (body, eff) = body, eff.Evd.seff_private in - let body = Future.chain de.proof_entry_body map in - let de = { de with proof_entry_body = body } in - let de = cast_opaque_proof_entry EffectEntry de in - [], OpaqueEntry de, false - | ParameterEntry e -> - [], ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict()) - | PrimitiveEntry e -> - [], ConstantEntry (Entries.PrimitiveEntry e), false + let decl, unsafe = match cd with + | DefinitionEntry de -> + (* We deal with side effects *) + if not de.proof_entry_opaque then + let body, eff = Future.force de.proof_entry_body in + (* This globally defines the side-effects in the environment + and registers their libobjects. *) + let () = export_side_effects eff in + let de = { de with proof_entry_body = Future.from_val (body, ()) } in + let cd = Entries.DefinitionEntry (cast_proof_entry de) in + ConstantEntry cd, false + else + let map (body, eff) = body, eff.Evd.seff_private in + let body = Future.chain de.proof_entry_body map in + let de = { de with proof_entry_body = body } in + let de = cast_opaque_proof_entry EffectEntry de in + OpaqueEntry de, false + | ParameterEntry e -> + ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict()) + | PrimitiveEntry e -> + ConstantEntry (Entries.PrimitiveEntry e), false in let kn = Global.add_constant name decl in if unsafe || is_unsafe_typing_flags() then feedback_axiom(); - kn, export + kn let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = let () = check_exists name in - let kn, export = define_constant ~name cd in - (* Register the libobjects attached to the constants and its subproofs *) - let () = List.iter register_side_effect export in + let kn = define_constant ~name cd in + (* Register the libobjects attached to the constants *) let () = register_constant kn kind local in kn @@ -344,11 +351,11 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff -let inline_private_constants ~univs env ce = +let inline_private_constants ~uctx env ce = let body, eff = Future.force ce.proof_entry_body in let cb, ctx = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in - let univs = UState.merge ~sideff:true Evd.univ_rigid univs ctx in - cb, univs + let uctx = UState.merge ~sideff:true Evd.univ_rigid uctx ctx in + cb, uctx (** Declaration of section variables and local definitions *) type variable_declaration = @@ -357,12 +364,14 @@ type variable_declaration = (* This object is only for things which iterate over objects to find variables (only Prettyp.print_context AFAICT) *) -let inVariable : unit -> obj = - declare_object { (default_object "VARIABLE") with +let objVariable : unit Libobject.Dyn.tag = + declare_object_full { (default_object "VARIABLE") with classify_function = (fun () -> Dispose)} +let inVariable v = Libobject.Dyn.Easy.inj v objVariable + let declare_variable ~name ~kind d = - (* Constr raisonne sur les noms courts *) + (* Variables are distinguished by only short names *) if Decls.variable_exists name then raise (AlreadyDeclared (None, name)); @@ -373,15 +382,13 @@ let declare_variable ~name ~kind d = | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) - let (body, eff) = Future.force de.proof_entry_body in - let ((body, uctx), export) = Global.export_private_constants (body, eff.Evd.seff_private) in - let eff = get_roles export eff in - let () = List.iter register_side_effect eff in - let poly, univs = match de.proof_entry_universes with + let ((body, body_ui), eff) = Future.force de.proof_entry_body in + let () = export_side_effects eff in + let poly, entry_ui = match de.proof_entry_universes with | Monomorphic_entry uctx -> false, uctx | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in - let univs = Univ.ContextSet.union uctx univs in + let univs = Univ.ContextSet.union body_ui entry_ui in (* We must declare the universe constraints before type-checking the term. *) let () = declare_universe_context ~poly univs in @@ -497,4 +504,9 @@ module Internal = struct ; proof_entry_type = Some typ }, args + type nonrec constant_obj = constant_obj + + let objVariable = objVariable + let objConstant = objConstant + end diff --git a/tactics/declare.mli b/tactics/declare.mli index c646d2f85b..0068b9842a 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 *) @@ -108,11 +108,11 @@ val declare_private_constant -> unit proof_entry -> Constant.t * Evd.side_effects -(** [inline_private_constants ~sideff ~univs env ce] will inline the +(** [inline_private_constants ~sideff ~uctx env ce] will inline the constants in [ce]'s body and return the body plus the updated [UState.t]. *) val inline_private_constants - : univs:UState.t + : uctx:UState.t -> Environ.env -> Evd.side_effects proof_entry -> Constr.t * UState.t @@ -131,7 +131,8 @@ val check_exists : Id.t -> unit (* Used outside this module only in indschemes *) exception AlreadyDeclared of (string option * Id.t) -(* For legacy support, do not use *) +(** {6 For legacy support, do not use} *) + module Internal : sig val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry @@ -145,4 +146,9 @@ module Internal : sig val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list + type constant_obj + + val objConstant : constant_obj Libobject.Dyn.tag + val objVariable : unit Libobject.Dyn.tag + end 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 361215bf38..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 *) @@ -32,11 +32,13 @@ let eauto_unif_flags = auto_flags_of_state TransparentState.full let e_give_exact ?(flags=eauto_unif_flags) c = Proofview.Goal.enter begin fun gl -> - let t1 = Tacmach.New.pf_unsafe_type_of gl c in + let sigma, t1 = Tacmach.New.pf_type_of gl c in let t2 = Tacmach.New.pf_concl gl in - let sigma = Tacmach.New.project gl in if occur_existential sigma t1 || occur_existential sigma t2 then - Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) + Tacticals.New.tclTHENLIST + [Proofview.Unsafe.tclEVARS sigma; + Clenvtac.unify ~flags t1; + exact_no_check c] else exact_check c end @@ -122,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) *) @@ -233,7 +238,7 @@ module SearchProblem = struct (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) (lgls, cost, pptac) :: aux tacl with e when CErrors.noncritical e -> - let e = CErrors.push e in + let e = Exninfo.capture e in Refiner.catch_failerror e; aux tacl in aux l @@ -329,7 +334,6 @@ let global_info_eauto = ref false let () = Goptions.(declare_bool_option { optdepr = false; - optname = "Debug Eauto"; optkey = ["Debug";"Eauto"]; optread = (fun () -> !global_debug_eauto); optwrite = (:=) global_debug_eauto }) @@ -337,7 +341,6 @@ let () = let () = Goptions.(declare_bool_option { optdepr = false; - optname = "Info Eauto"; optkey = ["Info";"Eauto"]; optread = (fun () -> !global_info_eauto); optwrite = (:=) global_info_eauto }) 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 ea61b8e4df..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 *) @@ -80,14 +80,11 @@ let up_to_delta = ref false (* true *) let general_decompose recognizer c = Proofview.Goal.enter begin fun gl -> - let type_of = pf_unsafe_type_of gl in - let env = pf_env gl in - let sigma = project gl in - let typc = type_of c in + let typc = pf_get_type_of gl c in tclTHENS (cut typc) [ tclTHEN (intro_using tmphyp_name) (onLastHypId - (ifOnHyp (recognizer env sigma) (general_decompose_aux (recognizer env sigma)) + (ifOnHyp recognizer (general_decompose_aux recognizer) (fun id -> clear [id]))); exact_no_check c ] end @@ -136,7 +133,7 @@ let induction_trailer abs_i abs_j bargs = (onLastHypId (fun id -> Proofview.Goal.enter begin fun gl -> - let idty = pf_unsafe_type_of gl (mkVar id) in + let idty = pf_get_type_of gl (mkVar id) in let fvty = global_vars (pf_env gl) (project gl) idty in let possible_bring_hyps = (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums 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 d6fda00ad8..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 *) @@ -49,14 +49,14 @@ let optimize_non_type_induction_scheme kind dep sort ind = let sigma = Evd.minimize_universes sigma in (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma) else - let sigma, pind = Evd.fresh_inductive_instance env sigma ind in + let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in (c, Evd.evar_universe_context sigma) let build_induction_scheme_in_type dep sort ind = let env = Global.env () in let sigma = Evd.from_env env in - let sigma, pind = Evd.fresh_inductive_instance env sigma ind in + let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in c, Evd.evar_universe_context sigma 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 bdfd200988..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 *) @@ -195,13 +195,13 @@ let rec solveArg hyps eqonleft mk largs rargs = match largs, rargs with ] | a1 :: largs, a2 :: rargs -> Proofview.Goal.enter begin fun gl -> - let rectype = pf_unsafe_type_of gl a1 in + let sigma, rectype = pf_type_of gl a1 in let decide = mk rectype a1 a2 in let tac hyp = solveArg (hyp :: hyps) eqonleft mk largs rargs in let subtacs = if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto] else [diseqCase hyps eqonleft;eqCase tac;default_auto] in - (tclTHENS (elim_type decide) subtacs) + tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENS (elim_type decide) subtacs) end | _ -> invalid_arg "List.fold_right2" @@ -274,11 +274,12 @@ let compare c1 c2 = pf_constr_of_global (lib_ref "core.eq.type") >>= fun eqc -> pf_constr_of_global (lib_ref "core.not.type") >>= fun notc -> Proofview.Goal.enter begin fun gl -> - let rectype = pf_unsafe_type_of gl c1 in + let sigma, rectype = pf_type_of gl c1 in let ops = (opc,eqc,notc) in let decide = mkDecideEqGoal true ops rectype c1 c2 in - (tclTHENS (cut decide) - [(tclTHEN intro - (tclTHEN (onLastHyp simplest_case) clear_last)); - decideEquality rectype ops]) + tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (tclTHENS (cut decide) + [(tclTHEN intro + (tclTHEN (onLastHyp simplest_case) clear_last)); + decideEquality rectype ops]) end 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 96b61b6994..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 *) @@ -72,7 +72,6 @@ let use_injection_in_context = function let () = declare_bool_option { optdepr = false; - optname = "injection in context"; optkey = ["Structural";"Injection"]; optread = (fun () -> !injection_in_context) ; optwrite = (fun b -> injection_in_context := b) } @@ -356,7 +355,7 @@ let find_elim hdcncl lft2rgt dep cls ot = Proofview.Goal.enter_one begin fun gl -> let sigma = project gl in let is_global_exists gr c = - Coqlib.has_ref gr && Termops.is_global sigma (Coqlib.lib_ref gr) c + Coqlib.has_ref gr && isRefX sigma (Coqlib.lib_ref gr) c in let inccl = Option.is_empty cls in let env = Proofview.Goal.env gl in @@ -564,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 = @@ -734,7 +733,6 @@ let keep_proof_equalities_for_injection = ref false let () = declare_bool_option { optdepr = false; - optname = "injection on prop arguments"; optkey = ["Keep";"Proof";"Equalities"]; optread = (fun () -> !keep_proof_equalities_for_injection) ; optwrite = (fun b -> keep_proof_equalities_for_injection := b) } @@ -1062,14 +1060,14 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let onEquality with_evars tac (c,lbindc) = Proofview.Goal.enter begin fun gl -> - let type_of = pf_unsafe_type_of gl in let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in - let t = type_of c in + let t = pf_get_type_of gl c in let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in let eqn = clenv_type eq_clause' in - let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in + (* FIXME evar leak *) + let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) (tac (eq,eqn,eq_args) eq_clause') @@ -1165,7 +1163,7 @@ let minimal_free_rels_rec env sigma = let rec minimalrec_free_rels_rec prev_rels (c,cty) = let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in let combined_rels = Int.Set.union prev_rels direct_rels in - let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i))) + let folder rels i = snd (minimalrec_free_rels_rec rels (c, get_type_of env sigma (mkRel i))) in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels))) in minimalrec_free_rels_rec Int.Set.empty @@ -1210,7 +1208,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let rec sigrec_clausal_form sigma siglen p_i = if Int.equal siglen 0 then (* is the default value typable with the expected type *) - let dflt_typ = unsafe_type_of env sigma dflt in + let sigma, dflt_typ = type_of env sigma dflt in try let sigma = Evarconv.unify_leq_delay env sigma dflt_typ p_i in let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in @@ -1224,29 +1222,21 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let sigma, ev = Evarutil.new_evar env sigma a in let rty = beta_applist sigma (p_i_minus_1,[ev]) in let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in - let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in - match evopt with - | Some w -> - let w_type = unsafe_type_of env sigma w in - begin match Evarconv.unify_leq_delay env sigma w_type a with - | sigma -> - let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in - sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) - | exception Evarconv.UnableToUnify _ -> - user_err Pp.(str "Cannot solve a unification problem.") - end - | None -> - (* This at least happens if what has been detected as a - dependency is not one; use an evasive error message; - even if the problem is upwards: unification should be - tried in the first place in make_iterated_tuple instead - of approximatively computing the free rels; then - unsolved evars would mean not binding rel *) - user_err Pp.(str "Cannot solve a unification problem.") + if EConstr.isEvar sigma ev then + (* This at least happens if what has been detected as a + dependency is not one; use an evasive error message; + even if the problem is upwards: unification should be + tried in the first place in make_iterated_tuple instead + of approximatively computing the free rels; then + unsolved evars would mean not binding rel *) + user_err Pp.(str "Cannot solve a unification problem.") + else + let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in + sigma, applist(exist_term,[a;p_i_minus_1;ev;tuple_tail]) in let sigma = Evd.clear_metas sigma in let sigma, scf = sigrec_clausal_form sigma siglen ty in - sigma, Evarutil.nf_evar sigma scf + sigma, Evarutil.nf_evar sigma scf (* The problem is to build a destructor (a generalization of the predecessor) which, when applied to a term made of constructors @@ -1319,7 +1309,7 @@ let make_iterated_tuple env sigma dflt (z,zty) = sigma, (tuple,tuplety,dfltval) let rec build_injrec env sigma dflt c = function - | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c) + | [] -> make_iterated_tuple env sigma dflt (c,get_type_of env sigma c) | ((sp,cnum),argnum)::l -> try let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in @@ -1341,17 +1331,17 @@ let inject_if_homogenous_dependent_pair ty = Proofview.Goal.enter begin fun gl -> try let sigma = Tacmach.New.project gl in - let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in + let eq,u,(t,t1,t2) = pf_apply find_this_eq_data_decompose gl ty in (* fetch the informations of the pair *) let sigTconstr = Coqlib.(lib_ref "core.sigT.type") in let existTconstr = Coqlib.lib_ref "core.sigT.intro" in (* check whether the equality deals with dep pairs or not *) let eqTypeDest = fst (decompose_app sigma t) in - if not (Termops.is_global sigma sigTconstr eqTypeDest) then raise Exit; + if not (isRefX sigma sigTconstr eqTypeDest) then raise Exit; let hd1,ar1 = decompose_app_vect sigma t1 and hd2,ar2 = decompose_app_vect sigma t2 in - if not (Termops.is_global sigma existTconstr hd1) then raise Exit; - if not (Termops.is_global sigma existTconstr hd2) then raise Exit; + if not (isRefX sigma existTconstr hd1) then raise Exit; + if not (isRefX sigma existTconstr hd2) then raise Exit; let (ind, _), _ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in (* check if the user has declared the dec principle *) (* and compare the fst arguments of the dep pair *) @@ -1360,7 +1350,7 @@ let inject_if_homogenous_dependent_pair ty = if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind && pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit; check_required_library ["Coq";"Logic";"Eqdep_dec"]; - let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in + let new_eq_args = [|pf_get_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in let inj2 = lib_ref "core.eqdep_dec.inj_pair2" in let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in (* cut with the good equality and prove the requested goal *) @@ -1603,7 +1593,7 @@ let cutSubstInConcl l2r eqn = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in + let (lbeq,u,(t,e1,e2)) = pf_apply find_eq_data_decompose gl eqn in let typ = pf_concl gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in @@ -1620,7 +1610,7 @@ let cutSubstInHyp l2r eqn id = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in + let (lbeq,u,(t,e1,e2)) = pf_apply find_eq_data_decompose gl eqn in let typ = pf_get_hyp_typ id gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in @@ -1637,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 = @@ -1694,14 +1683,13 @@ let regular_subst_tactic = ref true let () = declare_bool_option { optdepr = false; - optname = "more regular behavior of tactic subst"; optkey = ["Regular";"Subst";"Tactic"]; optread = (fun () -> !regular_subst_tactic); optwrite = (:=) regular_subst_tactic } let restrict_to_eq_and_identity eq = (* compatibility *) - if not (is_global (lib_ref "core.eq.type") eq) && - not (is_global (lib_ref "core.identity.type") eq) + if not (Constr.isRefX (lib_ref "core.eq.type") eq) && + not (Constr.isRefX (lib_ref "core.identity.type") eq) then raise Constr_matching.PatternMatchingFailure exception FoundHyp of (Id.t * constr * bool) @@ -1715,7 +1703,7 @@ let is_eq_x gl x d = | _ -> false in let c = pf_nf_evar gl (NamedDecl.get_type d) in - let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in + let (_,lhs,rhs) = pi3 (pf_apply find_eq_data_decompose gl c) in if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true)); if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false)) with Constr_matching.PatternMatchingFailure -> @@ -1812,7 +1800,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let find_equations gl = let env = Proofview.Goal.env gl in let sigma = project gl in - let find_eq_data_decompose = find_eq_data_decompose gl in + let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in let select_equation_name decl = try let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in @@ -1837,7 +1825,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = Proofview.Goal.enter begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in - let find_eq_data_decompose = find_eq_data_decompose gl in + let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in let c = pf_get_hyp hyp gl |> NamedDecl.get_type in let _,_,(_,x,y) = find_eq_data_decompose c in (* J.F.: added to prevent failure on goal containing x=x as an hyp *) @@ -1863,7 +1851,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let-ins *) Proofview.Goal.enter begin fun gl -> let sigma = project gl in - let find_eq_data_decompose = find_eq_data_decompose gl in + let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in let test (_,c) = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in @@ -1887,19 +1875,19 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let cond_eq_term_left c t gl = try - let (_,x,_) = pi3 (find_eq_data_decompose gl t) in + let (_,x,_) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then true else failwith "not convertible" with Constr_matching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term_right c t gl = try - let (_,_,x) = pi3 (find_eq_data_decompose gl t) in + let (_,_,x) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then false else failwith "not convertible" with Constr_matching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term c t gl = try - let (_,x,y) = pi3 (find_eq_data_decompose gl t) in + let (_,x,y) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then true else if pf_conv_x gl c y then false else failwith "not convertible" 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 7b3797119a..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 *) @@ -26,7 +26,6 @@ open Libnames open Smartlocate open Termops open Inductiveops -open Typing open Typeclasses open Pattern open Patternops @@ -206,7 +205,6 @@ let write_warn_hint = function let () = Goptions.(declare_string_option { optdepr = false; - optname = "behavior of non-imported hints"; optkey = ["Loose"; "Hint"; "Behavior"]; optread = read_warn_hint; optwrite = write_warn_hint; @@ -501,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 @@ -509,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 @@ -530,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 @@ -620,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 = @@ -629,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 @@ -925,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 *) @@ -966,16 +967,17 @@ let make_mode ref m = let make_trivial env sigma poly ?(name=PathAny) r = let c,ctx = fresh_global_or_constr env sigma poly r in let sigma = Evd.merge_context_set univ_flexible sigma ctx in - let t = hnf_constr env sigma (unsafe_type_of env sigma c) in + let t = hnf_constr env sigma (Retyping.get_type_of env sigma c) in let hd = head_constr sigma t in let ce = mk_clenv_from_env env sigma None (c,t) in - (Some hd, { pri=1; - poly = poly; - pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce))); - name = name; - db = None; - secvars = secvars_of_constr env sigma c; - code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) + (Some hd, + { pri=1; + poly = poly; + pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce))); + name = name; + db = None; + secvars = secvars_of_constr env sigma c; + code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) @@ -1029,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 @@ -1055,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 | _ -> () @@ -1131,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' @@ -1148,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 = @@ -1180,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 = @@ -1188,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 @@ -1214,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 @@ -1326,6 +1344,13 @@ let project_hint ~poly pri l2r r = let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in (info,false,true,PathAny, IsGlobRef (GlobRef.ConstRef c)) +let warn_deprecated_hint_constr = + CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated" + (fun () -> + Pp.strbrk + "Declaring arbitrary terms as hints is deprecated; declare a global reference instead" + ) + let interp_hints ~poly = fun h -> let env = Global.env () in @@ -1350,7 +1375,9 @@ let interp_hints ~poly = | HintsReference c -> let gr = global_with_alias c in (PathHints [gr], poly, IsGlobRef gr) - | HintsConstr c -> (PathAny, poly, f poly c) + | HintsConstr c -> + let () = warn_deprecated_hint_constr () in + (PathAny, poly, f poly c) in let fp = Constrintern.intern_constr_pattern env sigma in let fres (info, b, r) = @@ -1392,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) -> @@ -1511,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 2a9b71387e..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 @@ -160,6 +168,8 @@ module Hint_db : val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit + val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a + val use_dn : t -> bool val transparent_state : t -> TransparentState.t val set_transparent_state : t -> TransparentState.t -> t @@ -179,7 +189,7 @@ type hnf = bool type hint_term = | IsGlobRef of GlobRef.t - | IsConstr of constr * Univ.ContextSet.t + | IsConstr of constr * Univ.ContextSet.t [@ocaml.deprecated "Declare a hint constant instead"] type hints_entry = | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list @@ -209,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 90a9a7acd9..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 *) @@ -19,7 +19,6 @@ open Inductiveops open Constr_matching open Coqlib open Declarations -open Tacmach.New open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -432,10 +431,10 @@ let match_eq sigma eqn (ref, hetero) = in match EConstr.kind sigma eqn with | App (c, [|t; x; y|]) -> - if not hetero && Termops.is_global sigma ref c then PolymorphicLeibnizEq (t, x, y) + if not hetero && isRefX sigma ref c then PolymorphicLeibnizEq (t, x, y) else raise PatternMatchingFailure | App (c, [|t; x; t'; x'|]) -> - if hetero && Termops.is_global sigma ref c then HeterogenousEq (t, x, t', x') + if hetero && isRefX sigma ref c then HeterogenousEq (t, x, t', x') else raise PatternMatchingFailure | _ -> raise PatternMatchingFailure @@ -452,26 +451,26 @@ let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *) let hd,u = destInd sigma (fst (destApp sigma eqn)) in d,u,k -let extract_eq_args gl = function +let extract_eq_args env sigma = function | MonomorphicLeibnizEq (e1,e2) -> - let t = pf_unsafe_type_of gl e1 in (t,e1,e2) + let t = Retyping.get_type_of env sigma e1 in (t,e1,e2) | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2) | HeterogenousEq (t1,e1,t2,e2) -> - if pf_conv_x gl t1 t2 then (t1,e1,e2) + if Reductionops.is_conv env sigma t1 t2 then (t1,e1,e2) else raise PatternMatchingFailure -let find_eq_data_decompose gl eqn = - let (lbeq,u,eq_args) = find_eq_data (project gl) eqn in - (lbeq,u,extract_eq_args gl eq_args) +let find_eq_data_decompose env sigma eqn = + let (lbeq,u,eq_args) = find_eq_data sigma eqn in + (lbeq,u,extract_eq_args env sigma eq_args) -let find_this_eq_data_decompose gl eqn = +let find_this_eq_data_decompose env sigma eqn = let (lbeq,u,eq_args) = try (*first_match (match_eq eqn) inversible_equalities*) - find_eq_data (project gl) eqn + find_eq_data sigma eqn with PatternMatchingFailure -> user_err (str "No primitive equality found.") in let eq_args = - try extract_eq_args gl eq_args + try extract_eq_args env sigma eq_args with PatternMatchingFailure -> user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in (lbeq,u,eq_args) @@ -480,9 +479,9 @@ let find_this_eq_data_decompose gl eqn = let match_sigma env sigma ex = match EConstr.kind sigma ex with - | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sig.intro") f -> + | App (f, [| a; p; car; cdr |]) when isRefX sigma (lib_ref "core.sig.intro") f -> build_sigma (), (snd (destConstruct sigma f), a, p, car, cdr) - | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sigT.intro") f -> + | App (f, [| a; p; car; cdr |]) when isRefX sigma (lib_ref "core.sigT.intro") f -> build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr) | _ -> raise PatternMatchingFailure diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 803305a1ca..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 *) @@ -122,11 +122,11 @@ val match_with_equation: (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *) -val find_eq_data_decompose : Proofview.Goal.t -> constr -> +val find_eq_data_decompose : Environ.env -> evar_map -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** Idem but fails with an error message instead of PatternMatchingFailure *) -val find_this_eq_data_decompose : Proofview.Goal.t -> constr -> +val find_this_eq_data_decompose : Environ.env -> evar_map -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** A variant that returns more informative structure on the equality found *) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 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 be0421d42d..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 *) @@ -352,7 +352,7 @@ let dest_nf_eq env sigma t = match EConstr.kind sigma t with | App (r, [| t; x; y |]) -> let open Reductionops in let eq = Coqlib.lib_ref "core.eq.type" in - if EConstr.is_global sigma eq r then + if isRefX sigma eq r then (t, whd_all env sigma x, whd_all env sigma y) else user_err Pp.(str "Not an equality.") | _ -> @@ -464,7 +464,7 @@ let raw_inversion inv_kind id status names = let concl = Proofview.Goal.concl gl in let c = mkVar id in let (ind, t) = - try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c) + try pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl c) with UserError _ -> let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in CErrors.user_err msg 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 cf58c9306c..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 *) @@ -259,7 +259,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac = let lemInv id c = Proofview.Goal.enter begin fun gls -> try - let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in + let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_get_type_of gls c) in let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false with 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 3c9803432a..b228a04298 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 *) @@ -17,7 +17,6 @@ open Evd let use_unification_heuristics_ref = ref true let () = Goptions.(declare_bool_option { optdepr = false; - optname = "Solve unification constraints at every \".\""; optkey = ["Solve";"Unification";"Constraints"]; optread = (fun () -> !use_unification_heuristics_ref); optwrite = (fun a -> use_unification_heuristics_ref:=a); @@ -27,8 +26,8 @@ let use_unification_heuristics () = !use_unification_heuristics_ref exception NoSuchGoal let () = CErrors.register_handler begin function - | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") - | _ -> raise CErrors.Unhandled + | NoSuchGoal -> Some Pp.(str "No such goal.") + | _ -> None end let get_nth_V82_goal p i = @@ -117,35 +116,31 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t let next = let n = ref 0 in fun () -> incr n; !n -let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~poly typ tac = - let evd = Evd.from_ctx ctx in +let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ~uctx ~sign ~poly typ tac = + let evd = Evd.from_ctx uctx in let goals = [ (Global.env_of_context sign , typ) ] in let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in - try - let pf, status = by tac pf in - let open Proof_global in - let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in - match entries with - | [entry] -> - entry, status, universes - | _ -> - CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") - with reraise -> - let reraise = CErrors.push reraise in - iraise reraise - -let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = + let pf, status = by tac pf in + let open Proof_global in + let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in + match entries with + | [entry] -> + entry, status, uctx + | _ -> + CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") + +let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac = let name = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in - let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in - let cb, univs = - if side_eff then Declare.inline_private_constants ~univs env ce + let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in + let cb, uctx = + if side_eff then Declare.inline_private_constants ~uctx env ce else (* GG: side effects won't get reset: no need to treat their universes specially *) let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in - cb, UState.merge ~sideff:false Evd.univ_rigid univs ctx + cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx in - cb, status, univs + cb, ce.Declare.proof_entry_type, status, univs let refine_by_tactic ~name ~poly env sigma ty tac = (* Save the initial side-effects to restore them afterwards. We set the @@ -161,8 +156,8 @@ let refine_by_tactic ~name ~poly env sigma ty tac = try Proof.run_tactic env tac prf with Logic_monad.TacticFailure e as src -> (* Catch the inner error of the monad tactic *) - let (_, info) = CErrors.push src in - iraise (e, info) + let (_, info) = Exninfo.capture src in + Exninfo.iraise (e, info) in (* Plug back the retrieved sigma *) let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli index a2e742c0d7..c49e997757 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 *) @@ -64,8 +64,8 @@ val use_unification_heuristics : unit -> bool val build_constant_by_tactic : name:Id.t -> ?opaque:Proof_global.opacity_flag - -> UState.t - -> named_context_val + -> uctx:UState.t + -> sign:named_context_val -> poly:bool -> EConstr.types -> unit Proofview.tactic @@ -74,11 +74,11 @@ val build_constant_by_tactic val build_by_tactic : ?side_eff:bool -> env - -> UState.t + -> uctx:UState.t -> poly:bool - -> EConstr.types + -> typ:EConstr.types -> unit Proofview.tactic - -> constr * bool * UState.t + -> constr * types option * bool * UState.t val refine_by_tactic : name:Id.t diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index b1fd34e43c..623e6b8a42 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -1,21 +1,13 @@ (************************************************************************) (* * 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 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(***********************************************************************) -(* *) -(* This module defines proof facilities relevant to the *) -(* toplevel. In particular it defines the global proof *) -(* environment. *) -(* *) -(***********************************************************************) - open Util open Names open Context @@ -27,8 +19,7 @@ module NamedDecl = Context.Named.Declaration type proof_object = { name : Names.Id.t ; entries : Evd.side_effects Declare.proof_entry list - ; poly : bool - ; universes: UState.t + ; uctx: UState.t ; udecl : UState.universe_decl } @@ -143,7 +134,6 @@ let private_poly_univs = let b = ref true in let _ = Goptions.(declare_bool_option { optdepr = false; - optname = "use private polymorphic universes for Qed constants"; optkey = ["Private";"Polymorphic";"Universes"]; optread = (fun () -> !b); optwrite = ((:=) b); @@ -160,7 +150,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx in let fpl, univs = Future.split2 fpl in - let universes = if poly || now then Future.force univs else initial_euctx in + let uctx = if poly || now then Future.force univs else initial_euctx in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) @@ -168,7 +158,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let { Proof.sigma } = Proof.data proof in Evd.existential_opt_value0 sigma k in let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar - (UState.subst universes) in + (UState.subst uctx) in let make_body = if poly || now then @@ -183,7 +173,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let used_univs_typ = Vars.universes_of_constr typ in if allow_deferred then let initunivs = UState.univ_entry ~poly initial_euctx in - let ctx = constrain_variables universes in + let ctx = constrain_variables uctx in (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of the body. So we keep the two sets distinct. *) @@ -193,7 +183,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now (initunivs, typ), ((body, univs), eff) else if poly && opaque && private_poly_univs () then let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let universes = UState.restrict universes used_univs in + let universes = UState.restrict uctx used_univs in let typus = UState.restrict universes used_univs_typ in let udecl = UState.check_univ_decl ~poly typus udecl in let ubody = Univ.ContextSet.diff @@ -208,7 +198,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now the actually used universes. TODO: check if restrict is really necessary now. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx = UState.restrict universes used_univs in + let ctx = UState.restrict uctx used_univs in let univs = UState.check_univ_decl ~poly ctx udecl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in @@ -216,7 +206,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now else fun t p -> (* Already checked the univ_decl for the type universes when starting the proof. *) - let univctx = UState.univ_entry ~poly:false universes in + let univctx = UState.univ_entry ~poly:false uctx in let t = nf t in Future.from_val (univctx, t), Future.chain p (fun (pt,eff) -> @@ -241,7 +231,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body in let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in - { name; entries; poly; universes; udecl } + { name; entries; uctx; udecl } let return_proof ?(allow_partial=false) ps = let { proof } = ps in diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index 9161eae82f..e1c75c0649 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -1,16 +1,14 @@ (************************************************************************) (* * 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 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** This module defines proof facilities relevant to the - toplevel. In particular it defines the global proof - environment. *) +(** State for interactive proofs. *) type t @@ -33,9 +31,7 @@ type proof_object = (** name of the proof *) ; entries : Evd.side_effects Declare.proof_entry list (** list of the proof terms (in a form suitable for definitions). *) - ; poly : bool - (** polymorphic status *) - ; universes: UState.t + ; uctx: UState.t (** universe state *) ; udecl : UState.universe_decl (** universe declaration *) diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index fc7b126ee5..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 *) @@ -56,8 +56,6 @@ let strong_cbn flags = let simplIsCbn = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Plug the simpl tactic to the new cbn mechanism"; optkey = ["SimplIsCbn"]; optread = (fun () -> !simplIsCbn); optwrite = (fun a -> simplIsCbn:=a); 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 ed7ab9164a..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 *) @@ -587,7 +587,7 @@ module New = struct let ifOnHyp pred tac1 tac2 id = Proofview.Goal.enter begin fun gl -> let typ = Tacmach.New.pf_get_hyp_typ id gl in - if pred (id,typ) then + if pf_apply pred gl (id,typ) then tac1 id else tac2 id @@ -633,7 +633,7 @@ module New = struct (Proofview.Goal.enter begin fun gl -> let indclause = mk_clenv_from gl (c, t) in (* applying elimination_scheme just a little modified *) - let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim) in + let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim) in let indmv = match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with | Meta mv -> mv @@ -741,7 +741,7 @@ module New = struct let elimination_then tac c = Proofview.Goal.enter begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in + let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with | NotRecord -> true,gl_make_elim diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 31d26834d6..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 *) @@ -144,7 +144,7 @@ module New : sig (** [catch_failerror e] fails and decreases the level if [e] is an Ltac error with level more than 0. Otherwise succeeds. *) - val catch_failerror : Util.iexn -> unit tactic + val catch_failerror : Exninfo.iexn -> unit tactic val tclIDTAC : unit tactic val tclTHEN : unit tactic -> unit tactic -> unit tactic @@ -222,7 +222,7 @@ module New : sig val nLastDecls : Proofview.Goal.t -> int -> named_context - val ifOnHyp : (Id.t * types -> bool) -> + val ifOnHyp : (Environ.env -> evar_map -> Id.t * types -> bool) -> (Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) -> Id.t -> unit Proofview.tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9258a75461..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 *) @@ -47,6 +47,9 @@ open Context.Named.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration +let tclEVARS = Proofview.Unsafe.tclEVARS +let tclEVARSTHEN sigma t = Proofview.tclTHEN (tclEVARS sigma) t + let inj_with_occurrences e = (AllOccurrences,e) let typ_of env sigma c = @@ -64,7 +67,6 @@ let use_clear_hyp_by_default () = !clear_hyp_by_default let () = declare_bool_option { optdepr = false; - optname = "default clearing of hypotheses after use"; optkey = ["Default";"Clearing";"Used";"Hypotheses"]; optread = (fun () -> !clear_hyp_by_default) ; optwrite = (fun b -> clear_hyp_by_default := b) } @@ -80,7 +82,6 @@ let accept_universal_lemma_under_conjunctions () = let () = declare_bool_option { optdepr = false; - optname = "trivial unification in tactics applying under conjunctions"; optkey = ["Universal";"Lemma";"Under";"Conjunction"]; optread = (fun () -> !universal_lemma_under_conjunctions) ; optwrite = (fun b -> universal_lemma_under_conjunctions := b) } @@ -99,7 +100,6 @@ let use_bracketing_last_or_and_intro_pattern () = let () = declare_bool_option { optdepr = true; - optname = "bracketing last or-and introduction pattern"; optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; optread = (fun () -> !bracketing_last_or_and_intro_pattern); optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) } @@ -151,11 +151,12 @@ let convert_concl ~check ty k = Refine.refine ~typecheck:false begin fun sigma -> let sigma = if check then begin - ignore (Typing.unsafe_type_of env sigma ty); + let sigma, _ = Typing.type_of env sigma ty in match Reductionops.infer_conv env sigma ty conclty with | None -> error "Not convertible." | Some sigma -> sigma - end else sigma in + end else sigma + in let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ty in let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in (sigma, ans) @@ -849,12 +850,13 @@ let change_on_subterm ~check cv_pb deep t where env sigma c = change_and_check Reduction.CONV mayneedglobalcheck true (t subst) else fun env sigma _c -> t subst env sigma) env sigma c in - if !mayneedglobalcheck then + let sigma = if !mayneedglobalcheck then begin - try ignore (Typing.unsafe_type_of env sigma c) - with e when catchable_exception e -> + try fst (Typing.type_of env sigma c) + with e when noncritical e -> error "Replacement would lead to an ill-typed term." - end; + end else sigma + in (sigma, c) let change_in_concl ~check occl t = @@ -1308,30 +1310,23 @@ let cut c = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in - let relevance = - try - (* Backward compat: ensure that [c] is well-typed. Plus we - need to know the relevance *) - let typ = Typing.unsafe_type_of env sigma c in - let typ = whd_all env sigma typ in - match EConstr.kind sigma typ with - | Sort s -> Some (Sorts.relevance_of_sort (ESorts.kind sigma s)) - | _ -> None - with e when Pretype_errors.precatchable_exception e -> None - in - match relevance with - | Some r -> + (* 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 noncritical e -> + Tacticals.New.tclZEROMSG (str "Not a proposition or a type.") + | sigma, s -> + let r = Sorts.relevance_of_sort s in let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in (* Backward compat: normalize [c]. *) let c = if normalize_cut then local_strong whd_betaiota sigma c else c in - Refine.refine ~typecheck:false begin fun h -> - let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in - let (h, x) = Evarutil.new_evar env h c in - let f = mkLetIn (make_annot (Name id) r, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in - (h, f) - end - | None -> - Tacticals.New.tclZEROMSG (str "Not a proposition or a type.") + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Refine.refine ~typecheck:false begin fun h -> + let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in + let (h, x) = Evarutil.new_evar env h c in + let f = mkLetIn (make_annot (Name id) r, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in + (h, f) + end) end let error_uninstantiated_metas t clenv = @@ -1533,16 +1528,19 @@ exception IsNonrec let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite -let find_ind_eliminator ind s gl = - let env = Proofview.Goal.env gl in +let find_ind_eliminator env sigma ind s = let gr = lookup_eliminator env ind s in - Tacmach.New.pf_apply Evd.fresh_global gl gr + Evd.fresh_global env sigma gr let find_eliminator c gl = - let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let sigma, t = Typing.type_of env sigma c in + let ((ind,u),t) = reduce_to_quantified_ind env sigma t in if is_nonrec ind then raise IsNonrec; - let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in - evd, { elimindex = None; elimbody = (c,NoBindings) } + let sigma, c = find_ind_eliminator env sigma ind (Retyping.get_sort_family_of env sigma concl) in + sigma, { elimindex = None; elimbody = (c,NoBindings) } let default_elim with_evars clear_flag (c,_ as cx) = Proofview.tclORELSE @@ -1719,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) = @@ -1820,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 @@ -1850,12 +1848,12 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = let rec aux clause = try progress_with_clause flags innerclause clause with e when CErrors.noncritical e -> - let e' = CErrors.push e in + let e' = Exninfo.capture e in try aux (clenv_push_prod clause) with NotExtensibleClause -> match e with | UnableToApply -> explain_unable_to_apply_lemma ?loc env sigma thm innerclause - | _ -> iraise e' + | _ -> Exninfo.iraise e' in aux (make_clenv_binding env sigma (d,thm) lbind) @@ -1888,7 +1886,7 @@ let apply_in_once ?(respect_opaque = false) with_delta tac id ]) with e when with_destruct && CErrors.noncritical e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in (descend_in_conjunctions (Id.Set.singleton targetid) (fun b id -> aux (id::idstoclear) b (mkVar id)) (e, info) c) @@ -1928,18 +1926,20 @@ let apply_in_delayed_once ?(respect_opaque = false) with_delta let cut_and_apply c = Proofview.Goal.enter begin fun gl -> - let sigma = Tacmach.New.project gl in - match EConstr.kind sigma (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with - | Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 -> - let concl = Proofview.Goal.concl gl in - let env = Tacmach.New.pf_env gl in - Refine.refine ~typecheck:false begin fun sigma -> - let typ = mkProd (make_annot Anonymous Sorts.Relevant, c2, concl) in - let (sigma, f) = Evarutil.new_evar env sigma typ in - let (sigma, x) = Evarutil.new_evar env sigma c1 in - (sigma, mkApp (f, [|mkApp (c, [|x|])|])) - end - | _ -> error "lapply needs a non-dependent product." + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let sigma, t = Typing.type_of env sigma c in + match EConstr.kind sigma (hnf_constr env sigma t) with + | Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 -> + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Refine.refine ~typecheck:false begin fun sigma -> + let typ = mkProd (make_annot Anonymous Sorts.Relevant, c2, concl) in + let (sigma, f) = Evarutil.new_evar env sigma typ in + let (sigma, x) = Evarutil.new_evar env sigma c1 in + (sigma, mkApp (f, [|mkApp (c, [|x|])|])) + end) + | _ -> error "lapply needs a non-dependent product." end (********************************************************************) @@ -2285,8 +2285,8 @@ let intro_decomp_eq_function = ref (fun _ -> failwith "Not implemented") let declare_intro_decomp_eq f = intro_decomp_eq_function := f -let my_find_eq_data_decompose gl t = - try Some (find_eq_data_decompose gl t) +let my_find_eq_data_decompose env sigma t = + try Some (find_eq_data_decompose env sigma t) with e when is_anomaly e (* Hack in case equality is not yet defined... one day, maybe, known equalities will be dynamically registered *) @@ -2296,13 +2296,15 @@ let my_find_eq_data_decompose gl t = let intro_decomp_eq ?loc l thin tac id = Proofview.Goal.enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_unsafe_type_of gl c in - let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in - match my_find_eq_data_decompose gl t with + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, t = Typing.type_of env sigma c in + let _,t = reduce_to_quantified_ind env sigma t in + match my_find_eq_data_decompose env sigma t with | Some (eq,u,eq_args) -> !intro_decomp_eq_function - (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l) - (eq,t,eq_args) (c, t) + (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l) + (eq,t,eq_args) (c, t) | None -> Tacticals.New.tclZEROMSG (str "Not a primitive equality here.") end @@ -2310,16 +2312,19 @@ let intro_decomp_eq ?loc l thin tac id = let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id = Proofview.Goal.enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_unsafe_type_of gl c in - let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, t = Typing.type_of env sigma c in + let (ind,t) = reduce_to_quantified_ind env sigma t in let branchsigns = compute_constructor_signatures ~rec_flag:false ind in let nv_with_let = Array.map List.length branchsigns in let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in let ll = get_and_check_or_and_pattern ?loc ll branchsigns in - Tacticals.New.tclTHENLASTn - (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id])) - (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l) - nv_with_let ll) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tacticals.New.tclTHENLASTn + (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id])) + (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l) + nv_with_let ll)) end let rewrite_hyp_then assert_style with_evars thin l2r id tac = @@ -2333,9 +2338,8 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let type_of = Tacmach.New.pf_unsafe_type_of gl in - let whd_all = Tacmach.New.pf_apply whd_all gl in - let t = whd_all (type_of (mkVar id)) in + let sigma, t = Typing.type_of env sigma (mkVar id) in + let t = whd_all env sigma t in let eqtac, thin = match match_with_equality_type env sigma t with | Some (hdcncl,[_;lhs;rhs]) -> if l2r && isVar sigma lhs && not (occur_var env sigma (destVar sigma lhs) rhs) then @@ -2361,7 +2365,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]), thin in (* Skip the side conditions of the rewriting step *) - Tacticals.New.tclTHENFIRST eqtac (tac thin) + tclEVARSTHEN sigma (Tacticals.New.tclTHENFIRST eqtac (tac thin)) end let prepare_naming ?loc = function @@ -2977,6 +2981,13 @@ let quantify lconstr = (* Modifying/Adding an hypothesis *) +(* This applies (f i) to all elements of ctxt where the debrujn i is + free (so it is lifted at each level). *) +let rec map_rel_context_lift f env i (ctxt:EConstr.rel_context):EConstr.rel_context = + match ctxt with + | [] -> ctxt + | decl::ctxt' -> f i decl :: map_rel_context_lift f env (i+1) ctxt' + (* Instantiating some arguments (whatever their position) of an hypothesis or any term, leaving other arguments quantified. If operating on an hypothesis of the goal, the new hypothesis replaces it. @@ -2993,16 +3004,17 @@ let quantify lconstr = solve, ui are a mix of inferred args and yi. The overall effect is to remove from H as much quantification as possible given lbind. *) + let specialize (c,lbind) ipat = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let sigma, term = + let typ_of_c = Retyping.get_type_of env sigma c in + let sigma, term, typ = if lbind == NoBindings then - sigma, c + sigma, c, typ_of_c else (* ***** SOLVING ARGS ******* *) - let typ_of_c = Retyping.get_type_of env sigma c in (* If the term is lambda then we put a letin to put avoid interaction between the term and the bindings. *) let c = match EConstr.kind sigma c with @@ -3028,38 +3040,53 @@ let specialize (c,lbind) ipat = | _ -> x in (* We grab names used in product to remember them at re-abstracting phase *) let typ_of_c_hd = pf_get_type_of gl thd in - let lprod, concl = decompose_prod_assum sigma typ_of_c_hd in + let (lprod:rel_context), concl = decompose_prod_assum sigma typ_of_c_hd in (* lprd = initial products (including letins). l(tstack initially) = the same products after unification vs lbind (some metas remain) args: accumulator : args to apply to hd: inferred args + metas reabstracted *) - let rec rebuild_lambdas sigma lprd args hd l = + let rec rebuild sigma concl (lprd:rel_context) (accargs:EConstr.t list) + (accprods:rel_context) hd (l:EConstr.t list) = + let open Context.Rel.Declaration in match lprd , l with - | _, [] -> sigma,applist (hd, (List.map (nf_evar sigma) args)) - | Context.Rel.Declaration.LocalAssum(nme,_)::lp' , t::l' when occur_meta sigma t -> + | _, [] -> sigma + , applist (hd, (List.map (nf_evar sigma) (List.rev accargs))) + , EConstr.it_mkProd_or_LetIn concl accprods + | (LocalAssum(nme,_) as assum)::lp' , t::l' when occur_meta sigma t -> (* nme has not been resolved, let us re-abstract it. Same name but type updated by instantiation of other args. *) let sigma,new_typ_of_t = Typing.type_of clause.env sigma t in let r = Retyping.relevance_of_type env sigma new_typ_of_t in - let liftedargs = List.map liftrel args in (* lifting rels in the accumulator args *) - let sigma,hd' = rebuild_lambdas sigma lp' (liftedargs@[mkRel 1 ]) hd l' in + let liftedargs = List.map liftrel accargs in + let sigma,hd',prods = + rebuild sigma concl lp' (mkRel 1 ::liftedargs) (assum::accprods) hd l' in (* replace meta variable by the abstracted variable *) let hd'' = subst_term sigma t hd' in - (* lambda expansion *) - sigma,mkLambda ({nme with binder_relevance=r},new_typ_of_t,hd'') - | Context.Rel.Declaration.LocalAssum _::lp' , t::l' -> - let sigma,hd' = rebuild_lambdas sigma lp' (args@[t]) hd l' in - sigma,hd' - | Context.Rel.Declaration.LocalDef _::lp' , _ -> - (* letins have been reduced in l and should anyway not - correspond to an arg, we ignore them. *) - let sigma,hd' = rebuild_lambdas sigma lp' args hd l in - sigma,hd' + (* we reabstract the non solved argument *) + sigma,mkLambda ({nme with binder_relevance=r},new_typ_of_t,hd''),prods + | (LocalAssum (nme,tnme))::lp' , t::l' -> + (* thie arg was solved, we update thing accordingly *) + (* we replace in lprod the arg by rel 1 *) + let substlp' = (* rel 1 must be lifted along the context *) + map_rel_context_lift (fun i x -> map_constr (replace_term sigma (mkRel i) t) x) + env 1 lp' in + (* Then we lift every rel above the just removed arg *) + let updatedlp' = + map_rel_context_lift (fun i x -> map_constr (liftn (-1) i) x) env 1 substlp' in + (* We replace also the term in the conclusion, its rel index is the + length of the list lprd (remaining products before concl) *) + let concl'' = replace_term sigma (mkRel (List.length lprd)) t concl in + (* we also lift in concl the index above the arg *) + let concl' = liftn (-1) (List.length lprd) concl'' in + rebuild sigma concl' updatedlp' (t::accargs) accprods hd l' + | LocalDef _ as assum::lp' , _ -> + (* letins have been reduced in l and should anyway not correspond to an arg, we + ignore them, but we remember them in accprod, so that they remain in the type. *) + rebuild sigma concl lp' accargs (assum::accprods) hd l | _ ,_ -> assert false in - let sigma,hd = rebuild_lambdas sigma (List.rev lprod) [] thd tstack in - Evd.clear_metas sigma, hd + let sigma,hd,newtype = rebuild sigma concl (List.rev lprod) [] [] thd tstack in + Evd.clear_metas sigma, hd, newtype in - let typ = Retyping.get_type_of env sigma term in let tac = match EConstr.kind sigma (fst(EConstr.decompose_app sigma (snd(EConstr.decompose_lam_assum sigma c)))) with | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) -> @@ -3128,7 +3155,7 @@ let clear_for_destruct ids = (clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids) (function | ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT () - | e -> iraise e) + | e -> Exninfo.iraise e) (* Either unfold and clear if defined or simply clear if not a definition *) let expand_hyp id = @@ -3369,8 +3396,9 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = let id = match EConstr.kind sigma c with | Var id -> id | _ -> - let type_of = Tacmach.New.pf_unsafe_type_of gl in - id_of_name_using_hdchar env sigma (type_of c) Anonymous in + let type_of = Tacmach.New.pf_get_type_of gl in + id_of_name_using_hdchar env sigma (type_of c) Anonymous + in let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN (letin_tac None (Name x) c None allHypsAndConcl) @@ -3771,15 +3799,15 @@ let is_defined_variable env id = env |> lookup_named id |> is_local_def let abstract_args gl generalize_vars dep id defined f args = - let open Tacmach.New in let open Context.Rel.Declaration in let sigma = ref (Tacmach.New.project gl) in let env = Tacmach.New.pf_env gl in let concl = Tacmach.New.pf_concl gl in + let hyps = Proofview.Goal.hyps gl in let dep = dep || local_occur_var !sigma id concl in let avoid = ref Id.Set.empty in let get_id name = - let id = new_fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in + let id = fresh_id_in_env !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") env in avoid := Id.Set.add id !avoid; id in (* Build application generalized w.r.t. the argument plus the necessary eqs. @@ -3788,14 +3816,14 @@ let abstract_args gl generalize_vars dep id defined f args = eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *) *) - let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg = + let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars) arg = let name, ty_relevance, ty, arity = let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in let decl = List.hd rel in RelDecl.get_name decl, RelDecl.get_relevance decl, RelDecl.get_type decl, c in - let argty = Tacmach.New.pf_unsafe_type_of gl arg in - let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in + let sigma', argty = Typing.type_of env !sigma arg in + let sigma', ty = Evarsolve.refresh_universes (Some true) env sigma' ty in let () = sigma := sigma' in let lenctx = List.length ctx in let liftargty = lift lenctx argty in @@ -3803,7 +3831,7 @@ let abstract_args gl generalize_vars dep id defined f args = match EConstr.kind !sigma arg with | Var id when not (is_defined_variable env id) && leq && not (Id.Set.mem id nongenvars) -> (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, - Id.Set.add id nongenvars, Id.Set.remove id vars, env) + Id.Set.add id nongenvars, Id.Set.remove id vars) | _ -> let name = get_id name in let decl = LocalAssum (make_annot (Name name) ty_relevance, ty) in @@ -3825,7 +3853,7 @@ let abstract_args gl generalize_vars dep id defined f args = let refls = refl :: refls in let argvars = ids_of_constr !sigma vars arg in (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, - nongenvars, Id.Set.union argvars vars, env) + nongenvars, Id.Set.union argvars vars) in let f', args' = decompose_indapp !sigma f args in let dogen, f', args' = @@ -3839,15 +3867,16 @@ let abstract_args gl generalize_vars dep id defined f args = true, mkApp (f', before), after in if dogen then - let tyf' = Tacmach.New.pf_unsafe_type_of gl f' in - let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = - Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' + let sigma', tyf' = Typing.type_of env !sigma f' in + sigma := sigma'; + let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars = + Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty) args' in let args, refls = List.rev args, List.rev refls in let vars = if generalize_vars then let nogen = Id.Set.add id nogen in - hyps_of_vars (pf_env gl) (project gl) (Proofview.Goal.hyps gl) nogen vars + hyps_of_vars env !sigma hyps nogen vars else [] in let body, c' = @@ -3855,7 +3884,7 @@ let abstract_args gl generalize_vars dep id defined f args = else None, c' in let typ = Tacmach.New.pf_get_hyp_typ id gl in - let tac = make_abstract_generalize (pf_env gl) id typ concl dep ctx body c' eqs args refls in + let tac = make_abstract_generalize env id typ concl dep ctx body c' eqs args refls in let tac = Proofview.Unsafe.tclEVARS !sigma <*> tac in Some (tac, dep, succ (List.length ctx), vars) else None @@ -3923,7 +3952,7 @@ let specialize_eqs id = match EConstr.kind !evars ty with | Prod (na, t, b) -> (match EConstr.kind !evars t with - | App (eq, [| eqty; x; y |]) when EConstr.is_global !evars Coqlib.(lib_ref "core.eq.type") eq -> + | App (eq, [| eqty; x; y |]) when isRefX !evars Coqlib.(lib_ref "core.eq.type") eq -> let c = if noccur_between !evars 1 (List.length ctx) x then y else x in let pt = mkApp (eq, [| eqty; c; c |]) in let ind = destInd !evars eq in @@ -3931,7 +3960,7 @@ let specialize_eqs id = if unif (push_rel_context ctx env) evars pt t then aux true ctx (mkApp (acc, [| p |])) (subst1 p b) else acc, in_eqs, ctx, ty - | App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq -> + | App (heq, [| eqty; x; eqty'; y |]) when isRefX !evars (Lazy.force coq_heq_ref) heq -> let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in let pt = mkApp (heq, [| eqt; c; eqt; c |]) in let ind = destInd !evars heq in @@ -4102,8 +4131,8 @@ let compute_elim_sig sigma ?elimc elimt = | Some (LocalDef _) -> error_ind_scheme "" | Some (LocalAssum (_,ind)) -> let indhd,indargs = decompose_app sigma ind in - try {!res with indref = Some (fst (Termops.global_of_constr sigma indhd)) } - with e when CErrors.noncritical e -> + try {!res with indref = Some (fst (destRef sigma indhd)) } + with DestKO -> error "Cannot find the inductive type of the inductive scheme." let compute_scheme_signature evd scheme names_info ind_type_guess = @@ -4199,15 +4228,15 @@ let guess_elim isrec dep s hyp0 gl = let ind = EConstr.of_constr ind in (sigma, ind) in - let elimt = Typing.unsafe_type_of env sigma elimc in - sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u) + let sigma, elimt = Typing.type_of env sigma elimc in + sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u) let given_elim hyp0 (elimc,lbind as e) gl = let sigma = Tacmach.New.project gl in let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let ind_type_guess,_ = decompose_app sigma (snd (decompose_prod sigma tmptyp0)) in - let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in - Tacmach.New.project gl, (e, elimt), ind_type_guess + let sigma, elimt = Tacmach.New.pf_type_of gl elimc in + sigma, (e, elimt), ind_type_guess type scheme_signature = (Id.Set.t * (elim_arg_kind * bool * bool * Id.t) list) array @@ -4217,33 +4246,33 @@ type eliminator_source = | ElimOver of bool * Id.t let find_induction_type isrec elim hyp0 gl = - let sigma = Tacmach.New.project gl in - let scheme,elim = + let sigma, indref, nparams, elim = match elim with | None -> let sort = Tacticals.New.elimination_sort_of_goal gl in - let _, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in - let scheme = compute_elim_sig sigma ~elimc elimt in - (* We drop the scheme waiting to know if it is dependent *) - scheme, ElimOver (isrec,hyp0) + let sigma', (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in + let scheme = compute_elim_sig sigma' ~elimc elimt in + (* We drop the scheme and elimc/elimt waiting to know if it is dependent, this + needs no update to sigma at this point. *) + Tacmach.New.project gl, scheme.indref, scheme.nparams, ElimOver (isrec,hyp0) | Some e -> - let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in + let sigma, (elimc,elimt),ind_guess = given_elim hyp0 e gl in let scheme = compute_elim_sig sigma ~elimc elimt in if Option.is_empty scheme.indarg then error "Cannot find induction type"; - let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in + let indsign = compute_scheme_signature sigma scheme hyp0 ind_guess in let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in - scheme, ElimUsing (elim,indsign) + sigma, scheme.indref, scheme.nparams, ElimUsing (elim,indsign) in - match scheme.indref with + match indref with | None -> error_ind_scheme "" - | Some ref -> ref, scheme.nparams, elim + | Some ref -> sigma, (ref, nparams, elim) let get_elim_signature elim hyp0 gl = compute_elim_signature (given_elim hyp0 elim gl) hyp0 let is_functional_induction elimc gl = let sigma = Tacmach.New.project gl in - let scheme = compute_elim_sig sigma ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in + let scheme = compute_elim_sig sigma ~elimc (Tacmach.New.pf_get_type_of gl (fst elimc)) in (* The test is not safe: with non-functional induction on non-standard induction scheme, this may fail *) Option.is_empty scheme.indarg @@ -4357,10 +4386,11 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps = Proofview.Goal.enter begin fun gl -> - let elim_info = find_induction_type isrec elim hyp0 gl in - atomize_param_of_ind_then elim_info hyp0 (fun indvars -> - apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names - (fun elim -> induction_tac with_evars [] [hyp0] elim)) + let sigma, elim_info = find_induction_type isrec elim hyp0 gl in + tclEVARSTHEN sigma + (atomize_param_of_ind_then elim_info hyp0 (fun indvars -> + apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names + (fun elim -> induction_tac with_evars [] [hyp0] elim))) end let msg_not_right_number_induction_arguments scheme = @@ -4456,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 @@ -4635,18 +4665,16 @@ let induction_gen_l isrec with_evars elim names lc = | _ -> Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_unsafe_type_of gl in - let sigma = Tacmach.New.project gl in - Proofview.tclENV >>= fun env -> - let x = - id_of_name_using_hdchar env sigma (type_of c) Anonymous in - + let sigma, t = pf_apply Typing.type_of gl c in + let x = id_of_name_using_hdchar (Proofview.Goal.env gl) sigma t Anonymous in let id = new_fresh_id Id.Set.empty x gl in let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in let () = newlc:=id::!newlc in - Tacticals.New.tclTHEN - (letin_tac None (Name id) c None allHypsAndConcl) - (atomize_list newl') + Tacticals.New.tclTHENLIST [ + tclEVARS sigma; + letin_tac None (Name id) c None allHypsAndConcl; + atomize_list newl'; + ] end in Tacticals.New.tclTHENLIST [ @@ -4742,7 +4770,10 @@ let destruct ev clr c l e = let elim_scheme_type elim t = Proofview.Goal.enter begin fun gl -> - let clause = mk_clenv_type_of gl elim in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, elimt = Typing.type_of env sigma elim in + let clause = mk_clenv_from_env env sigma None (elim,elimt) in match EConstr.kind clause.evd (last_arg clause.evd clause.templval.rebus) with | Meta mv -> let clause' = @@ -4756,7 +4787,9 @@ let elim_scheme_type elim t = let elim_type t = Proofview.Goal.enter begin fun gl -> let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in - let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in + let evd, elimc = Tacmach.New.pf_apply find_ind_eliminator gl (fst ind) + (Tacticals.New.elimination_sort_of_goal gl) + in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t) end @@ -4834,7 +4867,8 @@ let prove_symmetry hdcncl eq_kind = Tacticals.New.onLastHyp simplest_case; one_constructor 1 NoBindings ]) -let match_with_equation sigma c = +let match_with_equation c = + Proofview.tclEVARMAP >>= fun sigma -> Proofview.tclENV >>= fun env -> try let res = match_with_equation env sigma c in @@ -4847,9 +4881,8 @@ let symmetry_red allowred = (* PL: usual symmetry don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) - let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - match_with_equation sigma concl >>= fun with_eqn -> + match_with_equation concl >>= fun with_eqn -> match with_eqn with | Some eq_data,_,_ -> Tacticals.New.tclTHEN @@ -4871,25 +4904,25 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = Proofview.Goal.enter begin fun gl -> - let sigma = Tacmach.New.project gl in - let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in - let sign,t = decompose_prod_assum sigma ctype in - Proofview.tclORELSE - begin - match_with_equation sigma t >>= fun (_,hdcncl,eq) -> - let symccl = - match eq with - | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |]) - | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |]) - | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in - Tacticals.New.tclTHENS (cut (EConstr.it_mkProd_or_LetIn symccl sign)) - [ intro_replacing id; - Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ] - end - begin function (e, info) -> match e with - | NoEquationFound -> Hook.get forward_setoid_symmetry_in id - | e -> Proofview.tclZERO ~info e - end + let sigma, ctype = Tacmach.New.pf_type_of gl (mkVar id) in + let sign,t = decompose_prod_assum sigma ctype in + tclEVARSTHEN sigma + (Proofview.tclORELSE + begin + match_with_equation t >>= fun (_,hdcncl,eq) -> + let symccl = + match eq with + | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |]) + | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |]) + | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in + Tacticals.New.tclTHENS (cut (EConstr.it_mkProd_or_LetIn symccl sign)) + [ intro_replacing id; + Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ] + end + begin function (e, info) -> match e with + | NoEquationFound -> Hook.get forward_setoid_symmetry_in id + | e -> Proofview.tclZERO ~info e + end) end let intros_symmetry = @@ -4916,25 +4949,26 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make () (* This is probably not very useful any longer *) let prove_transitivity hdcncl eq_kind t = Proofview.Goal.enter begin fun gl -> - let (eq1,eq2) = match eq_kind with - | MonomorphicLeibnizEq (c1,c2) -> - mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]) - | PolymorphicLeibnizEq (typ,c1,c2) -> - mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |]) - | HeterogenousEq (typ1,c1,typ2,c2) -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let type_of = Typing.unsafe_type_of env sigma in - let typt = type_of t in - (mkApp(hdcncl, [| typ1; c1; typt ;t |]), - mkApp(hdcncl, [| typt; t; typ2; c2 |])) - in - Tacticals.New.tclTHENFIRST (cut eq2) - (Tacticals.New.tclTHENFIRST (cut eq1) - (Tacticals.New.tclTHENLIST - [ Tacticals.New.tclDO 2 intro; - Tacticals.New.onLastHyp simplest_case; - assumption ])) + let sigma = Tacmach.New.project gl in + let sigma, eq1, eq2 = match eq_kind with + | MonomorphicLeibnizEq (c1,c2) -> + sigma, mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]) + | PolymorphicLeibnizEq (typ,c1,c2) -> + sigma, mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |]) + | HeterogenousEq (typ1,c1,typ2,c2) -> + let env = Proofview.Goal.env gl in + let sigma, typt = Typing.type_of env sigma t in + sigma, + mkApp(hdcncl, [| typ1; c1; typt ;t |]), + mkApp(hdcncl, [| typt; t; typ2; c2 |]) + in + tclEVARSTHEN sigma + (Tacticals.New.tclTHENFIRST (cut eq2) + (Tacticals.New.tclTHENFIRST (cut eq1) + (Tacticals.New.tclTHENLIST + [ Tacticals.New.tclDO 2 intro; + Tacticals.New.onLastHyp simplest_case; + assumption ]))) end let transitivity_red allowred t = @@ -4942,9 +4976,8 @@ let transitivity_red allowred t = (* PL: usual transitivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) - let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - match_with_equation sigma concl >>= fun with_eqn -> + match_with_equation concl >>= fun with_eqn -> match with_eqn with | Some eq_data,_,_ -> Tacticals.New.tclTHEN @@ -5008,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 *) |