aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/abstract.ml195
-rw-r--r--tactics/abstract.mli16
-rw-r--r--tactics/auto.ml4
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/class_tactics.ml130
-rw-r--r--tactics/contradiction.ml5
-rw-r--r--tactics/eauto.ml6
-rw-r--r--tactics/eqdecide.ml11
-rw-r--r--tactics/eqschemes.ml4
-rw-r--r--tactics/equality.ml54
-rw-r--r--tactics/hints.ml90
-rw-r--r--tactics/hints.mli14
-rw-r--r--tactics/hipattern.ml68
-rw-r--r--tactics/ind_tables.ml3
-rw-r--r--tactics/inv.ml19
-rw-r--r--tactics/tacticals.ml11
-rw-r--r--tactics/tacticals.mli2
-rw-r--r--tactics/tactics.ml261
-rw-r--r--tactics/tactics.mli6
-rw-r--r--tactics/tactics.mllib1
20 files changed, 479 insertions, 423 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
new file mode 100644
index 0000000000..2b4d9a7adf
--- /dev/null
+++ b/tactics/abstract.ml
@@ -0,0 +1,195 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+module CVars = Vars
+
+open Util
+open Names
+open Termops
+open EConstr
+open Decl_kinds
+open Evarutil
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
+(* tactical to save as name a subproof such that the generalisation of
+ the current goal, abstracted with respect to the local signature,
+ is solved by tac *)
+
+(** d1 is the section variable in the global context, d2 in the goal context *)
+let interpretable_as_section_decl env evd d1 d2 =
+ let open Context.Named.Declaration in
+ let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env !sigma c1 c2 with
+ | None -> false
+ | Some cstr ->
+ try ignore (Evd.add_universe_constraints !sigma cstr); true
+ with UState.UniversesDiffer -> false
+ in
+ match d2, d1 with
+ | LocalDef _, LocalAssum _ -> false
+ | LocalDef (_,b1,t1), LocalDef (_,b2,t2) ->
+ e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2
+ | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2)
+
+let rec decompose len c t accu =
+ let open Constr in
+ let open Context.Rel.Declaration in
+ if len = 0 then (c, t, accu)
+ else match kind c, kind t with
+ | Lambda (na, u, c), Prod (_, _, t) ->
+ decompose (pred len) c t (LocalAssum (na, u) :: accu)
+ | LetIn (na, b, u, c), LetIn (_, _, _, t) ->
+ decompose (pred len) c t (LocalDef (na, b, u) :: accu)
+ | _ -> assert false
+
+let rec shrink ctx sign c t accu =
+ let open Constr in
+ let open CVars in
+ match ctx, sign with
+ | [], [] -> (c, t, accu)
+ | p :: ctx, decl :: sign ->
+ if noccurn 1 c && noccurn 1 t then
+ let c = subst1 mkProp c in
+ let t = subst1 mkProp t in
+ shrink ctx sign c t accu
+ else
+ let c = Term.mkLambda_or_LetIn p c in
+ let t = Term.mkProd_or_LetIn p t in
+ let accu = if RelDecl.is_local_assum p
+ then mkVar (NamedDecl.get_id decl) :: accu
+ else accu
+ in
+ shrink ctx sign c t accu
+| _ -> assert false
+
+let shrink_entry sign const =
+ let open Entries in
+ let typ = match const.const_entry_type with
+ | None -> assert false
+ | Some t -> t
+ in
+ (** The body has been forced by the call to [build_constant_by_tactic] *)
+ let () = assert (Future.is_over const.const_entry_body) in
+ let ((body, uctx), eff) = Future.force const.const_entry_body in
+ let (body, typ, ctx) = decompose (List.length sign) body typ [] in
+ let (body, typ, args) = shrink ctx sign body typ [] in
+ let const = { const with
+ const_entry_body = Future.from_val ((body, uctx), eff);
+ const_entry_type = Some typ;
+ } in
+ (const, args)
+
+let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
+ let open Tacticals.New in
+ let open Tacmach.New in
+ let open Proofview.Notations in
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let current_sign = Global.named_context_val ()
+ and global_sign = Proofview.Goal.hyps gl in
+ let evdref = ref sigma in
+ let sign,secsign =
+ List.fold_right
+ (fun d (s1,s2) ->
+ let id = NamedDecl.get_id d in
+ if mem_named_context_val id current_sign &&
+ interpretable_as_section_decl env evdref (lookup_named_val id current_sign) d
+ then (s1,push_named_context_val d s2)
+ else (Context.Named.add d s1,s2))
+ global_sign (Context.Named.empty, Environ.empty_named_context_val) in
+ let id = Namegen.next_global_ident_away id (pf_ids_set_of_hyps gl) in
+ let concl = match goal_type with
+ | None -> Proofview.Goal.concl gl
+ | Some ty -> ty in
+ let concl = it_mkNamedProd_or_LetIn concl sign in
+ let concl =
+ try flush_and_check_evars !evdref concl
+ with Uninstantiated_evar _ ->
+ CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.") in
+
+ let evd, ctx, concl =
+ (* FIXME: should be done only if the tactic succeeds *)
+ let evd = Evd.minimize_universes !evdref in
+ let ctx = Evd.universe_context_set evd in
+ evd, ctx, Evarutil.nf_evars_universes evd concl
+ in
+ let concl = EConstr.of_constr concl in
+ let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
+ let ectx = Evd.evar_universe_context evd in
+ let (const, safe, ectx) =
+ try Pfedit.build_constant_by_tactic ~goal_kind:gk id ectx 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)
+ in
+ let const, args = shrink_entry sign const in
+ let args = List.map EConstr.of_constr args in
+ let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in
+ let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in
+ let cst () =
+ (** do not compute the implicit arguments, it may be costly *)
+ let () = Impargs.make_implicit_args false in
+ (** ppedrot: seems legit to have abstracted subproofs as local*)
+ Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl
+ in
+ let cst = Impargs.with_implicit_protection cst () in
+ let inst = match const.Entries.const_entry_universes with
+ | Entries.Monomorphic_const_entry _ -> EInstance.empty
+ | Entries.Polymorphic_const_entry ctx ->
+ (** We mimick what the kernel does, that is ensuring that no additional
+ constraints appear in the body of polymorphic constants. Ideally this
+ should be enforced statically. *)
+ let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in
+ let () = assert (Univ.ContextSet.is_empty body_uctx) in
+ EInstance.make (Univ.UContext.instance ctx)
+ in
+ let lem = mkConstU (cst, inst) in
+ let evd = Evd.set_universe_context evd ectx in
+ let open Safe_typing in
+ let eff = private_con_of_con (Global.safe_env ()) cst in
+ let effs = concat_private eff
+ Entries.(snd (Future.force const.const_entry_body)) in
+ let solve =
+ Proofview.tclEFFECTS effs <*>
+ tacK lem args
+ in
+ let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac
+ end
+
+let abstract_subproof ~opaque id gk tac =
+ cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> Tactics.exact_no_check (applist (lem, args)))
+
+let anon_id = Id.of_string "anonymous"
+
+let name_op_to_name name_op object_kind suffix =
+ let open Proof_global in
+ let default_gk = (Global, false, object_kind) in
+ let name, gk = match Proof_global.V82.get_current_initial_conclusions () with
+ | (id, (_, gk)) -> Some id, gk
+ | exception NoCurrentProof -> None, default_gk
+ in
+ match name_op with
+ | Some s -> s, gk
+ | None ->
+ let name = Option.default anon_id name in
+ Nameops.add_suffix name suffix, gk
+
+let tclABSTRACT ?(opaque=true) name_op tac =
+ let s, gk = if opaque
+ then name_op_to_name name_op (Proof Theorem) "_subproof"
+ else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
+ abstract_subproof ~opaque s gk tac
diff --git a/tactics/abstract.mli b/tactics/abstract.mli
new file mode 100644
index 0000000000..7fb671fbf8
--- /dev/null
+++ b/tactics/abstract.mli
@@ -0,0 +1,16 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open EConstr
+
+val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
+
+val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
diff --git a/tactics/auto.ml b/tactics/auto.ml
index d7de6c4fb5..65b2615b6b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -416,6 +416,7 @@ and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
"nocore" amongst the databases. *)
let trivial ?(debug=Off) lems dbnames =
+ Hints.wrap_hint_warning @@
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
@@ -427,6 +428,7 @@ let trivial ?(debug=Off) lems dbnames =
end
let full_trivial ?(debug=Off) lems =
+ Hints.wrap_hint_warning @@
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
@@ -501,6 +503,7 @@ let search d n mod_delta db_list local_db =
let default_search_depth = ref 5
let delta_auto debug mod_delta n lems dbnames =
+ Hints.wrap_hint_warning @@
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
@@ -524,6 +527,7 @@ let new_auto ?(debug=Off) n = delta_auto debug true n
let default_auto = auto !default_search_depth [] []
let delta_full_auto ?(debug=Off) mod_delta n lems =
+ Hints.wrap_hint_warning @@
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 8e296de617..76cbdee0d5 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -226,7 +226,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,ty) in
let eqclause =
if metas then eqclause
- else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
+ else fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd))
in
let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in
let rec split_last_two = function
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 3456d13bbe..81cf9289d1 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -494,15 +494,15 @@ let top_sort evm undefs =
let tosee = ref undefs in
let rec visit ev evi =
let evs = Evarutil.undefined_evars_of_evar_info evm evi in
- tosee := Evar.Map.remove ev !tosee;
+ tosee := Evar.Set.remove ev !tosee;
Evar.Set.iter (fun ev ->
- if Evar.Map.mem ev !tosee then
- visit ev (Evar.Map.find ev !tosee)) evs;
+ if Evar.Set.mem ev !tosee then
+ visit ev (Evd.find evm ev)) evs;
l' := ev :: !l';
in
- while not (Evar.Map.is_empty !tosee) do
- let ev, evi = Evar.Map.min_binding !tosee in
- visit ev evi
+ while not (Evar.Set.is_empty !tosee) do
+ let ev = Evar.Set.choose !tosee in
+ visit ev (Evd.find evm ev)
done;
List.rev !l'
@@ -512,15 +512,9 @@ let top_sort evm undefs =
*)
let evars_to_goals p evm =
- let goals = ref Evar.Map.empty in
- let map ev evi =
- let evi, goal = p evm ev evi in
- let () = if goal then goals := Evar.Map.add ev evi !goals in
- evi
- in
- let evm = Evd.raw_map_undefined map evm in
- if Evar.Map.is_empty !goals then None
- else Some (!goals, evm)
+ let goals, nongoals = Evar.Set.partition (p evm) (Evd.get_typeclass_evars evm) in
+ if Evar.Set.is_empty goals then None
+ else Some (goals, nongoals)
(** Making local hints *)
let make_resolve_hyp env sigma st flags only_classes pri decl =
@@ -641,14 +635,6 @@ module Search = struct
occur_existential evd concl
else true
- let mark_unresolvables sigma goals =
- List.fold_left
- (fun sigma gl ->
- let evi = Evd.find_undefined sigma gl in
- let evi' = Typeclasses.mark_unresolvable evi in
- Evd.add sigma gl evi')
- sigma goals
-
(** The general hint application tactic.
tac1 + tac2 .... The choice of OR or ORELSE is determined
depending on the dependencies of the goal and the unique/Prop
@@ -693,8 +679,9 @@ module Search = struct
let msg =
match fst ie with
| Pretype_errors.PretypeError (env, evd, Pretype_errors.CannotUnify (x,y,_)) ->
- str"Cannot unify " ++ print_constr_env env evd x ++ str" and " ++
- print_constr_env env evd y
+ str"Cannot unify " ++
+ Printer.pr_econstr_env env evd x ++ str" and " ++
+ Printer.pr_econstr_env env evd y
| ReachedLimitEx -> str "Proof-search reached its limit."
| NoApplicableEx -> str "Proof-search failed."
| e -> CErrors.iprint ie
@@ -778,7 +765,7 @@ module Search = struct
shelve_goals shelved <*>
(if List.is_empty goals then tclUNIT ()
else
- let sigma' = mark_unresolvables sigma goals in
+ let sigma' = make_unresolvables (fun x -> List.mem_f Evar.equal x goals) sigma in
with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state goals)) >>=
fun s -> result s i (Some (Option.default 0 k + j)))
end
@@ -934,17 +921,21 @@ module Search = struct
| Some i -> str ", with depth limit " ++ int i));
tac
+ let eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints =
+ Hints.wrap_hint_warning @@ eauto_tac ?st ?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, evm') ->
+ | Some (goals, nongoals) ->
let goals =
if !typeclasses_dependency_order then
- top_sort evm' goals
- else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals)
+ top_sort evm goals
+ else Evar.Set.elements goals
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.init evm [] in
let pv = Proofview.unshelve goals pv in
try
let (), pv', (unsafe, shelved, gaveup), _ =
@@ -963,7 +954,13 @@ module Search = struct
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')
+ 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
with Logic_monad.TacticFailure _ -> raise Not_found
@@ -1015,7 +1012,7 @@ let deps_of_constraints cstrs evm p =
let evar_dependencies pred evm p =
Evd.fold_undefined
(fun ev evi _ ->
- if Typeclasses.is_resolvable evi && pred evm ev evi then
+ if Evd.is_typeclass_evar evm ev && pred evm ev evi then
let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
in Intpart.union_set evars p
else ())
@@ -1031,8 +1028,7 @@ let split_evars pred evm =
let is_inference_forced p evd ev =
try
- let evi = Evd.find_undefined evd ev in
- if Typeclasses.is_resolvable evi && snd (p ev evi)
+ if Evar.Set.mem ev (Evd.get_typeclass_evars evd) && p ev
then
let (loc, k) = evar_source ev evd in
match k with
@@ -1064,55 +1060,32 @@ let error_unresolvable env comp evd =
Pretype_errors.unsatisfiable_constraints env evd ev comp
(** Check if an evar is concerned by the current resolution attempt,
- (and in particular is in the current component), and also update
- its evar_info.
- Invariant : this should only be applied to undefined evars,
- and return undefined evar_info *)
+ (and in particular is in the current component).
+ Invariant : this should only be applied to undefined evars. *)
-let select_and_update_evars p oevd in_comp evd ev evi =
- assert (evi.evar_body == Evar_empty);
+let select_and_update_evars p oevd in_comp evd ev =
try
- let oevi = Evd.find_undefined oevd ev in
- if Typeclasses.is_resolvable oevi then
- Typeclasses.mark_unresolvable evi,
- (in_comp ev && p evd ev evi)
- else evi, false
- with Not_found ->
- Typeclasses.mark_unresolvable evi, p evd ev evi
+ if Evd.is_typeclass_evar oevd ev then
+ (in_comp ev && p evd ev (Evd.find evd ev))
+ else false
+ with Not_found -> false
(** Do we still have unresolved evars that should be resolved ? *)
let has_undefined p oevd evd =
- let check ev evi = snd (p oevd ev evi) in
+ let check ev evi = p oevd ev in
Evar.Map.exists check (Evd.undefined_map evd)
-(** Revert the resolvability status of evars after resolution,
- potentially unprotecting some evars that were set unresolvable
- just for this call to resolution. *)
-
-let revert_resolvability oevd evd =
- let map ev evi =
- try
- if not (Typeclasses.is_resolvable evi) then
- let evi' = Evd.find_undefined oevd ev in
- if Typeclasses.is_resolvable evi' then
- Typeclasses.mark_resolvable evi
- else evi
- else evi
- with Not_found -> evi
- in
- Evd.raw_map_undefined map evd
-
exception Unresolved
(** If [do_split] is [true], we try to separate the problem in
several components and then solve them separately *)
let resolve_all_evars debug depth unique env p oevd do_split fail =
- let split = if do_split then split_evars p oevd else [Evar.Set.empty] in
- let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true
- in
+ let tcs = Evd.get_typeclass_evars oevd in
+ let split = if do_split then split_evars p oevd else [tcs] in
+ let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true in
let rec docomp evd = function
- | [] -> revert_resolvability oevd evd
+ | [] -> evd
| comp :: comps ->
let p = select_and_update_evars p oevd (in_comp comp) in
try
@@ -1130,7 +1103,9 @@ let resolve_all_evars debug depth unique env p oevd do_split fail =
let initial_select_evars filter =
fun evd ev evi ->
- filter ev (snd evi.Evd.evar_source) &&
+ filter ev (Lazy.from_val (snd evi.Evd.evar_source)) &&
+ (** Typeclass evars can contain evars whose conclusion is not
+ yet determined to be a class or not. *)
Typeclasses.is_class_evar evd evi
let resolve_typeclass_evars debug depth unique env evd filter split fail =
@@ -1143,18 +1118,21 @@ let resolve_typeclass_evars debug depth unique env evd filter split fail =
(initial_select_evars filter) evd split fail
let solve_inst env evd filter unique split fail =
- resolve_typeclass_evars
+ let ((), sigma) = Hints.wrap_hint_warning_fun env evd begin fun evd ->
+ (), resolve_typeclass_evars
(get_typeclasses_debug ())
(get_typeclasses_depth ())
unique env evd filter split fail
+ end in
+ sigma
let _ =
Hook.set Typeclasses.solve_all_instances_hook solve_inst
let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
+ let (term, sigma) = Hints.wrap_hint_warning_fun env sigma begin fun sigma ->
let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in
- let (gl,t,sigma) =
- Goal.V82.mk_goal sigma nc gl Store.empty in
+ let (gl,t,sigma) = Goal.V82.mk_goal sigma nc gl in
let (ev, _) = destEvar sigma t in
let gls = { it = gl ; sigma = sigma; } in
let hints = searchtable_map typeclasses_db in
@@ -1169,7 +1147,9 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
let evd = sig_sig gls' in
let t' = mkEvar (ev, Array.of_list subst) in
let term = Evarutil.nf_evar evd t' in
- evd, term
+ term, evd
+ end in
+ (sigma, term)
let _ =
Hook.set Typeclasses.solve_one_instance_hook
@@ -1205,6 +1185,7 @@ let is_ground c =
let autoapply c i =
let open Proofview.Notations in
+ Hints.wrap_hint_warning @@
Proofview.Goal.enter begin fun gl ->
let hintdb = try Hints.searchtable_map i with Not_found ->
CErrors.user_err (Pp.str ("Unknown hint database " ^ i ^ "."))
@@ -1216,5 +1197,6 @@ let autoapply c i =
unify_e_resolve false flags gl
((c,cty,Univ.ContextSet.empty),0,ce) <*>
Proofview.tclEVARMAP >>= (fun sigma ->
- let sigma = Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals sigma in
+ let sigma = Typeclasses.make_unresolvables
+ (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
Proofview.Unsafe.tclEVARS sigma) end
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index e12063fd44..bd95a62532 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -12,7 +12,6 @@ open Constr
open EConstr
open Hipattern
open Tactics
-open Coqlib
open Reductionops
open Proofview.Notations
@@ -33,8 +32,8 @@ let absurd c =
let sigma, j = Coercion.inh_coerce_to_sort env sigma j in
let t = j.Environ.utj_val in
Proofview.Unsafe.tclEVARS sigma <*>
- Tacticals.New.pf_constr_of_global (build_coq_not ()) >>= fun coqnot ->
- Tacticals.New.pf_constr_of_global (build_coq_False ()) >>= fun coqfalse ->
+ Tacticals.New.pf_constr_of_global (Coqlib.(lib_ref "core.not.type")) >>= fun coqnot ->
+ Tacticals.New.pf_constr_of_global (Coqlib.(lib_ref "core.False.type")) >>= fun coqfalse ->
Tacticals.New.tclTHENLIST [
elim_type coqfalse;
Simple.apply (mk_absurd_proof coqnot t)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 80d07c5c03..5067315d08 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -409,7 +409,7 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
(* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *)
let eauto_with_bases ?(debug=Off) np lems db_list =
- tclTRY (e_search_auto debug np lems db_list)
+ Proofview.V82.of_tactic (Hints.wrap_hint_warning (Proofview.V82.tactic (tclTRY (e_search_auto debug np lems db_list))))
let eauto ?(debug=Off) np lems dbnames =
let db_list = make_db_list dbnames in
@@ -420,8 +420,8 @@ let full_eauto ?(debug=Off) n lems gl =
tclTRY (e_search_auto debug n lems db_list) gl
let gen_eauto ?(debug=Off) np lems = function
- | None -> Proofview.V82.tactic (full_eauto ~debug np lems)
- | Some l -> Proofview.V82.tactic (eauto ~debug np lems l)
+ | None -> Hints.wrap_hint_warning (Proofview.V82.tactic (full_eauto ~debug np lems))
+ | Some l -> Hints.wrap_hint_warning (Proofview.V82.tactic (eauto ~debug np lems l))
let make_depth = function
| None -> !default_search_depth
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 832014a610..6388aa2c33 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -27,7 +27,6 @@ open Constr_matching
open Hipattern
open Proofview.Notations
open Tacmach.New
-open Coqlib
open Tactypes
(* This file containts the implementation of the tactics ``Decide
@@ -73,11 +72,10 @@ let choose_noteq eqonleft =
let generalize_right mk typ c1 c2 =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let store = Proofview.Goal.extra gl in
Refine.refine ~typecheck:false begin fun sigma ->
let na = Name (next_name_away_with_default "x" Anonymous (Termops.vars_of_env env)) in
let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in
- let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in
+ let (sigma, x) = Evarutil.new_evar env sigma ~principal:true newconcl in
(sigma, mkApp (x, [|c2|]))
end
end
@@ -269,9 +267,10 @@ let decideEquality rectype ops =
(* The tactic Compare *)
let compare c1 c2 =
- pf_constr_of_global (build_coq_sumbool ()) >>= fun opc ->
- pf_constr_of_global (Coqlib.build_coq_eq ()) >>= fun eqc ->
- pf_constr_of_global (build_coq_not ()) >>= fun notc ->
+ let open Coqlib in
+ pf_constr_of_global (lib_ref "core.sumbool.type") >>= fun opc ->
+ 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 ops = (opc,eqc,notc) in
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index ea5ff4a6cb..b12018cd66 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -99,7 +99,7 @@ let my_it_mkLambda_or_LetIn_name s c =
let get_coq_eq ctx =
try
- let eq = Globnames.destIndRef Coqlib.glob_eq in
+ let eq = Globnames.destIndRef (Coqlib.lib_ref "core.eq.type") in
(* Do not force the lazy if they are not defined *)
let eq, ctx = with_context_set ctx
(UnivGen.fresh_inductive_instance (Global.env ()) eq) in
@@ -785,7 +785,7 @@ let build_congr env (eq,refl,ctx) ind =
let varH = fresh env (Id.of_string "H") in
let varf = fresh env (Id.of_string "f") in
let ci = make_case_info (Global.env()) ind RegularStyle in
- let uni, ctx = UnivGen.extend_context (UnivGen.new_global_univ ()) ctx in
+ let uni, ctx = Univ.extend_in_context_set (UnivGen.new_global_univ ()) ctx in
let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in
let c =
my_it_mkLambda_or_LetIn paramsctxt
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d0f4b2c680..c4a6b1605d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -339,12 +339,17 @@ let jmeq_same_dom env sigma = function
let find_elim hdcncl lft2rgt dep cls ot =
Proofview.Goal.enter_one begin fun gl ->
let sigma = project gl in
- let is_global gr c = Termops.is_global sigma gr c in
+ let is_global_exists gr c =
+ Coqlib.has_ref gr && Termops.is_global sigma (Coqlib.lib_ref gr) c
+ in
let inccl = Option.is_empty cls in
let env = Proofview.Goal.env gl in
- if (is_global Coqlib.glob_eq hdcncl ||
- (is_global Coqlib.glob_jmeq hdcncl &&
- jmeq_same_dom env sigma ot)) && not dep
+ (* if (is_global Coqlib.glob_eq hdcncl || *)
+ (* (is_global Coqlib.glob_jmeq hdcncl && *)
+ (* jmeq_same_dom env sigma ot)) && not dep *)
+ if (is_global_exists "core.eq.type" hdcncl ||
+ (is_global_exists "core.JMeq.type" hdcncl
+ && jmeq_same_dom env sigma ot)) && not dep
then
let c =
match EConstr.kind sigma hdcncl with
@@ -356,9 +361,9 @@ let find_elim hdcncl lft2rgt dep cls ot =
| Some true, None
| Some false, Some _ ->
let c1 = destConstRef pr1 in
- let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical c1)) in
+ let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in
let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in
- let c1' = Global.constant_of_delta_kn (KerName.make mp dp l') in
+ let c1' = Global.constant_of_delta_kn (KerName.make mp l') in
begin
try
let _ = Global.lookup_constant c1' in
@@ -588,7 +593,7 @@ let classes_dirpath =
let init_setoid () =
if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
- else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]
+ else check_required_library ["Coq";"Setoids";"Setoid"]
let check_setoid cl =
Option.fold_left
@@ -637,8 +642,8 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
| None ->
tclFAIL 0 (str"Terms do not have convertible types")
| Some evd ->
- let e = build_coq_eq () in
- let sym = build_coq_eq_sym () in
+ let e = lib_ref "core.eq.type" in
+ let sym = lib_ref "core.eq.sym" in
Tacticals.New.pf_constr_of_global sym >>= fun sym ->
Tacticals.New.pf_constr_of_global e >>= fun e ->
let eq = applist (e, [t1;c1;c2]) in
@@ -930,9 +935,9 @@ let build_selector env sigma dirn c ind special default =
let ans = Inductiveops.make_case_or_project env sigma indf ci p c (Array.of_list brl) in
ans
-let build_coq_False () = pf_constr_of_global (build_coq_False ())
-let build_coq_True () = pf_constr_of_global (build_coq_True ())
-let build_coq_I () = pf_constr_of_global (build_coq_I ())
+let build_coq_False () = pf_constr_of_global (lib_ref "core.False.type")
+let build_coq_True () = pf_constr_of_global (lib_ref "core.True.type")
+let build_coq_I () = pf_constr_of_global (lib_ref "core.True.I")
let rec build_discriminator env sigma true_0 false_0 dirn c = function
| [] ->
@@ -1320,15 +1325,15 @@ let inject_if_homogenous_dependent_pair ty =
let sigma = Tacmach.New.project gl in
let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
(* fetch the informations of the pair *)
- let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
- let existTconstr () = (Coqlib.build_sigma_type()).Coqlib.intro in
+ 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 (Termops.is_global 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 (Termops.is_global sigma existTconstr hd1) then raise Exit;
+ if not (Termops.is_global 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 *)
@@ -1336,17 +1341,16 @@ let inject_if_homogenous_dependent_pair ty =
(* knows inductive types *)
if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind &&
pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
- Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
+ check_required_library ["Coq";"Logic";"Eqdep_dec"];
let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
- let inj2 = Coqlib.coq_reference "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"]
- "inj_pair2_eq_dec" 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 *)
tclTHENLIST
[Proofview.tclEFFECTS eff;
intro;
onLastHyp (fun hyp ->
- Tacticals.New.pf_constr_of_global Coqlib.glob_eq >>= fun ceq ->
+ Tacticals.New.pf_constr_of_global Coqlib.(lib_ref "core.eq.type") >>= fun ceq ->
tclTHENS (cut (mkApp (ceq,new_eq_args)))
[clear [destVar sigma hyp];
Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 ->
@@ -1671,8 +1675,8 @@ let _ =
optwrite = (:=) regular_subst_tactic }
let restrict_to_eq_and_identity eq = (* compatibility *)
- if not (is_global glob_eq eq) &&
- not (is_global glob_identity eq)
+ if not (is_global (lib_ref "core.eq.type") eq) &&
+ not (is_global (lib_ref "core.identity.type") eq)
then raise Constr_matching.PatternMatchingFailure
exception FoundHyp of (Id.t * constr * bool)
@@ -1788,7 +1792,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
try
let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
let u = EInstance.kind sigma u in
- let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
+ let eq = Constr.mkRef (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
match EConstr.kind sigma x, EConstr.kind sigma y with
| Var z, _ when not (is_evaluable env (EvalVarRef z)) ->
@@ -1839,7 +1843,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
try
let lbeq,u,(_,x,y) = find_eq_data_decompose c in
let u = EInstance.kind sigma u in
- let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
+ let eq = Constr.mkRef (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
if EConstr.eq_constr sigma x y then failwith "caught";
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 3835dee299..2f2d32e887 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -209,14 +209,14 @@ let fresh_key =
let cur = incr id; !id in
let lbl = Id.of_string ("_" ^ string_of_int cur) in
let kn = Lib.make_kn lbl in
- let (mp, dir, _) = KerName.repr kn in
+ let (mp, _) = KerName.repr kn in
(** We embed the full path of the kernel name in the label so that the
identifier should be unique. This ensures that including two modules
together won't confuse the corresponding labels. *)
- let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i"
- (ModPath.to_string mp) (DirPath.to_string dir) cur)
+ let lbl = Id.of_string_soft (Printf.sprintf "%s#%i"
+ (ModPath.to_string mp) cur)
in
- KerName.make mp dir (Label.of_id lbl)
+ KerName.make mp (Label.of_id lbl)
let pri_order_int (id1, {pri=pri1}) (id2, {pri=pri2}) =
let d = pri1 - pri2 in
@@ -787,7 +787,7 @@ let secvars_of_constr env sigma c =
secvars_of_idset (Termops.global_vars_set env sigma c)
let secvars_of_global env gr =
- secvars_of_idset (vars_of_global_reference env gr)
+ secvars_of_idset (vars_of_global env gr)
let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
let secvars = secvars_of_constr env sigma c in
@@ -942,7 +942,7 @@ let make_extern pri pat tacast =
let make_mode ref m =
let open Term in
- let ty, _ = Global.type_of_global_in_context (Global.env ()) ref in
+ let ty, _ = Typeops.type_of_global_in_context (Global.env ()) ref in
let ctx, t = decompose_prod ty in
let n = List.length ctx in
let m' = Array.of_list m in
@@ -1292,13 +1292,13 @@ let project_hint ~poly pri l2r r =
let sigma, c = Evd.fresh_global env sigma gr in
let t = Retyping.get_type_of env sigma c in
let t =
- Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in
+ Tacred.reduce_to_quantified_ref env sigma (lib_ref "core.iff.type") t in
let sign,ccl = decompose_prod_assum sigma t in
let (a,b) = match snd (decompose_app sigma ccl) with
| [a;b] -> (a,b)
| _ -> assert false in
let p =
- if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
+ if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in
let sigma, p = Evd.fresh_global env sigma p in
let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
let c = it_mkLambda_or_LetIn
@@ -1552,11 +1552,6 @@ let pr_hint_db_env env sigma db =
hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++
content
-(* Deprecated in the mli *)
-let pr_hint_db db =
- let sigma, env = Pfedit.get_current_context () in
- pr_hint_db_env env sigma db
-
let pr_hint_db_by_name env sigma dbname =
try
let db = searchtable_map dbname in pr_hint_db_env env sigma db
@@ -1579,25 +1574,76 @@ let print_mp mp =
let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true
+let hint_trace = Evd.Store.field ()
+
+let log_hint h =
+ let open Proofview.Notations in
+ Proofview.tclEVARMAP >>= fun sigma ->
+ let store = get_extra_data sigma in
+ match Store.get store hint_trace with
+ | None ->
+ (** All calls to hint logging should be well-scoped *)
+ assert false
+ | Some trace ->
+ let trace = KNmap.add h.uid h trace in
+ let store = Store.set store hint_trace trace in
+ Proofview.Unsafe.tclEVARS (set_extra_data store sigma)
+
let warn_non_imported_hint =
CWarnings.create ~name:"non-imported-hint" ~category:"automation"
(fun (hint,mp) ->
strbrk "Hint used but not imported: " ++ hint ++ print_mp mp)
-let warn h x =
- let open Proofview in
- tclBIND tclENV (fun env ->
- tclBIND tclEVARMAP (fun sigma ->
- let hint = pr_hint env sigma h in
- let (mp, _, _) = KerName.repr h.uid in
- warn_non_imported_hint (hint,mp);
- Proofview.tclUNIT x))
+let warn env sigma h =
+ let hint = pr_hint env sigma h in
+ let mp = KerName.modpath h.uid in
+ warn_non_imported_hint (hint,mp)
+
+let wrap_hint_warning t =
+ let open Proofview.Notations in
+ Proofview.tclEVARMAP >>= fun sigma ->
+ let store = get_extra_data sigma in
+ let old = Store.get store hint_trace in
+ let store = Store.set store hint_trace KNmap.empty in
+ Proofview.Unsafe.tclEVARS (set_extra_data store sigma) >>= fun () ->
+ t >>= fun ans ->
+ Proofview.tclENV >>= fun env ->
+ Proofview.tclEVARMAP >>= fun sigma ->
+ let store = get_extra_data sigma in
+ let hints = match Store.get store hint_trace with
+ | None -> assert false
+ | Some hints -> hints
+ in
+ let () = KNmap.iter (fun _ h -> warn env sigma h) hints in
+ let store = match old with
+ | None -> Store.remove store hint_trace
+ | Some v -> Store.set store hint_trace v
+ in
+ Proofview.Unsafe.tclEVARS (set_extra_data store sigma) >>= fun () ->
+ Proofview.tclUNIT ans
+
+let wrap_hint_warning_fun env sigma t =
+ let store = get_extra_data sigma in
+ let old = Store.get store hint_trace in
+ let store = Store.set store hint_trace KNmap.empty in
+ let (ans, sigma) = t (set_extra_data store sigma) in
+ let store = get_extra_data sigma in
+ let hints = match Store.get store hint_trace with
+ | None -> assert false
+ | Some hints -> hints
+ in
+ let () = KNmap.iter (fun _ h -> warn env sigma h) hints in
+ let store = match old with
+ | None -> Store.remove store hint_trace
+ | Some v -> Store.set store hint_trace v
+ in
+ (ans, set_extra_data store sigma)
let run_hint tac k = match !warn_hint with
| `LAX -> k tac.obj
| `WARN ->
if is_imported tac then k tac.obj
- else Proofview.tclBIND (k tac.obj) (fun x -> warn tac x)
+ else Proofview.tclTHEN (log_hint tac) (k tac.obj)
| `STRICT ->
if is_imported tac then k tac.obj
else Proofview.tclZERO (UserError (None, (str "Tactic failure.")))
diff --git a/tactics/hints.mli b/tactics/hints.mli
index c49ca2094a..6db8feccd0 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -282,6 +282,15 @@ val make_db_list : hint_db_name list -> hint_db list
val typeclasses_db : hint_db_name
val rewrite_db : hint_db_name
+val wrap_hint_warning : 'a Proofview.tactic -> 'a Proofview.tactic
+(** Use around toplevel calls to hint-using tactics, to enable the tracking of
+ non-imported hints. Any tactic calling [run_hint] must be wrapped this
+ way. *)
+
+val wrap_hint_warning_fun : env -> evar_map ->
+ (evar_map -> 'a * evar_map) -> 'a * evar_map
+(** Variant of the above for non-tactics *)
+
(** Printing hints *)
val pr_searchtable : env -> evar_map -> Pp.t
@@ -289,9 +298,4 @@ val pr_applicable_hint : unit -> Pp.t
val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
-val pr_hint_db : Hint_db.t -> Pp.t
-[@@ocaml.deprecated "please used pr_hint_db_env"]
val pr_hint : env -> evar_map -> hint -> Pp.t
-
-type nonrec hint_info = hint_info
-[@@ocaml.deprecated "Use [Typeclasses.hint_info]"]
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 7da059ae35..708412720a 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -289,24 +289,22 @@ let coq_refl_jm_pattern =
mkPattern (mkGProd "A" mkGHole (mkGProd "x" (mkGVar "A")
(mkGApp mkGHole [mkGVar "A"; mkGVar "x"; mkGVar "A"; mkGVar "x";])))
-open Globnames
-
let match_with_equation env sigma t =
if not (isApp sigma t) then raise NoEquationFound;
let (hdapp,args) = destApp sigma t in
match EConstr.kind sigma hdapp with
| Ind (ind,u) ->
- if GlobRef.equal (IndRef ind) glob_eq then
- Some (build_coq_eq_data()),hdapp,
- PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if GlobRef.equal (IndRef ind) glob_identity then
- Some (build_coq_identity_data()),hdapp,
- PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if GlobRef.equal (IndRef ind) glob_jmeq then
- Some (build_coq_jmeq_data()),hdapp,
- HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
- else
- let (mib,mip) = Global.lookup_inductive ind in
+ if Coqlib.check_ind_ref "core.eq.type" ind then
+ Some (build_coq_eq_data()),hdapp,
+ PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+ else if Coqlib.check_ind_ref "core.identity.type" ind then
+ Some (build_coq_identity_data()),hdapp,
+ PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+ else if Coqlib.check_ind_ref "core.JMeq.type" ind then
+ Some (build_coq_jmeq_data()),hdapp,
+ HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
+ else
+ let (mib,mip) = Global.lookup_inductive ind in
let constr_types = mip.mind_nf_lc in
let nconstr = Array.length mip.mind_consnames in
if Int.equal nconstr 1 then
@@ -438,12 +436,12 @@ let match_eq sigma eqn (ref, hetero) =
| _ -> raise PatternMatchingFailure
let no_check () = true
-let check_jmeq_loaded () = Library.library_is_loaded Coqlib.jmeq_module
+let check_jmeq_loaded () = has_ref "core.JMeq.type"
let equalities =
- [(coq_eq_ref, false), no_check, build_coq_eq_data;
- (coq_jmeq_ref, true), check_jmeq_loaded, build_coq_jmeq_data;
- (coq_identity_ref, false), no_check, build_coq_identity_data]
+ [(lazy(lib_ref "core.eq.type"), false), no_check, build_coq_eq_data;
+ (lazy(lib_ref "core.JMeq.type"), true), check_jmeq_loaded, build_coq_jmeq_data;
+ (lazy(lib_ref "core.identity.type"), false), no_check, build_coq_identity_data]
let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *)
let d,k = first_match (match_eq sigma eqn) equalities in
@@ -478,9 +476,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 (Lazy.force coq_exist_ref) f ->
+ | App (f, [| a; p; car; cdr |]) when Termops.is_global 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 (Lazy.force coq_existT_ref) f ->
+ | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sigT.intro") f ->
build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr)
| _ -> raise PatternMatchingFailure
@@ -489,7 +487,7 @@ let find_sigma_data_decompose env ex = (* fails with PatternMatchingFailure *)
(* Pattern "(sig ?1 ?2)" *)
let coq_sig_pattern =
- lazy (mkPattern (mkGAppRef coq_sig_ref [mkGPatVar "X1"; mkGPatVar "X2"]))
+ lazy (mkPattern (mkGAppRef (lazy (lib_ref "core.sig.type")) [mkGPatVar "X1"; mkGPatVar "X2"]))
let match_sigma env sigma t =
match Id.Map.bindings (matches env sigma (Lazy.force coq_sig_pattern) t) with
@@ -507,44 +505,44 @@ let is_matching_sigma env sigma t = is_matching env sigma (Lazy.force coq_sig_pa
let coq_eqdec ~sum ~rev =
lazy (
- let eqn = mkGAppRef coq_eq_ref (List.map mkGPatVar ["X1"; "X2"; "X3"]) in
- let args = [eqn; mkGAppRef coq_not_ref [eqn]] in
+ let eqn = mkGAppRef (lazy (lib_ref "core.eq.type")) (List.map mkGPatVar ["X1"; "X2"; "X3"]) in
+ let args = [eqn; mkGAppRef (lazy (lib_ref "core.not.type")) [eqn]] in
let args = if rev then List.rev args else args in
mkPattern (mkGAppRef sum args)
)
+let sumbool_type = lazy (lib_ref "core.sumbool.type")
+let or_type = lazy (lib_ref "core.or.type")
+
(** [{ ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 }] *)
-let coq_eqdec_inf_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:false
+let coq_eqdec_inf_pattern = coq_eqdec ~sum:sumbool_type ~rev:false
(** [{ ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 }] *)
-let coq_eqdec_inf_rev_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:true
+let coq_eqdec_inf_rev_pattern = coq_eqdec ~sum:sumbool_type ~rev:true
(** %coq_or_ref (?X2 = ?X3 :> ?X1) (~ ?X2 = ?X3 :> ?X1) *)
-let coq_eqdec_pattern = coq_eqdec ~sum:coq_or_ref ~rev:false
+let coq_eqdec_pattern = coq_eqdec ~sum:or_type ~rev:false
(** %coq_or_ref (~ ?X2 = ?X3 :> ?X1) (?X2 = ?X3 :> ?X1) *)
-let coq_eqdec_rev_pattern = coq_eqdec ~sum:coq_or_ref ~rev:true
-
-let op_or = coq_or_ref
-let op_sum = coq_sumbool_ref
+let coq_eqdec_rev_pattern = coq_eqdec ~sum:or_type ~rev:true
let match_eqdec env sigma t =
let eqonleft,op,subst =
- try true,op_sum,matches env sigma (Lazy.force coq_eqdec_inf_pattern) t
+ try true,sumbool_type,matches env sigma (Lazy.force coq_eqdec_inf_pattern) t
with PatternMatchingFailure ->
- try false,op_sum,matches env sigma (Lazy.force coq_eqdec_inf_rev_pattern) t
+ try false,sumbool_type,matches env sigma (Lazy.force coq_eqdec_inf_rev_pattern) t
with PatternMatchingFailure ->
- try true,op_or,matches env sigma (Lazy.force coq_eqdec_pattern) t
+ try true,or_type,matches env sigma (Lazy.force coq_eqdec_pattern) t
with PatternMatchingFailure ->
- false,op_or,matches env sigma (Lazy.force coq_eqdec_rev_pattern) t in
+ false,or_type,matches env sigma (Lazy.force coq_eqdec_rev_pattern) t in
match Id.Map.bindings subst with
| [(_,typ);(_,c1);(_,c2)] ->
eqonleft, Lazy.force op, c1, c2, typ
| _ -> anomaly (Pp.str "Unexpected pattern.")
(* Patterns "~ ?" and "? -> False" *)
-let coq_not_pattern = lazy (mkPattern (mkGAppRef coq_not_ref [mkGHole]))
-let coq_imp_False_pattern = lazy (mkPattern (mkGArrow mkGHole (mkGRef coq_False_ref)))
+let coq_not_pattern = lazy (mkPattern (mkGAppRef (lazy (lib_ref "core.not.type")) [mkGHole]))
+let coq_imp_False_pattern = lazy (mkPattern (mkGArrow mkGHole (mkGRef (lazy (lib_ref "core.False.type")))))
let is_matching_not env sigma t = is_matching env sigma (Lazy.force coq_not_pattern) t
let is_matching_imp_False env sigma t = is_matching env sigma (Lazy.force coq_imp_False_pattern) t
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index e4013152e6..b81967c781 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -56,8 +56,7 @@ let subst_scheme (subst,(kind,l)) =
(kind,Array.Smart.map (subst_one_scheme subst) l)
let discharge_scheme (_,(kind,l)) =
- Some (kind,Array.map (fun (ind,const) ->
- (Lib.discharge_inductive ind,Lib.discharge_con const)) l)
+ Some (kind, l)
let inScheme : string * (inductive * Constant.t) array -> obj =
declare_object {(default_object "SCHEME") with
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 43786c8e19..6a39a10fc4 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -70,6 +70,11 @@ type inversion_kind =
| FullInversion
| FullInversionClear
+let evd_comb1 f evdref x =
+ let (evd',y) = f !evdref x in
+ evdref := evd';
+ y
+
let compute_eqn env sigma n i ai =
(mkRel (n-i),get_type_of env sigma (mkRel (n-i)))
@@ -94,7 +99,7 @@ let make_inv_predicate env evd indf realargs id status concl =
| Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*)
| None ->
let sort = get_sort_family_of env !evd concl in
- let sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd sort in
+ let sort = evd_comb1 Evd.fresh_sort_in_family evd sort in
let p = make_arity env !evd true indf sort in
let evd',(p,ptyp) = Unification.abstract_list_all env
!evd p concl (realargs@[mkVar id])
@@ -124,19 +129,19 @@ let make_inv_predicate env evd indf realargs id status concl =
evd := sigma; res
in
let eq_term = eqdata.Coqlib.eq in
- let eq = Evarutil.evd_comb1 (Evd.fresh_global env) evd eq_term in
+ let eq = evd_comb1 (Evd.fresh_global env) evd eq_term in
let eqn = applist (eq,[eqnty;lhs;rhs]) in
let eqns = (Anonymous, lift n eqn) :: eqns in
let refl_term = eqdata.Coqlib.refl in
- let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in
+ let refl_term = evd_comb1 (Evd.fresh_global env) evd refl_term in
let refl = mkApp (refl_term, [|eqnty; rhs|]) in
- let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in
+ let _ = evd_comb1 (Typing.type_of env) evd refl in
let args = refl :: args in
build_concl eqns args (succ n) restlist
in
let (newconcl, args) = build_concl [] [] 0 realargs in
let predicate = it_mkLambda_or_LetIn newconcl (name_context env !evd hyps) in
- let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in
+ let _ = evd_comb1 (Typing.type_of env) evd predicate in
(* OK - this predicate should now be usable by res_elimination_then to
do elimination on the conclusion. *)
predicate, args
@@ -345,7 +350,7 @@ let remember_first_eq id x = if !x == Logic.MoveLast then x := Logic.MoveAfter i
let dest_nf_eq env sigma t = match EConstr.kind sigma t with
| App (r, [| t; x; y |]) ->
let open Reductionops in
- let lazy eq = Coqlib.coq_eq_ref in
+ let eq = Coqlib.lib_ref "core.eq.type" in
if EConstr.is_global sigma eq r then
(t, whd_all env sigma x, whd_all env sigma y)
else user_err Pp.(str "Not an equality.")
@@ -495,7 +500,7 @@ let raw_inversion inv_kind id status names =
(* Error messages of the inversion tactics *)
let wrap_inv_error id = function (e, info) -> match e with
| Indrec.RecursionSchemeError
- (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Set as k),i)) ->
+ (_, Indrec.NotAllowedCaseAnalysis (_,(Type _ | Set as k),i)) ->
Proofview.tclENV >>= fun env ->
Proofview.tclEVARMAP >>= fun sigma ->
tclZEROMSG (
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 837865e644..f2cf915fe3 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -60,10 +60,6 @@ let tclIFTHENSELSE = Refiner.tclIFTHENSELSE
let tclIFTHENSVELSE = Refiner.tclIFTHENSVELSE
let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST
-(* Synonyms *)
-
-let tclTHENSEQ = tclTHENLIST
-
(************************************************************************)
(* Tacticals applying on hypotheses *)
(************************************************************************)
@@ -655,12 +651,11 @@ module New = struct
| _ ->
let name_elim =
match EConstr.kind sigma elim with
- | Const (kn, _) -> Constant.to_string kn
- | Var id -> Id.to_string id
- | _ -> "\b"
+ | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim
+ | _ -> mt ()
in
user_err ~hdr:"Tacticals.general_elim_then_using"
- (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
+ (str "The elimination combinator " ++ name_elim ++ str " is unknown.")
in
let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
let branchsigns = compute_constructor_signatures ~rec_flag ind in
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 1e66c2b0b1..cc15469d0e 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -23,8 +23,6 @@ val tclIDTAC_MESSAGE : Pp.t -> tactic
val tclORELSE0 : tactic -> tactic -> tactic
val tclORELSE : tactic -> tactic -> tactic
val tclTHEN : tactic -> tactic -> tactic
-val tclTHENSEQ : tactic list -> tactic
-[@@ocaml.deprecated "alias of Tacticals.tclTHENLIST"]
val tclTHENLIST : tactic list -> tactic
val tclTHEN_i : tactic -> (int -> tactic) -> tactic
val tclTHENFIRST : tactic -> tactic -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6999b17d8e..5cead11a5c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -8,8 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-module CVars = Vars
-
open Pp
open CErrors
open Util
@@ -36,7 +34,6 @@ open Refiner
open Tacticals
open Hipattern
open Coqlib
-open Decl_kinds
open Evarutil
open Indrec
open Pretype_errors
@@ -117,14 +114,14 @@ let _ =
(** This tactic creates a partial proof realizing the introduction rule, but
does not check anything. *)
-let unsafe_intro env store decl b =
+let unsafe_intro env decl b =
Refine.refine ~typecheck:false begin fun sigma ->
let ctx = named_context_val env in
let nctx = push_named_context_val decl ctx in
let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in
let ninst = mkRel 1 :: inst in
let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
- let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
+ let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ninst in
(sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) ev)
end
@@ -133,7 +130,6 @@ let introduction id =
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
let hyps = named_context_val (Proofview.Goal.env gl) in
- let store = Proofview.Goal.extra gl in
let env = Proofview.Goal.env gl in
let () = if mem_named_context_val id hyps then
user_err ~hdr:"Tactics.introduction"
@@ -141,8 +137,8 @@ let introduction id =
in
let open Context.Named.Declaration in
match EConstr.kind sigma concl with
- | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b
- | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b
+ | Prod (_, t, b) -> unsafe_intro env (LocalAssum (id, t)) b
+ | LetIn (_, c, t, b) -> unsafe_intro env (LocalDef (id, c, t)) b
| _ -> raise (RefinerError (env, sigma, IntroNeedsProduct))
end
@@ -152,7 +148,6 @@ let error msg = CErrors.user_err Pp.(str msg)
let convert_concl ?(check=true) ty k =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let store = Proofview.Goal.extra gl in
let conclty = Proofview.Goal.concl gl in
Refine.refine ~typecheck:false begin fun sigma ->
let sigma =
@@ -162,7 +157,7 @@ let convert_concl ?(check=true) ty k =
| None -> error "Not convertible."
| Some sigma -> sigma
end else sigma in
- let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty 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)
end
@@ -173,11 +168,10 @@ let convert_hyp ?(check=true) d =
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let ty = Proofview.Goal.concl gl in
- let store = Proofview.Goal.extra gl in
let sign = convert_hyp check (named_context_val env) sigma d in
let env = reset_with_named_context sign env in
Refine.refine ~typecheck:false begin fun sigma ->
- Evarutil.new_evar env sigma ~principal:true ~store ty
+ Evarutil.new_evar env sigma ~principal:true ty
end
end
@@ -284,12 +278,11 @@ let move_hyp id dest =
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let ty = Proofview.Goal.concl gl in
- let store = Proofview.Goal.extra gl in
let sign = named_context_val env in
let sign' = move_hyp_in_named_context env sigma id dest sign in
let env = reset_with_named_context sign' env in
Refine.refine ~typecheck:false begin fun sigma ->
- Evarutil.new_evar env sigma ~principal:true ~store ty
+ Evarutil.new_evar env sigma ~principal:true ty
end
end
@@ -313,7 +306,6 @@ let rename_hyp repl =
Proofview.Goal.enter begin fun gl ->
let hyps = Proofview.Goal.hyps gl in
let concl = Proofview.Goal.concl gl in
- let store = Proofview.Goal.extra gl in
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
(** Check that we do not mess variables *)
@@ -344,7 +336,7 @@ let rename_hyp repl =
let nctx = val_of_named_context nhyps in
let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
Refine.refine ~typecheck:false begin fun sigma ->
- Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance
+ Evarutil.new_evar_instance nctx sigma nconcl ~principal:true instance
end
end
@@ -445,13 +437,12 @@ let internal_cut_gen ?(check=true) dir replace id t =
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
- let store = Proofview.Goal.extra gl in
let sign = named_context_val env in
let sign',t,concl,sigma =
if replace then
let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in
let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
- let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in
+ let sign' = insert_decl_in_named_context env sigma (LocalAssum (id,t)) nexthyp sign' in
sign',t,concl,sigma
else
(if check && mem_named_context_val id sign then
@@ -464,10 +455,10 @@ let internal_cut_gen ?(check=true) dir replace id t =
let (sigma,ev,ev') =
if dir then
let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
- let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in
+ let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
(sigma,ev,ev')
else
- let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in
+ let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
(sigma,ev,ev') in
let term = mkLetIn (Name id, ev, t, EConstr.Vars.subst_var id ev') in
@@ -791,9 +782,9 @@ let e_change_in_hyp redfun (id,where) =
(convert_hyp c)
end
-type change_arg = Ltac_pretype.patvar_map -> evar_map -> evar_map * EConstr.constr
+type change_arg = Ltac_pretype.patvar_map -> env -> evar_map -> evar_map * EConstr.constr
-let make_change_arg c pats sigma = (sigma, replace_vars (Id.Map.bindings pats) c)
+let make_change_arg c pats env sigma = (sigma, replace_vars (Id.Map.bindings pats) c)
let check_types env sigma mayneedglobalcheck deep newc origc =
let t1 = Retyping.get_type_of env sigma newc in
@@ -818,7 +809,7 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
(* Now we introduce different instances of the previous tacticals *)
let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
- let (sigma, t') = t sigma in
+ let (sigma, t') = t env sigma in
let sigma = check_types env sigma mayneedglobalcheck deep t' c in
match infer_conv ~pb:cv_pb env sigma t' c with
| None -> user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
@@ -2102,11 +2093,10 @@ let keep hyps =
let apply_type ~typecheck newcl args =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let store = Proofview.Goal.extra gl in
Refine.refine ~typecheck begin fun sigma ->
let newcl = nf_betaiota env sigma newcl (* As in former Logic.refine *) in
let (sigma, ev) =
- Evarutil.new_evar env sigma ~principal:true ~store newcl in
+ Evarutil.new_evar env sigma ~principal:true newcl in
(sigma, applist (ev, args))
end
end
@@ -2120,13 +2110,12 @@ let bring_hyps hyps =
else
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let store = Proofview.Goal.extra gl in
let concl = Tacmach.New.pf_concl gl in
let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
let args = Array.of_list (Context.Named.to_instance mkVar hyps) in
Refine.refine ~typecheck:false begin fun sigma ->
let (sigma, ev) =
- Evarutil.new_evar env sigma ~principal:true ~store newcl in
+ Evarutil.new_evar env sigma ~principal:true newcl in
(sigma, mkApp (ev, args))
end
end
@@ -2668,7 +2657,7 @@ let mk_eq_name env id {CAst.loc;v=ido} =
(* unsafe *)
-let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
+let mkletin_goal env sigma with_eq dep (id,lastlhyp,ccl,c) ty =
let open Context.Named.Declaration in
let t = match ty with Some t -> t | _ -> typ_of env sigma c in
let decl = if dep then LocalDef (id,c,t)
@@ -2683,11 +2672,11 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
let eq = applist (eq,args) in
let refl = applist (refl, [t;mkVar id]) in
let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in
- let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in
+ let (sigma, x) = new_evar newenv sigma ~principal:true ccl in
(sigma, mkNamedLetIn id c t (mkNamedLetIn heq refl eq x))
| None ->
let newenv = insert_before [decl] lastlhyp env in
- let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in
+ let (sigma, x) = new_evar newenv sigma ~principal:true ccl in
(sigma, mkNamedLetIn id c t x)
let pose_tac na c =
@@ -3552,12 +3541,13 @@ let error_ind_scheme s =
let s = if not (String.is_empty s) then s^" " else s in
user_err ~hdr:"Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
-let coq_eq sigma = Evarutil.new_global sigma (Coqlib.build_coq_eq ())
-let coq_eq_refl sigma = Evarutil.new_global sigma (Coqlib.build_coq_eq_refl ())
+let coq_eq sigma = Evarutil.new_global sigma Coqlib.(lib_ref "core.eq.type")
+let coq_eq_refl sigma = Evarutil.new_global sigma Coqlib.(lib_ref "core.eq.refl")
-let coq_heq_ref = lazy (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq")
+let coq_heq_ref = lazy (Coqlib.lib_ref "core.JMeq.type")
let coq_heq sigma = Evarutil.new_global sigma (Lazy.force coq_heq_ref)
-let coq_heq_refl sigma = Evarutil.new_global sigma (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
+let coq_heq_refl sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.JMeq.refl")
+(* let coq_heq_refl = lazy (glob (lib_ref "core.JMeq.refl")) *)
let mkEq sigma t x y =
let sigma, eq = coq_eq sigma in
@@ -3789,7 +3779,7 @@ let abstract_args gl generalize_vars dep id defined f args =
let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
let open Context.Named.Declaration in
Proofview.Goal.enter begin fun gl ->
- Coqlib.check_required_library Coqlib.jmeq_module_name;
+ Coqlib.(check_required_library jmeq_module_name);
let sigma = Tacmach.New.project gl in
let (f, args, def, id, oldid) =
let oldid = Tacmach.New.pf_get_new_id id gl in
@@ -3849,7 +3839,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 (Lazy.force coq_eq_ref) eq ->
+ | App (eq, [| eqty; x; y |]) when EConstr.is_global !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
@@ -4107,12 +4097,15 @@ let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info =
let guess_elim isrec dep s hyp0 gl =
let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
let (mind, u), _ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in
- let evd, elimc =
- if isrec && not (is_nonrec mind) then find_ind_eliminator mind s gl
+ let env = Tacmach.New.pf_env gl in
+ let sigma = Tacmach.New.project gl in
+ let sigma, elimc =
+ if isrec && not (is_nonrec mind)
+ then
+ let gr = lookup_eliminator mind s in
+ Evd.fresh_global env sigma gr
else
- let env = Tacmach.New.pf_env gl in
- let sigma = Tacmach.New.project gl in
- let u = EInstance.kind (Tacmach.New.project gl) u in
+ let u = EInstance.kind sigma u in
if dep then
let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in
let ind = EConstr.of_constr ind in
@@ -4122,8 +4115,8 @@ let guess_elim isrec dep s hyp0 gl =
let ind = EConstr.of_constr ind in
(sigma, ind)
in
- let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
- evd, ((elimc, NoBindings), elimt), mkIndU (mind, u)
+ let elimt = Typing.unsafe_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
@@ -4430,7 +4423,6 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let ccl = Proofview.Goal.concl gl in
- let store = Proofview.Goal.extra gl in
let check = check_enough_applied env sigma elim in
let (sigma', c) = use_bindings env sigma elim false (c0,lbind) t0 in
let abs = AbstractPattern (from_prefix,check,Name id,(pending,c),cls,false) in
@@ -4456,7 +4448,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
let b = not with_evars && with_eq != None in
let (sigma, c) = use_bindings env sigma elim b (c0,lbind) t0 in
let t = Retyping.get_type_of env sigma c in
- mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t)
+ mkletin_goal env sigma with_eq false (id,lastlhyp,ccl,c) (Some t)
end;
if with_evars then Proofview.shelve_unifiable else guard_no_unifiable;
if is_arg_pure_hyp
@@ -4477,7 +4469,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
let tac =
Tacticals.New.tclTHENLIST [
Refine.refine ~typecheck:false begin fun sigma ->
- mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None
+ mkletin_goal env sigma with_eq true (id,lastlhyp,ccl,c) None
end;
(tac inhyps)
]
@@ -4892,183 +4884,6 @@ let transitivity t = transitivity_gen (Some t)
let intros_transitivity n = Tacticals.New.tclTHEN intros (transitivity_gen n)
-(* tactical to save as name a subproof such that the generalisation of
- the current goal, abstracted with respect to the local signature,
- is solved by tac *)
-
-(** d1 is the section variable in the global context, d2 in the goal context *)
-let interpretable_as_section_decl env evd d1 d2 =
- let open Context.Named.Declaration in
- let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env !sigma c1 c2 with
- | None -> false
- | Some cstr ->
- try ignore (Evd.add_universe_constraints !sigma cstr); true
- with UniversesDiffer -> false
- in
- match d2, d1 with
- | LocalDef _, LocalAssum _ -> false
- | LocalDef (_,b1,t1), LocalDef (_,b2,t2) ->
- e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2
- | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2)
-
-let rec decompose len c t accu =
- let open Context.Rel.Declaration in
- if len = 0 then (c, t, accu)
- else match Constr.kind c, Constr.kind t with
- | Lambda (na, u, c), Prod (_, _, t) ->
- decompose (pred len) c t (LocalAssum (na, u) :: accu)
- | LetIn (na, b, u, c), LetIn (_, _, _, t) ->
- decompose (pred len) c t (LocalDef (na, b, u) :: accu)
- | _ -> assert false
-
-let rec shrink ctx sign c t accu =
- let open Constr in
- let open CVars in
- match ctx, sign with
- | [], [] -> (c, t, accu)
- | p :: ctx, decl :: sign ->
- if noccurn 1 c && noccurn 1 t then
- let c = subst1 mkProp c in
- let t = subst1 mkProp t in
- shrink ctx sign c t accu
- else
- let c = Term.mkLambda_or_LetIn p c in
- let t = Term.mkProd_or_LetIn p t in
- let accu = if RelDecl.is_local_assum p
- then mkVar (NamedDecl.get_id decl) :: accu
- else accu
- in
- shrink ctx sign c t accu
-| _ -> assert false
-
-let shrink_entry sign const =
- let open Entries in
- let typ = match const.const_entry_type with
- | None -> assert false
- | Some t -> t
- in
- (** The body has been forced by the call to [build_constant_by_tactic] *)
- let () = assert (Future.is_over const.const_entry_body) in
- let ((body, uctx), eff) = Future.force const.const_entry_body in
- let (body, typ, ctx) = decompose (List.length sign) body typ [] in
- let (body, typ, args) = shrink ctx sign body typ [] in
- let const = { const with
- const_entry_body = Future.from_val ((body, uctx), eff);
- const_entry_type = Some typ;
- } in
- (const, args)
-
-let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
- let open Tacticals.New in
- let open Tacmach.New in
- let open Proofview.Notations in
- Proofview.Goal.enter begin fun gl ->
- let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
- let current_sign = Global.named_context_val ()
- and global_sign = Proofview.Goal.hyps gl in
- let evdref = ref sigma in
- let sign,secsign =
- List.fold_right
- (fun d (s1,s2) ->
- let id = NamedDecl.get_id d in
- if mem_named_context_val id current_sign &&
- interpretable_as_section_decl env evdref (lookup_named_val id current_sign) d
- then (s1,push_named_context_val d s2)
- else (Context.Named.add d s1,s2))
- global_sign (Context.Named.empty, empty_named_context_val) in
- let id = next_global_ident_away id (pf_ids_set_of_hyps gl) in
- let concl = match goal_type with
- | None -> Proofview.Goal.concl gl
- | Some ty -> ty in
- let concl = it_mkNamedProd_or_LetIn concl sign in
- let concl =
- try flush_and_check_evars !evdref concl
- with Uninstantiated_evar _ ->
- error "\"abstract\" cannot handle existentials." in
-
- let evd, ctx, concl =
- (* FIXME: should be done only if the tactic succeeds *)
- let evd = Evd.minimize_universes !evdref in
- let ctx = Evd.universe_context_set evd in
- evd, ctx, Evarutil.nf_evars_universes evd concl
- in
- let concl = EConstr.of_constr concl in
- let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in
- let ectx = Evd.evar_universe_context evd in
- let (const, safe, ectx) =
- try Pfedit.build_constant_by_tactic ~goal_kind:gk id ectx 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)
- in
- let const, args = shrink_entry sign const in
- let args = List.map EConstr.of_constr args in
- let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in
- let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in
- let cst () =
- (** do not compute the implicit arguments, it may be costly *)
- let () = Impargs.make_implicit_args false in
- (** ppedrot: seems legit to have abstracted subproofs as local*)
- Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl
- in
- let cst = Impargs.with_implicit_protection cst () in
- let lem =
- match const.Entries.const_entry_universes with
- | Entries.Polymorphic_const_entry uctx ->
- let uctx = Univ.ContextSet.of_context uctx in
- (** Hack: the kernel may generate definitions whose universe variables are
- not the same as requested in the entry because of constraints delayed
- in the body, even in polymorphic mode. We mimick what it does for now
- in hope it is fixed at some point. *)
- let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in
- let uctx = Univ.ContextSet.to_context (Univ.ContextSet.union uctx body_uctx) in
- let u = Univ.UContext.instance uctx in
- mkConstU (cst, EInstance.make u)
- | Entries.Monomorphic_const_entry _ ->
- mkConst cst
- in
- let evd = Evd.set_universe_context evd ectx in
- let open Safe_typing in
- let eff = private_con_of_con (Global.safe_env ()) cst in
- let effs = concat_private eff
- Entries.(snd (Future.force const.const_entry_body)) in
- let solve =
- Proofview.tclEFFECTS effs <*>
- tacK lem args
- in
- let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in
- Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac
- end
-
-let abstract_subproof ~opaque id gk tac =
- cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args)))
-
-let anon_id = Id.of_string "anonymous"
-
-let name_op_to_name name_op object_kind suffix =
- let open Proof_global in
- let default_gk = (Global, false, object_kind) in
- let name, gk = match Proof_global.V82.get_current_initial_conclusions () with
- | (id, (_, gk)) -> Some id, gk
- | exception NoCurrentProof -> None, default_gk
- in
- match name_op with
- | Some s -> s, gk
- | None ->
- let name = Option.default anon_id name in
- add_suffix name suffix, gk
-
-let tclABSTRACT ?(opaque=true) name_op tac =
- let s, gk = if opaque
- then name_op_to_name name_op (Proof Theorem) "_subproof"
- else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
- abstract_subproof ~opaque s gk tac
-
let constr_eq ~strict x y =
let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in
let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c088e404b0..7efadb2c28 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -145,7 +145,7 @@ val exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic
type tactic_reduction = Reductionops.reduction_function
type e_tactic_reduction = Reductionops.e_reduction_function
-type change_arg = patvar_map -> evar_map -> evar_map * constr
+type change_arg = patvar_map -> env -> evar_map -> evar_map * constr
val make_change_arg : constr -> change_arg
val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
@@ -418,10 +418,6 @@ val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic
val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
-val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
-
-val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
-
val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic
val specialize_eqs : Id.t -> unit Proofview.tactic
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index f54ad86a3f..5afec74fae 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -7,6 +7,7 @@ Ind_tables
Eqschemes
Elimschemes
Tactics
+Abstract
Elim
Equality
Contradiction
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 05:39:07 +0000