aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/abstract.ml60
-rw-r--r--tactics/abstract.mli12
-rw-r--r--tactics/class_tactics.ml99
-rw-r--r--tactics/class_tactics.mli2
-rw-r--r--tactics/declare.ml512
-rw-r--r--tactics/declare.mli154
-rw-r--r--tactics/declareUctx.ml34
-rw-r--r--tactics/declareUctx.mli (renamed from tactics/leminv.mli)12
-rw-r--r--tactics/eauto.ml48
-rw-r--r--tactics/elimschemes.ml8
-rw-r--r--tactics/eqschemes.ml35
-rw-r--r--tactics/eqschemes.mli4
-rw-r--r--tactics/equality.ml24
-rw-r--r--tactics/hints.ml181
-rw-r--r--tactics/hints.mli20
-rw-r--r--tactics/ind_tables.ml113
-rw-r--r--tactics/ind_tables.mli32
-rw-r--r--tactics/leminv.ml297
-rw-r--r--tactics/pfedit.ml193
-rw-r--r--tactics/pfedit.mli94
-rw-r--r--tactics/proof_global.ml285
-rw-r--r--tactics/proof_global.mli99
-rw-r--r--tactics/redexpr.ml17
-rw-r--r--tactics/tacticals.ml3
-rw-r--r--tactics/tacticals.mli1
-rw-r--r--tactics/tactics.ml12
-rw-r--r--tactics/tactics.mllib5
27 files changed, 294 insertions, 2062 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index e85d94cd72..6b575d0807 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -11,7 +11,6 @@
open Util
open Termops
open EConstr
-open Evarutil
module NamedDecl = Context.Named.Declaration
@@ -41,6 +40,9 @@ let name_op_to_name ~name_op ~name suffix =
| Some s -> s
| None -> Nameops.add_suffix name suffix
+let declare_abstract = ref (fun ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl ->
+ CErrors.anomaly (Pp.str "Abstract declaration hook not registered"))
+
let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
let open Tacticals.New in
let open Tacmach.New in
@@ -76,61 +78,9 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
| 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 sigma concl
- with Uninstantiated_evar _ ->
- CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.") in
-
- let sigma, ctx, concl =
- (* FIXME: should be done only if the tactic succeeds *)
- let sigma = Evd.minimize_universes sigma in
- let ctx = Evd.universe_context_set sigma in
- sigma, ctx, Evarutil.nf_evars_universes sigma 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 sigma in
- let (const, safe, ectx) =
- 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) = 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 *)
- let const = Declare.Internal.map_entry_body const ~f:(fun _ -> body, ()) in
- (* EJGA: Hack related to the above call to
- `build_constant_by_tactic` with `~opaque:Transparent`. Even if
- the abstracted term is destined to be opaque, if we trigger the
- `if poly && opaque && private_poly_univs ()` in `Proof_global`
- kernel will boom. This deserves more investigation. *)
- let const = Declare.Internal.set_opacity ~opaque const in
- let const, args = Declare.Internal.shrink_entry sign const in
- let args = List.map EConstr.of_constr args 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_private_constant ~local:Declare.ImportNeedQualified ~name ~kind const
- in
- let cst, eff = Impargs.with_implicit_protection cst () in
- let inst = match const.Declare.proof_entry_universes with
- | Entries.Monomorphic_entry _ -> EInstance.empty
- | Entries.Polymorphic_entry (_, ctx) ->
- (* We mimic 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.Declare.proof_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 sigma = Evd.set_universe_context sigma ectx in
- let effs = Evd.concat_side_effects eff effs in
+ let effs, sigma, lem, args, safe =
+ !declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl in
let solve =
Proofview.tclEFFECTS effs <*>
tacK lem args
diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index 5c936ff9d6..a138a457b3 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -20,3 +20,15 @@ val cache_term_by_tactic_then
-> unit Proofview.tactic
val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
+
+val declare_abstract :
+ ( name:Names.Id.t
+ -> poly:bool
+ -> kind:Decls.logical_kind
+ -> sign:EConstr.named_context
+ -> secsign:Environ.named_context_val
+ -> opaque:bool
+ -> solve_tac:unit Proofview.tactic
+ -> Evd.evar_map
+ -> EConstr.t
+ -> Evd.side_effects * Evd.evar_map * EConstr.t * EConstr.t list * bool) ref
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 92d56d2904..a51fc8b347 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -38,33 +38,48 @@ let typeclasses_db = "typeclass_instances"
(** Options handling *)
let typeclasses_debug = ref 0
-let typeclasses_depth = ref None
+
+let typeclasses_depth_opt_name = ["Typeclasses";"Depth"]
+let get_typeclasses_depth =
+ Goptions.declare_intopt_option_and_ref
+ ~depr:false
+ ~key:typeclasses_depth_opt_name
+
+let set_typeclasses_depth =
+ Goptions.set_int_option_value typeclasses_depth_opt_name
(** When this flag is enabled, the resolution of type classes tries to avoid
useless introductions. This is no longer useful since we have eta, but is
here for compatibility purposes. Another compatibility issues is that the
cost (in terms of search depth) can differ. *)
-let typeclasses_limit_intros = ref true
-let set_typeclasses_limit_intros d = (:=) typeclasses_limit_intros d
-let get_typeclasses_limit_intros () = !typeclasses_limit_intros
-
-let typeclasses_dependency_order = ref false
-let set_typeclasses_dependency_order d = (:=) typeclasses_dependency_order d
-let get_typeclasses_dependency_order () = !typeclasses_dependency_order
-
-let typeclasses_iterative_deepening = ref false
-let set_typeclasses_iterative_deepening d = (:=) typeclasses_iterative_deepening d
-let get_typeclasses_iterative_deepening () = !typeclasses_iterative_deepening
+let get_typeclasses_limit_intros =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Typeclasses";"Limit";"Intros"]
+ ~value:true
+
+let get_typeclasses_dependency_order =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Typeclasses";"Dependency";"Order"]
+ ~value:false
+
+let iterative_deepening_opt_name = ["Typeclasses";"Iterative";"Deepening"]
+let get_typeclasses_iterative_deepening =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:iterative_deepening_opt_name
+ ~value:false
(** [typeclasses_filtered_unif] governs the unification algorithm used by type
classes. If enabled, a new algorithm based on pattern filtering and refine
will be used. When disabled, the previous algorithm based on apply will be
used. *)
-let typeclasses_filtered_unification = ref false
-let set_typeclasses_filtered_unification d =
- (:=) typeclasses_filtered_unification d
-let get_typeclasses_filtered_unification () =
- !typeclasses_filtered_unification
+let get_typeclasses_filtered_unification =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Typeclasses";"Filtered";"Unification"]
+ ~value:false
let set_typeclasses_debug d = (:=) typeclasses_debug (if d then 1 else 0)
let get_typeclasses_debug () = if !typeclasses_debug > 0 then true else false
@@ -75,40 +90,8 @@ let set_typeclasses_verbose =
let get_typeclasses_verbose () =
if !typeclasses_debug = 0 then None else Some !typeclasses_debug
-let set_typeclasses_depth d = (:=) typeclasses_depth d
-let get_typeclasses_depth () = !typeclasses_depth
-
-open Goptions
-
-let () =
- declare_bool_option
- { optdepr = false;
- optkey = ["Typeclasses";"Limit";"Intros"];
- optread = get_typeclasses_limit_intros;
- optwrite = set_typeclasses_limit_intros; }
-
-let () =
- declare_bool_option
- { optdepr = false;
- optkey = ["Typeclasses";"Dependency";"Order"];
- optread = get_typeclasses_dependency_order;
- optwrite = set_typeclasses_dependency_order; }
-
-let () =
- declare_bool_option
- { optdepr = false;
- optkey = ["Typeclasses";"Iterative";"Deepening"];
- optread = get_typeclasses_iterative_deepening;
- optwrite = set_typeclasses_iterative_deepening; }
-
-let () =
- declare_bool_option
- { optdepr = false;
- optkey = ["Typeclasses";"Filtered";"Unification"];
- optread = get_typeclasses_filtered_unification;
- optwrite = set_typeclasses_filtered_unification; }
-
let () =
+ let open Goptions in
declare_bool_option
{ optdepr = false;
optkey = ["Typeclasses";"Debug"];
@@ -116,24 +99,18 @@ let () =
optwrite = set_typeclasses_debug; }
let _ =
+ let open Goptions in
declare_int_option
{ optdepr = false;
optkey = ["Typeclasses";"Debug";"Verbosity"];
optread = get_typeclasses_verbose;
optwrite = set_typeclasses_verbose; }
-let () =
- declare_int_option
- { optdepr = false;
- optkey = ["Typeclasses";"Depth"];
- optread = get_typeclasses_depth;
- optwrite = set_typeclasses_depth; }
-
type search_strategy = Dfs | Bfs
let set_typeclasses_strategy = function
- | Dfs -> set_typeclasses_iterative_deepening false
- | Bfs -> set_typeclasses_iterative_deepening true
+ | Dfs -> Goptions.set_bool_option_value iterative_deepening_opt_name false
+ | Bfs -> Goptions.set_bool_option_value iterative_deepening_opt_name true
let pr_ev evs ev =
Printer.pr_econstr_env (Goal.V82.env evs ev) evs (Goal.V82.concl evs ev)
@@ -977,7 +954,7 @@ module Search = struct
| None -> None (* This happens only because there's no evar having p *)
| Some (goals, nongoals) ->
let goalsl =
- if !typeclasses_dependency_order then
+ if get_typeclasses_dependency_order () then
top_sort evm goals
else Evar.Set.elements goals
in
@@ -1211,7 +1188,7 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
with Refiner.FailError _ -> raise Not_found
in
let evd = sig_sig gls' in
- let t' = mkEvar (ev, Array.of_list subst) in
+ let t' = mkEvar (ev, subst) in
let term = Evarutil.nf_evar evd t' in
term, evd
end in
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index e26338436d..b97b90d777 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -19,10 +19,8 @@ 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
val set_typeclasses_depth : int option -> unit
-val get_typeclasses_depth : unit -> int option
type search_strategy = Dfs | Bfs
diff --git a/tactics/declare.ml b/tactics/declare.ml
deleted file mode 100644
index 5e6f78be6f..0000000000
--- a/tactics/declare.ml
+++ /dev/null
@@ -1,512 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* 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 is about the low-level declaration of logical objects *)
-
-open Pp
-open Util
-open Names
-open Declarations
-open Entries
-open Safe_typing
-open Libobject
-open Lib
-
-(* object_kind , id *)
-exception AlreadyDeclared of (string option * Id.t)
-
-let _ = CErrors.register_handler (function
- | AlreadyDeclared (kind, id) ->
- Some
- (seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind
- ; Id.print id; str " already exists."])
- | _ ->
- None)
-
-module NamedDecl = Context.Named.Declaration
-
-type import_status = ImportDefaultBehavior | ImportNeedQualified
-
-(** Monomorphic universes need to survive sections. *)
-
-let name_instance inst =
- let map lvl = match Univ.Level.name lvl with
- | None -> (* Having Prop/Set/Var as section universes makes no sense *)
- assert false
- | Some na ->
- try
- let qid = Nametab.shortest_qualid_of_universe na in
- Name (Libnames.qualid_basename qid)
- with Not_found ->
- (* Best-effort naming from the string representation of the level.
- See univNames.ml for a similar hack. *)
- Name (Id.of_string_soft (Univ.Level.to_string lvl))
- in
- Array.map map (Univ.Instance.to_array inst)
-
-let declare_universe_context ~poly ctx =
- if poly then
- let uctx = Univ.ContextSet.to_context ctx in
- let nas = name_instance (Univ.UContext.instance uctx) in
- Global.push_section_context (nas, uctx)
- else
- Global.push_context_set ~strict:true ctx
-
-(** Declaration of constants and parameters *)
-
-type constant_obj = {
- cst_kind : Decls.logical_kind;
- cst_locl : import_status;
-}
-
-type 'a proof_entry = {
- proof_entry_body : 'a Entries.const_entry_body;
- (* List of section variables *)
- proof_entry_secctx : Id.Set.t option;
- (* State id on which the completion of type checking is reported *)
- proof_entry_feedback : Stateid.t option;
- proof_entry_type : Constr.types option;
- proof_entry_universes : Entries.universes_entry;
- proof_entry_opaque : bool;
- proof_entry_inline_code : bool;
-}
-
-type 'a constant_entry =
- | DefinitionEntry of 'a proof_entry
- | ParameterEntry of parameter_entry
- | PrimitiveEntry of primitive_entry
-
-(* At load-time, the segment starting from the module name to the discharge *)
-(* section (if Remark or Fact) is needed to access a construction *)
-let load_constant i ((sp,kn), obj) =
- if Nametab.exists_cci sp then
- raise (AlreadyDeclared (None, Libnames.basename sp));
- let con = Global.constant_of_delta_kn kn in
- Nametab.push (Nametab.Until i) sp (GlobRef.ConstRef con);
- Dumpglob.add_constant_kind con obj.cst_kind
-
-(* Opening means making the name without its module qualification available *)
-let open_constant i ((sp,kn), obj) =
- (* Never open a local definition *)
- match obj.cst_locl with
- | ImportNeedQualified -> ()
- | ImportDefaultBehavior ->
- let con = Global.constant_of_delta_kn kn in
- Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con)
-
-let exists_name id =
- Decls.variable_exists id || Global.exists_objlabel (Label.of_id id)
-
-let check_exists id =
- if exists_name id then
- raise (AlreadyDeclared (None, id))
-
-let cache_constant ((sp,kn), obj) =
- (* Invariant: the constant must exist in the logical environment, except when
- redefining it when exiting a section. See [discharge_constant]. *)
- let kn' =
- if Global.exists_objlabel (Label.of_id (Libnames.basename sp))
- then Constant.make1 kn
- else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(Libnames.basename sp) ++ str".")
- in
- assert (Constant.equal kn' (Constant.make1 kn));
- Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn));
- Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind
-
-let discharge_constant ((sp, kn), obj) =
- Some obj
-
-(* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant cst = {
- cst_kind = cst.cst_kind;
- cst_locl = cst.cst_locl;
-}
-
-let classify_constant cst = Substitute (dummy_constant cst)
-
-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;
- classify_function = classify_constant;
- 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)
-
-let register_constant kn kind local =
- let o = inConstant {
- cst_kind = kind;
- cst_locl = local;
- } in
- let id = Label.to_id (Constant.label kn) in
- let _ = add_leaf id o in
- update_tables kn
-
-let register_side_effect (c, role) =
- let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in
- match role with
- | 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
- let v =
- String.concat " "
- (CList.map_filter (fun decl ->
- let id = NamedDecl.get_id decl in
- if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None
- else Some (Id.to_string id))
- (keep_hyps env s_bo)) in
- Aux_file.record_in_aux "context_used" v
-
-let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
-
-let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
- ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body =
- { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
- proof_entry_secctx = None;
- proof_entry_type = types;
- proof_entry_universes = univs;
- proof_entry_opaque = opaque;
- proof_entry_feedback = None;
- proof_entry_inline_code = inline}
-
-let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
- ?(univs=default_univ_entry) body =
- { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), ());
- proof_entry_secctx = None;
- proof_entry_type = types;
- proof_entry_universes = univs;
- proof_entry_opaque = opaque;
- proof_entry_feedback = None;
- proof_entry_inline_code = inline}
-
-let delayed_definition_entry ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?(univs=default_univ_entry) ?types body =
- { proof_entry_body = body
- ; proof_entry_secctx = section_vars
- ; proof_entry_type = types
- ; proof_entry_universes = univs
- ; proof_entry_opaque = opaque
- ; proof_entry_feedback = feedback_id
- ; proof_entry_inline_code = inline
- }
-
-let cast_proof_entry e =
- let (body, ctx), () = Future.force e.proof_entry_body in
- let univs =
- if Univ.ContextSet.is_empty ctx then e.proof_entry_universes
- else match e.proof_entry_universes with
- | Monomorphic_entry ctx' ->
- (* This can actually happen, try compiling EqdepFacts for instance *)
- Monomorphic_entry (Univ.ContextSet.union ctx' ctx)
- | Polymorphic_entry _ ->
- CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.");
- in
- {
- const_entry_body = body;
- const_entry_secctx = e.proof_entry_secctx;
- const_entry_feedback = e.proof_entry_feedback;
- const_entry_type = e.proof_entry_type;
- const_entry_universes = univs;
- const_entry_inline_code = e.proof_entry_inline_code;
- }
-
-type ('a, 'b) effect_entry =
-| EffectEntry : (private_constants, private_constants Entries.const_entry_body) effect_entry
-| PureEntry : (unit, Constr.constr) effect_entry
-
-let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proof_entry) : b opaque_entry =
- let typ = match e.proof_entry_type with
- | None -> assert false
- | Some typ -> typ
- in
- let secctx = match e.proof_entry_secctx with
- | None ->
- let open Environ in
- let env = Global.env () in
- let hyp_typ, hyp_def =
- if List.is_empty (Environ.named_context env) then
- Id.Set.empty, Id.Set.empty
- else
- let ids_typ = global_vars_set env typ in
- let pf, env = match entry with
- | PureEntry ->
- let (pf, _), () = Future.force e.proof_entry_body in
- pf, env
- | EffectEntry ->
- let (pf, _), eff = Future.force e.proof_entry_body in
- let env = Safe_typing.push_private_constants env eff in
- pf, env
- in
- let vars = global_vars_set env pf in
- ids_typ, vars
- in
- let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in
- Environ.really_needed env (Id.Set.union hyp_typ hyp_def)
- | Some hyps -> hyps
- in
- let (body, univs : b * _) = match entry with
- | PureEntry ->
- let (body, uctx), () = Future.force e.proof_entry_body in
- let univs = match e.proof_entry_universes with
- | Monomorphic_entry uctx' -> Monomorphic_entry (Univ.ContextSet.union uctx uctx')
- | Polymorphic_entry _ ->
- assert (Univ.ContextSet.is_empty uctx);
- e.proof_entry_universes
- in
- body, univs
- | EffectEntry -> e.proof_entry_body, e.proof_entry_universes
- in
- {
- opaque_entry_body = body;
- opaque_entry_secctx = secctx;
- opaque_entry_feedback = e.proof_entry_feedback;
- opaque_entry_type = typ;
- opaque_entry_universes = univs;
- }
-
-let feedback_axiom () = Feedback.(feedback AddedAxiom)
-
-let is_unsafe_typing_flags () =
- let flags = Environ.typing_flags (Global.env()) in
- not (flags.check_universes && flags.check_guarded && flags.check_positive)
-
-let define_constant ~name cd =
- (* Logically define the constant and its subproofs, no libobject tampering *)
- 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
-
-let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
- let () = check_exists name in
- let kn = define_constant ~name cd in
- (* Register the libobjects attached to the constants *)
- let () = register_constant kn kind local in
- kn
-
-let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de =
- let kn, eff =
- let de =
- if not de.proof_entry_opaque then
- DefinitionEff (cast_proof_entry de)
- else
- let de = cast_opaque_proof_entry PureEntry de in
- OpaqueEff de
- in
- Global.add_private_constant name de
- in
- let () = register_constant kn kind local in
- let seff_roles = match role with
- | None -> Cmap.empty
- | Some r -> Cmap.singleton kn r
- in
- let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
- kn, eff
-
-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 uctx = UState.merge ~sideff:true Evd.univ_rigid uctx ctx in
- cb, uctx
-
-(** Declaration of section variables and local definitions *)
-type variable_declaration =
- | SectionLocalDef of Evd.side_effects proof_entry
- | SectionLocalAssum of { typ:Constr.types; impl:Glob_term.binding_kind; }
-
-(* This object is only for things which iterate over objects to find
- variables (only Prettyp.print_context AFAICT) *)
-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 =
- (* Variables are distinguished by only short names *)
- if Decls.variable_exists name then
- raise (AlreadyDeclared (None, name));
-
- let impl,opaque = match d with (* Fails if not well-typed *)
- | SectionLocalAssum {typ;impl} ->
- let () = Global.push_named_assum (name,typ) in
- impl, true
- | 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, 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 body_ui entry_ui in
- (* We must declare the universe constraints before type-checking the
- term. *)
- let () = declare_universe_context ~poly univs in
- let se = {
- secdef_body = body;
- secdef_secctx = de.proof_entry_secctx;
- secdef_feedback = de.proof_entry_feedback;
- secdef_type = de.proof_entry_type;
- } in
- let () = Global.push_named_def (name, se) in
- Glob_term.Explicit, de.proof_entry_opaque
- in
- Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
- Decls.(add_variable_data name {opaque;kind});
- ignore(add_leaf name (inVariable ()) : Libobject.object_name);
- Impargs.declare_var_implicits ~impl name;
- Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
-
-(* Declaration messages *)
-
-let pr_rank i = pr_nth (i+1)
-
-let fixpoint_message indexes l =
- Flags.if_verbose Feedback.msg_info (match l with
- | [] -> CErrors.anomaly (Pp.str "no recursive definition.")
- | [id] -> Id.print id ++ str " is recursively defined" ++
- (match indexes with
- | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
- | _ -> mt ())
- | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
- spc () ++ str "are recursively defined" ++
- match indexes with
- | Some a -> spc () ++ str "(decreasing respectively on " ++
- prvect_with_sep pr_comma pr_rank a ++
- str " arguments)"
- | None -> mt ()))
-
-let cofixpoint_message l =
- Flags.if_verbose Feedback.msg_info (match l with
- | [] -> CErrors.anomaly (Pp.str "No corecursive definition.")
- | [id] -> Id.print id ++ str " is corecursively defined"
- | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
- spc () ++ str "are corecursively defined"))
-
-let recursive_message isfix i l =
- (if isfix then fixpoint_message i else cofixpoint_message) l
-
-let definition_message id =
- Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
-
-let assumption_message id =
- (* Changing "assumed" to "declared", "assuming" referring more to
- the type of the object than to the name of the object (see
- discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
- Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
-
-module Internal = struct
-
- let map_entry_body ~f entry =
- { entry with proof_entry_body = Future.chain entry.proof_entry_body f }
-
- let map_entry_type ~f entry =
- { entry with proof_entry_type = f entry.proof_entry_type }
-
- let set_opacity ~opaque entry =
- { entry with proof_entry_opaque = opaque }
-
- let get_fix_exn entry = Future.fix_exn_of entry.proof_entry_body
-
- 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 Vars 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 Context.Rel.Declaration.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 typ = match const.proof_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.proof_entry_body) in
- let ((body, uctx), eff) = Future.force const.proof_entry_body in
- let (body, typ, ctx) = decompose (List.length sign) body typ [] in
- let (body, typ, args) = shrink ctx sign body typ [] in
- { const with
- proof_entry_body = Future.from_val ((body, uctx), eff)
- ; 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
deleted file mode 100644
index 0068b9842a..0000000000
--- a/tactics/declare.mli
+++ /dev/null
@@ -1,154 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* 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) *)
-(************************************************************************)
-
-open Names
-open Constr
-open Entries
-
-(** This module provides the official functions to declare new variables,
- parameters, constants and inductive types. Using the following functions
- will add the entries in the global environment (module [Global]), will
- register the declarations in the library (module [Lib]) --- so that the
- reset works properly --- and will fill some global tables such as
- [Nametab] and [Impargs]. *)
-
-(** Proof entries *)
-type 'a proof_entry = private {
- proof_entry_body : 'a Entries.const_entry_body;
- (* List of section variables *)
- proof_entry_secctx : Id.Set.t option;
- (* State id on which the completion of type checking is reported *)
- proof_entry_feedback : Stateid.t option;
- proof_entry_type : Constr.types option;
- proof_entry_universes : Entries.universes_entry;
- proof_entry_opaque : bool;
- proof_entry_inline_code : bool;
-}
-
-(** Declaration of local constructions (Variable/Hypothesis/Local) *)
-
-type variable_declaration =
- | SectionLocalDef of Evd.side_effects proof_entry
- | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; }
-
-type 'a constant_entry =
- | DefinitionEntry of 'a proof_entry
- | ParameterEntry of parameter_entry
- | PrimitiveEntry of primitive_entry
-
-val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
-
-val declare_variable
- : name:variable
- -> kind:Decls.logical_kind
- -> variable_declaration
- -> unit
-
-(** Declaration of global constructions
- i.e. Definition/Theorem/Axiom/Parameter/... *)
-
-(* Default definition entries, transparent with no secctx or proj information *)
-val definition_entry
- : ?fix_exn:Future.fix_exn
- -> ?opaque:bool
- -> ?inline:bool
- -> ?types:types
- -> ?univs:Entries.universes_entry
- -> ?eff:Evd.side_effects
- -> constr
- -> Evd.side_effects proof_entry
-
-val pure_definition_entry
- : ?fix_exn:Future.fix_exn
- -> ?opaque:bool
- -> ?inline:bool
- -> ?types:types
- -> ?univs:Entries.universes_entry
- -> constr
- -> unit proof_entry
-
-(* Delayed definition entries *)
-val delayed_definition_entry
- : ?opaque:bool
- -> ?inline:bool
- -> ?feedback_id:Stateid.t
- -> ?section_vars:Id.Set.t
- -> ?univs:Entries.universes_entry
- -> ?types:types
- -> 'a Entries.const_entry_body
- -> 'a proof_entry
-
-type import_status = ImportDefaultBehavior | ImportNeedQualified
-
-(** [declare_constant id cd] declares a global declaration
- (constant/parameter) with name [id] in the current section; it returns
- the full path of the declaration
-
- internal specify if the constant has been created by the kernel or by the
- user, and in the former case, if its errors should be silent *)
-val declare_constant
- : ?local:import_status
- -> name:Id.t
- -> kind:Decls.logical_kind
- -> Evd.side_effects constant_entry
- -> Constant.t
-
-val declare_private_constant
- : ?role:Evd.side_effect_role
- -> ?local:import_status
- -> name:Id.t
- -> kind:Decls.logical_kind
- -> unit proof_entry
- -> Constant.t * Evd.side_effects
-
-(** [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
- : uctx:UState.t
- -> Environ.env
- -> Evd.side_effects proof_entry
- -> Constr.t * UState.t
-
-(** Declaration messages *)
-
-val definition_message : Id.t -> unit
-val assumption_message : Id.t -> unit
-val fixpoint_message : int array option -> Id.t list -> unit
-val cofixpoint_message : Id.t list -> unit
-val recursive_message : bool (** true = fixpoint *) ->
- int array option -> Id.t list -> unit
-
-val check_exists : Id.t -> unit
-
-(* Used outside this module only in indschemes *)
-exception AlreadyDeclared of (string option * Id.t)
-
-(** {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
- val map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entry
- (* Overriding opacity is indeed really hacky *)
- val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry
-
- (* TODO: This is only used in DeclareDef to forward the fix to
- hooks, should eventually go away *)
- val get_fix_exn : 'a proof_entry -> Future.fix_exn
-
- 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/declareUctx.ml b/tactics/declareUctx.ml
new file mode 100644
index 0000000000..3f67ff20a4
--- /dev/null
+++ b/tactics/declareUctx.ml
@@ -0,0 +1,34 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* 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) *)
+(************************************************************************)
+
+(** Monomorphic universes need to survive sections. *)
+
+let name_instance inst =
+ let map lvl = match Univ.Level.name lvl with
+ | None -> (* Having Prop/Set/Var as section universes makes no sense *)
+ assert false
+ | Some na ->
+ try
+ let qid = Nametab.shortest_qualid_of_universe na in
+ Names.Name (Libnames.qualid_basename qid)
+ with Not_found ->
+ (* Best-effort naming from the string representation of the level.
+ See univNames.ml for a similar hack. *)
+ Names.Name (Names.Id.of_string_soft (Univ.Level.to_string lvl))
+ in
+ Array.map map (Univ.Instance.to_array inst)
+
+let declare_universe_context ~poly ctx =
+ if poly then
+ let uctx = Univ.ContextSet.to_context ctx in
+ let nas = name_instance (Univ.UContext.instance uctx) in
+ Global.push_section_context (nas, uctx)
+ else
+ Global.push_context_set ~strict:true ctx
diff --git a/tactics/leminv.mli b/tactics/declareUctx.mli
index 5a5de7b58f..7ecfab04f2 100644
--- a/tactics/leminv.mli
+++ b/tactics/declareUctx.mli
@@ -8,14 +8,4 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Names
-open EConstr
-open Constrexpr
-open Tactypes
-
-val lemInv_clause :
- quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
-
-val add_inversion_lemma_exn : poly:bool ->
- Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) ->
- unit
+val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index a89e5ef19a..28b5ed5811 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -430,29 +430,39 @@ let make_dimension n = function
| None -> (true,make_depth n)
| Some d -> (false,d)
+let autounfolds ids csts gl cls =
+ let hyps = Tacmach.New.pf_ids_of_hyps gl in
+ let env = Tacmach.New.pf_env gl in
+ let ids = List.filter (fun id -> List.mem id hyps && Tacred.is_evaluable env (EvalVarRef id)) ids in
+ let csts = List.filter (fun cst -> Tacred.is_evaluable env (EvalConstRef cst)) csts in
+ let flags =
+ List.fold_left (fun flags cst -> CClosure.RedFlags.(red_add flags (fCONST cst)))
+ (List.fold_left (fun flags id -> CClosure.RedFlags.(red_add flags (fVAR id)))
+ CClosure.betaiotazeta ids) csts
+ in reduct_option ~check:false (Reductionops.clos_norm_flags flags, DEFAULTcast) cls
+
let cons a l = a :: l
-let autounfolds db occs cls gl =
- let unfolds = List.concat (List.map (fun dbname ->
- let db = try searchtable_map dbname
- with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname)
- in
- let (ids, csts) = Hint_db.unfolds db in
- let hyps = pf_ids_of_hyps gl in
- let ids = Id.Set.filter (fun id -> List.mem id hyps) ids in
- Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts
- (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db)
- in Proofview.V82.of_tactic (unfold_option unfolds cls) gl
+exception UnknownDatabase of string
let autounfold db cls =
- Proofview.V82.tactic begin fun gl ->
- let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in
- let tac = autounfolds db in
- tclMAP (function
- | OnHyp (id,occs,where) -> tac occs (Some (id,where))
- | OnConcl occs -> tac occs None)
- cls gl
- end
+ if not (Locusops.clause_with_generic_occurrences cls) then
+ user_err ~hdr:"autounfold" (str "\"at\" clause not supported");
+ match List.fold_left (fun (ids, csts) dbname ->
+ let db = try searchtable_map dbname
+ with Not_found -> raise (UnknownDatabase dbname)
+ in
+ let (db_ids, db_csts) = Hint_db.unfolds db in
+ (Id.Set.fold cons db_ids ids, Cset.fold cons db_csts csts)) ([], []) db
+ with
+ | (ids, csts) -> Proofview.Goal.enter begin fun gl ->
+ let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in
+ let tac = autounfolds ids csts gl in
+ Tacticals.New.tclMAP (function
+ | OnHyp (id, _, where) -> tac (Some (id, where))
+ | OnConcl _ -> tac None) cls
+ end
+ | exception UnknownDatabase dbname -> Tacticals.New.tclZEROMSG (str "Unknown database " ++ str dbname)
let autounfold_tac db cls =
Proofview.tclUNIT () >>= fun () ->
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 910e042e7a..9a517652a7 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -27,11 +27,11 @@ open Ind_tables
let optimize_non_type_induction_scheme kind dep sort ind =
let env = Global.env () in
let sigma = Evd.from_env env in
- if check_scheme kind ind then
+ match lookup_scheme kind ind with
+ | Some cte ->
(* in case the inductive has a type elimination, generates only one
induction scheme, the other ones share the same code with the
appropriate type *)
- let cte = lookup_scheme kind ind in
let sigma, cte = Evd.fresh_constant_instance env sigma cte in
let c = mkConstU cte in
let t = type_of_constant_in (Global.env()) cte in
@@ -48,7 +48,7 @@ let optimize_non_type_induction_scheme kind dep sort ind =
let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in
let sigma = Evd.minimize_universes sigma in
(Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma)
- else
+ | None ->
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)
@@ -62,7 +62,7 @@ let build_induction_scheme_in_type dep sort ind =
let declare_individual_scheme_object name ?aux f =
let f : individual_scheme_object_function =
- fun _ ind -> f ind, Evd.empty_side_effects
+ fun _ ind -> f ind
in
declare_individual_scheme_object name ?aux f
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 98da61781e..7c702eab3a 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -229,7 +229,7 @@ let sym_scheme_kind =
declare_individual_scheme_object "_sym_internal"
(fun _ ind ->
let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in
- (c, ctx), Evd.empty_side_effects)
+ (c, ctx))
(**********************************************************************)
(* Build the involutivity of symmetry for an inductive type *)
@@ -248,17 +248,17 @@ let sym_scheme_kind =
(**********************************************************************)
let const_of_scheme kind env ind ctx =
- let sym_scheme, eff = (find_scheme kind ind) in
+ let sym_scheme = match lookup_scheme kind ind with Some cst -> cst | None -> assert false in
let sym, ctx = with_context_set ctx
(UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in
- mkConstU sym, ctx, eff
+ mkConstU sym, ctx
let build_sym_involutive_scheme env ind =
let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
get_sym_eq_data env indu in
let eq,eqrefl,ctx = get_coq_eq ctx in
- let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
+ let sym, ctx = const_of_scheme sym_scheme_kind env ind ctx in
let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect mkRel n paramsctxt) in
let inds = snd (mind_arity mip) in
let indr = Sorts.relevance_of_sort_family inds in
@@ -297,10 +297,11 @@ let build_sym_involutive_scheme env ind =
mkRel 1|])),
mkRel 1 (* varH *),
[|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
- in (c, UState.of_context_set ctx), eff
+ in (c, UState.of_context_set ctx)
let sym_involutive_scheme_kind =
declare_individual_scheme_object "_sym_involutive"
+ ~deps:(fun ind -> [SchemeIndividualDep (ind, sym_scheme_kind)])
(fun _ ind ->
build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind)
@@ -368,8 +369,8 @@ let build_l2r_rew_scheme dep env ind kind =
let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
get_sym_eq_data env indu in
- let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
- let sym_involutive, ctx, eff' = const_of_scheme sym_involutive_scheme_kind env ind ctx in
+ let sym, ctx = const_of_scheme sym_scheme_kind env ind ctx in
+ let sym_involutive, ctx = const_of_scheme sym_involutive_scheme_kind env ind ctx in
let eq,eqrefl,ctx = get_coq_eq ctx in
let cstr n p =
mkApp (mkConstructUi(indu,1),
@@ -454,8 +455,7 @@ let build_l2r_rew_scheme dep env ind kind =
[|main_body|])
else
main_body))))))
- in (c, UState.of_context_set ctx),
- Evd.concat_side_effects eff' eff
+ in (c, UState.of_context_set ctx)
(**********************************************************************)
(* Build the left-to-right rewriting lemma for hypotheses associated *)
@@ -698,6 +698,10 @@ let build_r2l_rew_scheme dep env ind k =
(**********************************************************************)
let rew_l2r_dep_scheme_kind =
declare_individual_scheme_object "_rew_r_dep"
+ ~deps:(fun ind -> [
+ SchemeIndividualDep (ind, sym_scheme_kind);
+ SchemeIndividualDep (ind, sym_involutive_scheme_kind);
+ ])
(fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType)
(**********************************************************************)
@@ -708,7 +712,7 @@ let rew_l2r_dep_scheme_kind =
(**********************************************************************)
let rew_r2l_dep_scheme_kind =
declare_individual_scheme_object "_rew_dep"
- (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
+ (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType)
(**********************************************************************)
(* Dependent rewrite from right-to-left in hypotheses *)
@@ -718,7 +722,7 @@ let rew_r2l_dep_scheme_kind =
(**********************************************************************)
let rew_r2l_forward_dep_scheme_kind =
declare_individual_scheme_object "_rew_fwd_dep"
- (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
+ (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType)
(**********************************************************************)
(* Dependent rewrite from left-to-right in hypotheses *)
@@ -728,7 +732,7 @@ let rew_r2l_forward_dep_scheme_kind =
(**********************************************************************)
let rew_l2r_forward_dep_scheme_kind =
declare_individual_scheme_object "_rew_fwd_r_dep"
- (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
+ (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType)
(**********************************************************************)
(* Non-dependent rewrite from either left-to-right in conclusion or *)
@@ -742,7 +746,7 @@ let rew_l2r_forward_dep_scheme_kind =
let rew_l2r_scheme_kind =
declare_individual_scheme_object "_rew_r"
(fun _ ind -> fix_r2l_forward_rew_scheme
- (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Evd.empty_side_effects)
+ (build_r2l_forward_rew_scheme false (Global.env()) ind InType))
(**********************************************************************)
(* Non-dependent rewrite from either right-to-left in conclusion or *)
@@ -752,7 +756,7 @@ let rew_l2r_scheme_kind =
(**********************************************************************)
let rew_r2l_scheme_kind =
declare_individual_scheme_object "_rew"
- (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Evd.empty_side_effects)
+ (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType)
(* End of rewriting schemes *)
@@ -835,5 +839,4 @@ let build_congr env (eq,refl,ctx) ind =
let congr_scheme_kind = declare_individual_scheme_object "_congr"
(fun _ ind ->
(* May fail if equality is not defined *)
- build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind,
- Evd.empty_side_effects)
+ build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind)
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index d1038f2655..6447708ace 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -27,7 +27,7 @@ val rew_r2l_scheme_kind : individual scheme_kind
val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family ->
constr Evd.in_evar_universe_context
val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family ->
- constr Evd.in_evar_universe_context * Evd.side_effects
+ constr Evd.in_evar_universe_context
val build_r2l_forward_rew_scheme :
bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context
val build_l2r_forward_rew_scheme :
@@ -39,7 +39,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context
val sym_scheme_kind : individual scheme_kind
val build_sym_involutive_scheme : env -> inductive ->
- constr Evd.in_evar_universe_context * Evd.side_effects
+ constr Evd.in_evar_universe_context
val sym_involutive_scheme_kind : individual scheme_kind
(** Builds a congruence scheme for an equality type *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 49645d82a4..e1d34af13e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -411,8 +411,7 @@ let find_elim hdcncl lft2rgt dep cls ot =
match EConstr.kind sigma hdcncl with
| Ind (ind,u) ->
- let c, eff = find_scheme scheme_name ind in
- Proofview.tclEFFECTS eff <*>
+ find_scheme scheme_name ind >>= fun c ->
pf_constr_of_global (GlobRef.ConstRef c)
| _ -> assert false
end
@@ -1001,14 +1000,13 @@ let ind_scheme_of_eq lbeq to_kind =
let from_kind = inductive_sort_family mip in
(* use ind rather than case by compatibility *)
let kind = Elimschemes.nondep_elim_scheme from_kind to_kind in
- let c, eff = find_scheme kind (destIndRef lbeq.eq) in
- GlobRef.ConstRef c, eff
+ find_scheme kind (destIndRef lbeq.eq) >>= fun c ->
+ Proofview.tclUNIT (GlobRef.ConstRef c)
let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind =
build_coq_I () >>= fun i ->
- let eq_elim, eff = ind_scheme_of_eq lbeq to_kind in
- Proofview.tclEFFECTS eff <*>
+ ind_scheme_of_eq lbeq to_kind >>= fun eq_elim ->
pf_constr_of_global eq_elim >>= fun eq_elim ->
Proofview.tclUNIT
(applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2]))
@@ -1045,7 +1043,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
tclTHENS (assert_after Anonymous false_0)
- [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))]
+ [onLastHypId gen_absurdity; (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))]
let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
@@ -1347,23 +1345,23 @@ let inject_if_homogenous_dependent_pair ty =
(* and compare the fst arguments of the dep pair *)
(* Note: should work even if not an inductive type, but the table only *)
(* knows inductive types *)
- if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind &&
+ if not (Option.has_some (Ind_tables.lookup_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_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
+ find_scheme (!eq_dec_scheme_kind_name()) ind >>= fun c ->
(* 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.(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 ->
- Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr
- (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))))
+ Refiner.refiner ~check:true EConstr.Unsafe.(to_constr
+ (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
])]
with Exit ->
Proofview.tclUNIT ()
@@ -1408,7 +1406,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
(Proofview.tclIGNORE (Proofview.Monad.List.map
(fun (pf,ty) -> tclTHENS (cut ty)
[inject_if_homogenous_dependent_pair ty;
- Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))])
+ Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)])
(if l2r then List.rev injectors else injectors)))
(tac (List.length injectors)))
diff --git a/tactics/hints.ml b/tactics/hints.ml
index a907b9e783..5fb519cc4f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -23,7 +23,6 @@ open Globnames
open Libobject
open Namegen
open Libnames
-open Smartlocate
open Termops
open Inductiveops
open Typeclasses
@@ -100,8 +99,6 @@ let empty_hint_info =
(* The Type of Constructions Autotactic Hints *)
(************************************************************************)
-type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
-
type 'a hint_ast =
| Res_pf of 'a (* Hint Apply *)
| ERes_pf of 'a (* Hint EApply *)
@@ -164,10 +161,6 @@ type full_hint = hint with_metadata
type hint_entry = GlobRef.t option *
raw_hint hint_ast with_uid with_metadata
-type reference_or_constr =
- | HintsReference of qualid
- | HintsConstr of Constrexpr.constr_expr
-
type hint_mode =
| ModeInput (* No evars *)
| ModeNoHeadEvar (* No evar at the head *)
@@ -178,37 +171,26 @@ type 'a hints_transparency_target =
| HintsConstants
| HintsReferences of 'a list
-type hints_expr =
- | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
- | HintsResolveIFF of bool * qualid list * int option
- | HintsImmediate of reference_or_constr list
- | HintsUnfold of qualid list
- | HintsTransparency of qualid hints_transparency_target * bool
- | HintsMode of qualid * hint_mode list
- | HintsConstructors of qualid list
- | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
-
-type import_level = [ `LAX | `WARN | `STRICT ]
-
-let warn_hint : import_level ref = ref `LAX
-let read_warn_hint () = match !warn_hint with
-| `LAX -> "Lax"
-| `WARN -> "Warn"
-| `STRICT -> "Strict"
-
-let write_warn_hint = function
-| "Lax" -> warn_hint := `LAX
-| "Warn" -> warn_hint := `WARN
-| "Strict" -> warn_hint := `STRICT
-| _ -> user_err Pp.(str "Only the following flags are accepted: Lax, Warn, Strict.")
-
-let () =
- Goptions.(declare_string_option
- { optdepr = false;
- optkey = ["Loose"; "Hint"; "Behavior"];
- optread = read_warn_hint;
- optwrite = write_warn_hint;
- })
+type import_level = HintLax | HintWarn | HintStrict
+
+let warn_hint_to_string = function
+| HintLax -> "Lax"
+| HintWarn -> "Warn"
+| HintStrict -> "Strict"
+
+let string_to_warn_hint = function
+| "Lax" -> HintLax
+| "Warn" -> HintWarn
+| "Strict" -> HintStrict
+| _ -> user_err Pp.(str "Only the following values are accepted: Lax, Warn, Strict.")
+
+let warn_hint =
+ Goptions.declare_interpreted_string_option_and_ref
+ ~depr:false
+ ~key:["Loose"; "Hint"; "Behavior"]
+ ~value:HintLax
+ string_to_warn_hint
+ warn_hint_to_string
let fresh_key =
let id = Summary.ref ~name:"HINT-COUNTER" 0 in
@@ -896,7 +878,7 @@ let fresh_global_or_constr env sigma poly cr =
else begin
if isgr then
warn_polymorphic_hint (pr_hint_term env sigma ctx cr);
- Declare.declare_universe_context ~poly:false ctx;
+ DeclareUctx.declare_universe_context ~poly:false ctx;
(c, Univ.ContextSet.empty)
end
@@ -1164,7 +1146,7 @@ let inAutoHint : hint_obj -> obj =
declare_object {(default_object "AUTOHINT") with
cache_function = cache_autohint;
load_function = load_autohint;
- open_function = open_autohint;
+ open_function = simple_open open_autohint;
subst_function = subst_autohint;
classify_function = classify_autohint; }
@@ -1311,114 +1293,6 @@ let prepare_hint check env init (sigma,c) =
let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
(c', diff)
-let project_hint ~poly pri l2r r =
- let open EConstr in
- let open Coqlib in
- let gr = Smartlocate.global_with_alias r in
- let env = Global.env() in
- let sigma = Evd.from_env env in
- 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 (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 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
- (mkApp (p,[|mkArrow a Sorts.Relevant (lift 1 b);mkArrow b Sorts.Relevant (lift 1 a);c|])) sign in
- let name =
- Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
- in
- let ctx = Evd.univ_entry ~poly sigma in
- let c = EConstr.to_constr sigma c in
- let cb = Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c)) in
- let c = Declare.declare_constant
- ~local:Declare.ImportDefaultBehavior
- ~name ~kind:Decls.(IsDefinition Definition) cb
- in
- 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
- let sigma = Evd.from_env env in
- let f poly c =
- let evd,c = Constrintern.interp_open_constr env sigma c in
- let env = Global.env () in
- let sigma = Evd.from_env env in
- let (c, diff) = prepare_hint true env sigma (evd,c) in
- if poly then IsConstr (c, diff)
- else
- let () = Declare.declare_universe_context ~poly:false diff in
- IsConstr (c, Univ.ContextSet.empty)
- in
- let fref r =
- let gr = global_with_alias r in
- Dumpglob.add_glob ?loc:r.CAst.loc gr;
- gr in
- let fr r = evaluable_of_global_reference env (fref r) in
- let fi c =
- match c with
- | HintsReference c ->
- let gr = global_with_alias c in
- (PathHints [gr], poly, IsGlobRef gr)
- | 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) =
- let path, poly, gr = fi r in
- let info = { info with hint_pattern = Option.map fp info.hint_pattern } in
- (info, poly, b, path, gr)
- in
- let ft = function
- | HintsVariables -> HintsVariables
- | HintsConstants -> HintsConstants
- | HintsReferences lhints -> HintsReferences (List.map fr lhints)
- in
- let fp = Constrintern.intern_constr_pattern (Global.env()) in
- match h with
- | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
- | HintsResolveIFF (l2r, lc, n) ->
- HintsResolveEntry (List.map (project_hint ~poly n l2r) lc)
- | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
- | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
- | HintsTransparency (t, b) -> HintsTransparencyEntry (ft t, b)
- | HintsMode (r, l) -> HintsModeEntry (fref r, l)
- | HintsConstructors lqid ->
- let constr_hints_of_ind qid =
- let ind = global_inductive_with_alias qid in
- let mib,_ = Global.lookup_inductive ind in
- Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind";
- List.init (nconstructors env ind)
- (fun i -> let c = (ind,i+1) in
- let gr = GlobRef.ConstructRef c in
- empty_hint_info,
- (Declareops.inductive_is_polymorphic mib), true,
- PathHints [gr], IsGlobRef gr)
- in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
- | HintsExtern (pri, patcom, tacexp) ->
- let pat = Option.map (fp sigma) patcom in
- let l = match pat with None -> [] | Some (l, _) -> l in
- let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
- let env = Genintern.({ (empty_glob_sign env) with ltacvars }) in
- let _, tacexp = Genintern.generic_intern env tacexp in
- HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
-
let add_hints ~locality dbnames h =
let local, superglobal = match locality with
| Goptions.OptDefault | Goptions.OptGlobal -> false, true
@@ -1563,8 +1437,7 @@ let pr_hint_term env sigma cl =
(* print all hints that apply to the concl of the current goal *)
let pr_applicable_hint pf =
let env = Global.env () in
- let pts = Proof_global.get_proof pf in
- let Proof.{goals;sigma} = Proof.data pts in
+ let Proof.{goals;sigma} = Proof.data pf in
match goals with
| [] -> CErrors.user_err Pp.(str "No focused goal.")
| g::_ ->
@@ -1690,12 +1563,12 @@ let wrap_hint_warning_fun env sigma t =
in
(ans, set_extra_data store sigma)
-let run_hint tac k = match !warn_hint with
-| `LAX -> k tac.obj
-| `WARN ->
+let run_hint tac k = match warn_hint () with
+| HintLax -> k tac.obj
+| HintWarn ->
if is_imported tac then k tac.obj
else Proofview.tclTHEN (log_hint tac) (k tac.obj)
-| `STRICT ->
+| HintStrict ->
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 9e11931247..f5fd3348e4 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -32,8 +32,6 @@ val empty_hint_info : 'a Typeclasses.hint_info_gen
(** Pre-created hint databases *)
-type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
-
type 'a hint_ast =
| Res_pf of 'a (* Hint Apply *)
| ERes_pf of 'a (* Hint EApply *)
@@ -78,10 +76,6 @@ type search_entry
type hint_entry
-type reference_or_constr =
- | HintsReference of Libnames.qualid
- | HintsConstr of Constrexpr.constr_expr
-
type hint_mode =
| ModeInput (* No evars *)
| ModeNoHeadEvar (* No evar at the head *)
@@ -92,16 +86,6 @@ type 'a hints_transparency_target =
| HintsConstants
| HintsReferences of 'a list
-type hints_expr =
- | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
- | HintsResolveIFF of bool * Libnames.qualid list * int option
- | HintsImmediate of reference_or_constr list
- | HintsUnfold of Libnames.qualid list
- | HintsTransparency of Libnames.qualid hints_transparency_target * bool
- | HintsMode of Libnames.qualid * hint_mode list
- | HintsConstructors of Libnames.qualid list
- | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
-
type 'a hints_path_gen =
| PathAtom of 'a hints_path_atom_gen
| PathStar of 'a hints_path_gen
@@ -217,8 +201,6 @@ val current_db_names : unit -> String.Set.t
val current_pure_db : unit -> hint_db list
-val interp_hints : poly:bool -> hints_expr -> hints_entry
-
val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit
val prepare_hint : bool (* Check no remaining evars *) ->
@@ -306,7 +288,7 @@ val wrap_hint_warning_fun : env -> evar_map ->
(** Printing hints *)
val pr_searchtable : env -> evar_map -> Pp.t
-val pr_applicable_hint : Proof_global.t -> Pp.t
+val pr_applicable_hint : Proof.t -> 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
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 8336fae02f..9164a4ff26 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -32,9 +32,9 @@ type internal_flag =
| UserIndividualRequest (* user action, a message is displayed *)
type mutual_scheme_object_function =
- internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
+ internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context
type individual_scheme_object_function =
- internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
+ internal_flag -> inductive -> constr Evd.in_evar_universe_context
type 'a scheme_kind = string
@@ -46,9 +46,13 @@ let pr_scheme_kind = Pp.str
type individual
type mutual
+type scheme_dependency =
+| SchemeMutualDep of MutInd.t * mutual scheme_kind
+| SchemeIndividualDep of inductive * individual scheme_kind
+
type scheme_object_function =
- | MutualSchemeFunction of mutual_scheme_object_function
- | IndividualSchemeFunction of individual_scheme_object_function
+ | MutualSchemeFunction of mutual_scheme_object_function * (MutInd.t -> scheme_dependency list) option
+ | IndividualSchemeFunction of individual_scheme_object_function * (inductive -> scheme_dependency list) option
let scheme_object_table =
(Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
@@ -68,11 +72,11 @@ let declare_scheme_object s aux f =
Hashtbl.add scheme_object_table key (s,f);
key
-let declare_mutual_scheme_object s ?(aux="") f =
- declare_scheme_object s aux (MutualSchemeFunction f)
+let declare_mutual_scheme_object s ?deps ?(aux="") f =
+ declare_scheme_object s aux (MutualSchemeFunction (f, deps))
-let declare_individual_scheme_object s ?(aux="") f =
- declare_scheme_object s aux (IndividualSchemeFunction f)
+let declare_individual_scheme_object s ?deps ?(aux="") f =
+ declare_scheme_object s aux (IndividualSchemeFunction (f, deps))
(**********************************************************************)
(* Defining/retrieving schemes *)
@@ -86,18 +90,24 @@ let compute_name internal id =
Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
else id
+let declare_definition_scheme = ref (fun ~internal ~univs ~role ~name c ->
+ CErrors.anomaly (Pp.str "scheme declaration not registered"))
+
+let lookup_scheme kind ind =
+ try Some (DeclareScheme.lookup_scheme kind ind) with Not_found -> None
+
+let check_scheme kind ind = Option.has_some (lookup_scheme kind ind)
+
let define internal role id c poly univs =
let id = compute_name internal id in
let ctx = UState.minimize univs in
let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
let univs = UState.univ_entry ~poly ctx in
- let entry = Declare.pure_definition_entry ~univs c in
- let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in
- let () = if internal then () else Declare.definition_message id in
- kn, eff
+ !declare_definition_scheme ~internal ~univs ~role ~name:id c
-let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
- let (c, ctx), eff = f mode ind in
+(* Assumes that dependencies are already defined *)
+let rec define_individual_scheme_base kind suff f mode idopt (mind,i as ind) eff =
+ let (c, ctx) = f mode ind in
let mib = Global.lookup_mind mind in
let id = match idopt with
| Some id -> id
@@ -105,17 +115,21 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
let role = Evd.Schema (ind, kind) in
let internal = mode == InternalTacticRequest in
let const, neff = define internal role id c (Declareops.inductive_is_polymorphic mib) ctx in
+ let eff = Evd.concat_side_effects neff eff in
DeclareScheme.declare_scheme kind [|ind,const|];
- const, Evd.concat_side_effects neff eff
+ const, eff
-let define_individual_scheme kind mode names (mind,i as ind) =
+and define_individual_scheme kind mode names (mind,i as ind) =
match Hashtbl.find scheme_object_table kind with
- | _,MutualSchemeFunction f -> assert false
- | s,IndividualSchemeFunction f ->
- define_individual_scheme_base kind s f mode names ind
-
-let define_mutual_scheme_base kind suff f mode names mind =
- let (cl, ctx), eff = f mode mind in
+ | _,MutualSchemeFunction _ -> assert false
+ | s,IndividualSchemeFunction (f, deps) ->
+ let deps = match deps with None -> [] | Some deps -> deps ind in
+ let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in
+ define_individual_scheme_base kind s f mode names ind eff
+
+(* Assumes that dependencies are already defined *)
+and define_mutual_scheme_base kind suff f mode names mind eff =
+ let (cl, ctx) = f mode mind in
let mib = Global.lookup_mind mind in
let ids = Array.init (Array.length mib.mind_packets) (fun i ->
try Int.List.assoc i names
@@ -131,34 +145,49 @@ let define_mutual_scheme_base kind suff f mode names mind =
DeclareScheme.declare_scheme kind schemes;
consts, eff
-let define_mutual_scheme kind mode names mind =
+and define_mutual_scheme kind mode names mind =
match Hashtbl.find scheme_object_table kind with
| _,IndividualSchemeFunction _ -> assert false
- | s,MutualSchemeFunction f ->
- define_mutual_scheme_base kind s f mode names mind
-
-let find_scheme_on_env_too kind ind =
- let s = DeclareScheme.lookup_scheme kind ind in
- s, Evd.empty_side_effects
+ | s,MutualSchemeFunction (f, deps) ->
+ let deps = match deps with None -> [] | Some deps -> deps mind in
+ let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in
+ define_mutual_scheme_base kind s f mode names mind eff
+
+and declare_scheme_dependence mode eff = function
+| SchemeIndividualDep (ind, kind) ->
+ if check_scheme kind ind then eff
+ else
+ let _, eff' = define_individual_scheme kind mode None ind in
+ Evd.concat_side_effects eff' eff
+| SchemeMutualDep (mind, kind) ->
+ if check_scheme kind (mind, 0) then eff
+ else
+ let _, eff' = define_mutual_scheme kind mode [] mind in
+ Evd.concat_side_effects eff' eff
let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
- try find_scheme_on_env_too kind ind
- with Not_found ->
+ let open Proofview.Notations in
+ match lookup_scheme kind ind with
+ | Some s ->
+ (* FIXME: we need to perform this call to reset the environment, since the
+ imperative scheme table is desynchronized from the monadic interface. *)
+ Proofview.tclEFFECTS Evd.empty_side_effects <*>
+ Proofview.tclUNIT s
+ | None ->
match Hashtbl.find scheme_object_table kind with
- | s,IndividualSchemeFunction f ->
- define_individual_scheme_base kind s f mode None ind
- | s,MutualSchemeFunction f ->
- let ca, eff = define_mutual_scheme_base kind s f mode [] mind in
- ca.(i), eff
+ | s,IndividualSchemeFunction (f, deps) ->
+ let deps = match deps with None -> [] | Some deps -> deps ind in
+ let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in
+ let c, eff = define_individual_scheme_base kind s f mode None ind eff in
+ Proofview.tclEFFECTS eff <*> Proofview.tclUNIT c
+ | s,MutualSchemeFunction (f, deps) ->
+ let deps = match deps with None -> [] | Some deps -> deps mind in
+ let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in
+ let ca, eff = define_mutual_scheme_base kind s f mode [] mind eff in
+ Proofview.tclEFFECTS eff <*> Proofview.tclUNIT ca.(i)
let define_individual_scheme kind mode names ind =
ignore (define_individual_scheme kind mode names ind)
let define_mutual_scheme kind mode names mind =
ignore (define_mutual_scheme kind mode names mind)
-
-let check_scheme kind ind =
- try let _ = find_scheme_on_env_too kind ind in true
- with Not_found -> false
-
-let lookup_scheme = DeclareScheme.lookup_scheme
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index dad2036c64..09fb051194 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -25,19 +25,27 @@ type internal_flag =
| InternalTacticRequest
| UserIndividualRequest
+type scheme_dependency =
+| SchemeMutualDep of MutInd.t * mutual scheme_kind
+| SchemeIndividualDep of inductive * individual scheme_kind
+
type mutual_scheme_object_function =
- internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
+ internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context
type individual_scheme_object_function =
- internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
+ internal_flag -> inductive -> constr Evd.in_evar_universe_context
(** Main functions to register a scheme builder. Note these functions
are not safe to be used by plugins as their effects won't be undone
on backtracking *)
-val declare_mutual_scheme_object : string -> ?aux:string ->
+val declare_mutual_scheme_object : string ->
+ ?deps:(MutInd.t -> scheme_dependency list) ->
+ ?aux:string ->
mutual_scheme_object_function -> mutual scheme_kind
-val declare_individual_scheme_object : string -> ?aux:string ->
+val declare_individual_scheme_object : string ->
+ ?deps:(inductive -> scheme_dependency list) ->
+ ?aux:string ->
individual_scheme_object_function ->
individual scheme_kind
@@ -51,11 +59,17 @@ val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -
(int * Id.t) list -> MutInd.t -> unit
(** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Evd.side_effects
-
-val check_scheme : 'a scheme_kind -> inductive -> bool
+val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t Proofview.tactic
-(** Like [find_scheme] but fails when the scheme is not already in the cache *)
-val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t
+(** Like [find_scheme] but does not generate a constant on the fly *)
+val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t option
val pr_scheme_kind : 'a scheme_kind -> Pp.t
+
+val declare_definition_scheme :
+ (internal : bool
+ -> univs:Entries.universes_entry
+ -> role:Evd.side_effect_role
+ -> name:Id.t
+ -> Constr.t
+ -> Constant.t * Evd.side_effects) ref
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
deleted file mode 100644
index 5a8ec404ee..0000000000
--- a/tactics/leminv.ml
+++ /dev/null
@@ -1,297 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* 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) *)
-(************************************************************************)
-
-open Pp
-open CErrors
-open Util
-open Names
-open Termops
-open Environ
-open Constr
-open Context
-open EConstr
-open Vars
-open Namegen
-open Evd
-open Printer
-open Reductionops
-open Inductiveops
-open Tacmach.New
-open Clenv
-open Tacticals.New
-open Tactics
-open Context.Named.Declaration
-
-module NamedDecl = Context.Named.Declaration
-
-let no_inductive_inconstr env sigma constr =
- (str "Cannot recognize an inductive predicate in " ++
- pr_leconstr_env env sigma constr ++
- str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++
- spc () ++ str "or of the type of constructors" ++ spc () ++
- str "is hidden by constant definitions.")
-
-(* Inversion stored in lemmas *)
-
-(* ALGORITHM:
-
- An inversion stored in a lemma is computed from a term-pattern, in
- a signature, as follows:
-
- Suppose we have an inductive relation, (I abar), in a signature Gamma:
-
- Gamma |- (I abar)
-
- Then we compute the free-variables of abar. Suppose that Gamma is
- thinned out to only include these.
-
- [We need technically to require that all free-variables of the
- types of the free variables of abar are themselves free-variables
- of abar. This needs to be checked, but it should not pose a
- problem - it is hard to imagine cases where it would not hold.]
-
- Now, we pose the goal:
-
- (P:(Gamma)Prop)(Gamma)(I abar)->(P vars[Gamma]).
-
- We execute the tactic:
-
- REPEAT Intro THEN (OnLastHyp (Inv NONE false o outSOME))
-
- This leaves us with some subgoals. All the assumptions after "P"
- in these subgoals are new assumptions. I.e. if we have a subgoal,
-
- P:(Gamma)Prop, Gamma, Hbar:Tbar |- (P ybar)
-
- then the assumption we needed to have was
-
- (Hbar:Tbar)(P ybar)
-
- So we construct all the assumptions we need, and rebuild the goal
- with these assumptions. Then, we can re-apply the same tactic as
- above, but instead of stopping after the inversion, we just apply
- the respective assumption in each subgoal.
-
- *)
-
-(* returns the sub_signature of sign corresponding to those identifiers that
- * are not global. *)
-(*
-let get_local_sign sign =
- let lid = ids_of_sign sign in
- let globsign = Global.named_context() in
- let add_local id res_sign =
- if not (mem_sign globsign id) then
- add_sign (lookup_sign id sign) res_sign
- else
- res_sign
- in
- List.fold_right add_local lid nil_sign
-*)
-(* returns the identifier of lid that was the latest declared in sign.
- * (i.e. is the identifier id of lid such that
- * sign_length (sign_prefix id sign) > sign_length (sign_prefix id' sign) >
- * for any id'<>id in lid).
- * it returns both the pair (id,(sign_prefix id sign)) *)
-(*
-let max_prefix_sign lid sign =
- let rec max_rec (resid,prefix) = function
- | [] -> (resid,prefix)
- | (id::l) ->
- let pre = sign_prefix id sign in
- if sign_length pre > sign_length prefix then
- max_rec (id,pre) l
- else
- max_rec (resid,prefix) l
- in
- match lid with
- | [] -> nil_sign
- | id::l -> snd (max_rec (id, sign_prefix id sign) l)
-*)
-let rec add_prods_sign env sigma t =
- match EConstr.kind sigma (whd_all env sigma t) with
- | Prod (na,c1,b) ->
- let id = id_of_name_using_hdchar env sigma t na.binder_name in
- let b'= subst1 (mkVar id) b in
- add_prods_sign (push_named (LocalAssum ({na with binder_name=id},c1)) env) sigma b'
- | LetIn (na,c1,t1,b) ->
- let id = id_of_name_using_hdchar env sigma t na.binder_name in
- let b'= subst1 (mkVar id) b in
- add_prods_sign (push_named (LocalDef ({na with binder_name=id},c1,t1)) env) sigma b'
- | _ -> (env,t)
-
-(* [dep_option] indicates whether the inversion lemma is dependent or not.
- If it is dependent and I is of the form (x_bar:T_bar)(I t_bar) then
- the stated goal will be (x_bar:T_bar)(H:(I t_bar))(P t_bar H)
- where P:(x_bar:T_bar)(H:(I x_bar))[sort].
- The generalisation of such a goal at the moment of the dependent case should
- be easy.
-
- If it is non dependent, then if [I]=(I t_bar) and (x_bar:T_bar) are the
- variables occurring in [I], then the stated goal will be:
- (x_bar:T_bar)(I t_bar)->(P x_bar)
- where P: P:(x_bar:T_bar)[sort].
-*)
-
-let compute_first_inversion_scheme env sigma ind sort dep_option =
- let indf,realargs = dest_ind_type ind in
- let allvars = vars_of_env env in
- let p = next_ident_away (Id.of_string "P") allvars in
- let pty,goal =
- if dep_option then
- let pty = make_arity env sigma true indf sort in
- let r = relevance_of_inductive_type env ind in
- let goal =
- mkProd
- (make_annot Anonymous r, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1]))
- in
- pty,goal
- else
- let i = mkAppliedInd ind in
- let ivars = global_vars env sigma i in
- let revargs,ownsign =
- fold_named_context
- (fun env d (revargs,hyps) ->
- let d = map_named_decl EConstr.of_constr d in
- let id = NamedDecl.get_id d in
- if Id.List.mem id ivars then
- ((mkVar id)::revargs, Context.Named.add d hyps)
- else
- (revargs,hyps))
- env ~init:([],[])
- in
- let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in
- let goal = mkArrow i Sorts.Relevant (applist(mkVar p, List.rev revargs)) in
- (pty,goal)
- in
- let npty = nf_all env sigma pty in
- let extenv = push_named (LocalAssum (make_annot p Sorts.Relevant,npty)) env in
- extenv, goal
-
-(* [inversion_scheme sign I]
-
- Given a local signature, [sign], and an instance of an inductive
- relation, [I], inversion_scheme will prove the associated inversion
- scheme on sort [sort]. Depending on the value of [dep_option] it will
- build a dependent lemma or a non-dependent one *)
-
-let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
- let (env,i) = add_prods_sign env sigma t in
- let ind =
- try find_rectype env sigma i
- with Not_found ->
- user_err ~hdr:"inversion_scheme" (no_inductive_inconstr env sigma i)
- in
- let (invEnv,invGoal) =
- compute_first_inversion_scheme env sigma ind sort dep_option
- in
- assert
- (List.subset
- (global_vars env sigma invGoal)
- (ids_of_named_context (named_context invEnv)));
- (*
- user_err ~hdr:"lemma_inversion"
- (str"Computed inversion goal was not closed in initial signature.");
- *)
- let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
- let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in
- let pfterm = List.hd (Proof.partial_proof pf) in
- let global_named_context = Global.named_context_val () in
- let ownSign = ref begin
- fold_named_context
- (fun env d sign ->
- let d = map_named_decl EConstr.of_constr d in
- if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign
- else Context.Named.add d sign)
- invEnv ~init:Context.Named.empty
- end in
- let avoid = ref Id.Set.empty in
- let Proof.{sigma} = Proof.data pf in
- let sigma = Evd.minimize_universes sigma in
- let rec fill_holes c =
- match EConstr.kind sigma c with
- | Evar (e,args) ->
- let h = next_ident_away (Id.of_string "H") !avoid in
- let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
- avoid := Id.Set.add h !avoid;
- ownSign := Context.Named.add (LocalAssum (make_annot h Sorts.Relevant,ty)) !ownSign;
- applist (mkVar h, inst)
- | _ -> EConstr.map sigma fill_holes c
- in
- let c = fill_holes pfterm in
- (* warning: side-effect on ownSign *)
- let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
- let p = EConstr.to_constr sigma invProof in
- p, sigma
-
-let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
- let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
- let univs = Evd.univ_entry ~poly sigma in
- let entry = Declare.definition_entry ~univs invProof in
- let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in
- ()
-
-(* inv_op = Inv (derives de complete inv. lemma)
- * inv_op = InvNoThining (derives de semi inversion lemma) *)
-
-let add_inversion_lemma_exn ~poly na com comsort bool tac =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in
- let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
- try
- add_inversion_lemma ~poly na env sigma c sort bool tac
- with
- | UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
- user_err ~hdr:"Inv needs Nodep Prop Set" s
-
-(* ================================= *)
-(* Applying a given inversion lemma *)
-(* ================================= *)
-
-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_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
- | NoSuchBinding ->
- user_err
- (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
- | UserError (a,b) ->
- user_err ~hdr:"LemInv"
- (str "Cannot refine current goal with the lemma " ++
- pr_leconstr_env (pf_env gls) (project gls) c)
- end
-
-let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id
-
-let lemInvIn id c ids =
- Proofview.Goal.enter begin fun gl ->
- let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
- let intros_replace_ids =
- let concl = Proofview.Goal.concl gl in
- let sigma = project gl in
- let nb_of_new_hyp = nb_prod sigma concl - List.length ids in
- if nb_of_new_hyp < 1 then
- intros_replacing ids
- else
- (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids))
- in
- ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c))
- (intros_replace_ids)))
- end
-
-let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id
-
-let lemInv_clause id c = function
- | [] -> lemInv_gen id c
- | l -> lemInvIn_gen id c l
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
deleted file mode 100644
index b228a04298..0000000000
--- a/tactics/pfedit.ml
+++ /dev/null
@@ -1,193 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* 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) *)
-(************************************************************************)
-
-open Pp
-open Util
-open Names
-open Environ
-open Evd
-
-let use_unification_heuristics_ref = ref true
-let () = Goptions.(declare_bool_option {
- optdepr = false;
- optkey = ["Solve";"Unification";"Constraints"];
- optread = (fun () -> !use_unification_heuristics_ref);
- optwrite = (fun a -> use_unification_heuristics_ref:=a);
-})
-
-let use_unification_heuristics () = !use_unification_heuristics_ref
-
-exception NoSuchGoal
-let () = CErrors.register_handler begin function
- | NoSuchGoal -> Some Pp.(str "No such goal.")
- | _ -> None
-end
-
-let get_nth_V82_goal p i =
- let Proof.{ sigma; goals } = Proof.data p in
- try { it = List.nth goals (i-1) ; sigma }
- with Failure _ -> raise NoSuchGoal
-
-let get_goal_context_gen pf i =
- let { it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in
- (sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
-
-let get_goal_context pf i =
- let p = Proof_global.get_proof pf in
- get_goal_context_gen p i
-
-let get_current_goal_context pf =
- let p = Proof_global.get_proof pf in
- try get_goal_context_gen p 1
- with
- | NoSuchGoal ->
- (* spiwack: returning empty evar_map, since if there is no goal,
- under focus, there is no accessible evar either. EJGA: this
- seems strange, as we have pf *)
- let env = Global.env () in
- Evd.from_env env, env
-
-let get_proof_context p =
- try get_goal_context_gen p 1
- with
- | NoSuchGoal ->
- (* No more focused goals *)
- let { Proof.sigma } = Proof.data p in
- sigma, Global.env ()
-
-let get_current_context pf =
- let p = Proof_global.get_proof pf in
- get_proof_context p
-
-let solve ?with_end_tac gi info_lvl tac pr =
- let tac = match with_end_tac with
- | None -> tac
- | Some etac -> Proofview.tclTHEN tac etac in
- let tac = match info_lvl with
- | None -> tac
- | Some _ -> Proofview.Trace.record_info_trace tac
- in
- let nosuchgoal = Proofview.tclZERO (Proof_bullet.SuggestNoSuchGoals (1,pr)) in
- let tac = let open Goal_select in match gi with
- | SelectAlreadyFocused ->
- let open Proofview.Notations in
- Proofview.numgoals >>= fun n ->
- if n == 1 then tac
- else
- let e = CErrors.UserError
- (None,
- Pp.(str "Expected a single focused goal but " ++
- int n ++ str " goals are focused."))
- in
- Proofview.tclZERO e
-
- | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
- | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
- | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac
- | SelectAll -> tac
- in
- let tac =
- if use_unification_heuristics () then
- Proofview.tclTHEN tac Refine.solve_constraints
- else tac
- in
- let env = Global.env () in
- let (p,(status,info),()) = Proof.run_tactic env tac pr in
- let env = Global.env () in
- let sigma = Evd.from_env env in
- let () =
- match info_lvl with
- | None -> ()
- | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info))
- in
- (p,status)
-
-let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None tac)
-
-(**********************************************************************)
-(* Shortcut to build a term using tactics *)
-
-let next = let n = ref 0 in fun () -> incr n; !n
-
-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
- 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 ~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 uctx ctx
- in
- 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
- current set of side-effects to be empty so that we can retrieve the
- ones created during the tactic invocation easily. *)
- let eff = Evd.eval_side_effects sigma in
- let sigma = Evd.drop_side_effects sigma in
- (* Save the existing goals *)
- let prev_future_goals = save_future_goals sigma in
- (* Start a proof *)
- let prf = Proof.start ~name ~poly sigma [env, ty] in
- let (prf, _, ()) =
- try Proof.run_tactic env tac prf
- with Logic_monad.TacticFailure e as src ->
- (* Catch the inner error of the monad tactic *)
- 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
- assert (stack = []);
- let ans = match Proofview.initial_goals entry with
- | [c, _] -> c
- | _ -> assert false
- in
- let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in
- (* [neff] contains the freshly generated side-effects *)
- let neff = Evd.eval_side_effects sigma in
- (* Reset the old side-effects *)
- let sigma = Evd.drop_side_effects sigma in
- let sigma = Evd.emit_side_effects eff sigma in
- (* Restore former goals *)
- let sigma = restore_future_goals sigma prev_future_goals in
- (* Push remaining goals as future_goals which is the only way we
- have to inform the caller that there are goals to collect while
- not being encapsulated in the monad *)
- (* Goals produced by tactic "shelve" *)
- let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in
- (* Goals produced by tactic "give_up" *)
- let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in
- (* Other goals *)
- let sigma = List.fold_right Evd.declare_future_goal goals sigma in
- (* Get rid of the fresh side-effects by internalizing them in the term
- itself. Note that this is unsound, because the tactic may have solved
- other goals that were already present during its invocation, so that
- those goals rely on effects that are not present anymore. Hopefully,
- this hack will work in most cases. *)
- let neff = neff.Evd.seff_private in
- let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in
- ans, sigma
diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli
deleted file mode 100644
index c49e997757..0000000000
--- a/tactics/pfedit.mli
+++ /dev/null
@@ -1,94 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* 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) *)
-(************************************************************************)
-
-(** Global proof state. A quite redundant wrapper on {!Proof_global}. *)
-
-open Names
-open Constr
-open Environ
-
-(** {6 ... } *)
-
-exception NoSuchGoal
-
-(** [get_goal_context n] returns the context of the [n]th subgoal of
- the current focused proof or raises a [UserError] if there is no
- focused proof or if there is no more subgoals *)
-
-val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env
-
-(** [get_current_goal_context ()] works as [get_goal_context 1] *)
-val get_current_goal_context : Proof_global.t -> Evd.evar_map * env
-
-(** [get_proof_context ()] gets the goal context for the first subgoal
- of the proof *)
-val get_proof_context : Proof.t -> Evd.evar_map * env
-
-(** [get_current_context ()] returns the context of the
- current focused goal. If there is no focused goal but there
- is a proof in progress, it returns the corresponding evar_map.
- If there is no pending proof then it returns the current global
- environment and empty evar_map. *)
-val get_current_context : Proof_global.t -> Evd.evar_map * env
-
-(** {6 ... } *)
-
-(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
- subgoal of the current focused proof. [solve SelectAll
- tac] applies [tac] to all subgoals. *)
-
-val solve : ?with_end_tac:unit Proofview.tactic ->
- Goal_select.t -> int option -> unit Proofview.tactic ->
- Proof.t -> Proof.t * bool
-
-(** [by tac] applies tactic [tac] to the 1st subgoal of the current
- focused proof.
- Returns [false] if an unsafe tactic has been used. *)
-
-val by : unit Proofview.tactic -> Proof_global.t -> Proof_global.t * bool
-
-(** Option telling if unification heuristics should be used. *)
-val use_unification_heuristics : unit -> bool
-
-(** [build_by_tactic typ tac] returns a term of type [typ] by calling
- [tac]. The return boolean, if [false] indicates the use of an unsafe
- tactic. *)
-
-val build_constant_by_tactic
- : name:Id.t
- -> ?opaque:Proof_global.opacity_flag
- -> uctx:UState.t
- -> sign:named_context_val
- -> poly:bool
- -> EConstr.types
- -> unit Proofview.tactic
- -> Evd.side_effects Declare.proof_entry * bool * UState.t
-
-val build_by_tactic
- : ?side_eff:bool
- -> env
- -> uctx:UState.t
- -> poly:bool
- -> typ:EConstr.types
- -> unit Proofview.tactic
- -> constr * types option * bool * UState.t
-
-val refine_by_tactic
- : name:Id.t
- -> poly:bool
- -> env -> Evd.evar_map
- -> EConstr.types
- -> unit Proofview.tactic
- -> constr * Evd.evar_map
-(** A variant of the above function that handles open terms as well.
- Caveat: all effects are purged in the returned term at the end, but other
- evars solved by side-effects are NOT purged, so that unexpected failures may
- occur. Ideally all code using this function should be rewritten in the
- monad. *)
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
deleted file mode 100644
index 623e6b8a42..0000000000
--- a/tactics/proof_global.ml
+++ /dev/null
@@ -1,285 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* 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) *)
-(************************************************************************)
-
-open Util
-open Names
-open Context
-
-module NamedDecl = Context.Named.Declaration
-
-(*** Proof Global Environment ***)
-
-type proof_object =
- { name : Names.Id.t
- ; entries : Evd.side_effects Declare.proof_entry list
- ; uctx: UState.t
- ; udecl : UState.universe_decl
- }
-
-type opacity_flag = Opaque | Transparent
-
-type t =
- { endline_tactic : Genarg.glob_generic_argument option
- ; section_vars : Id.Set.t option
- ; proof : Proof.t
- ; udecl: UState.universe_decl
- (** Initial universe declarations *)
- ; initial_euctx : UState.t
- (** The initial universe context (for the statement) *)
- }
-
-(*** Proof Global manipulation ***)
-
-let get_proof ps = ps.proof
-let get_proof_name ps = (Proof.data ps.proof).Proof.name
-
-let get_initial_euctx ps = ps.initial_euctx
-
-let map_proof f p = { p with proof = f p.proof }
-let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res
-
-let map_fold_proof_endline f ps =
- let et =
- match ps.endline_tactic with
- | None -> Proofview.tclUNIT ()
- | Some tac ->
- let open Geninterp in
- let {Proof.poly} = Proof.data ps.proof in
- let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in
- let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
- let tac = Geninterp.interp tag ist tac in
- Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
- in
- let (newpr,ret) = f et ps.proof in
- let ps = { ps with proof = newpr } in
- ps, ret
-
-let compact_the_proof pf = map_proof Proof.compact pf
-
-(* Sets the tactic to be used when a tactic line is closed with [...] *)
-let set_endline_tactic tac ps =
- { ps with endline_tactic = Some tac }
-
-(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
- name [name] with goals [goals] (a list of pairs of environment and
- conclusion). The proof is started in the evar map [sigma] (which
- can typically contain universe constraints), and with universe
- bindings [udecl]. *)
-let start_proof ~name ~udecl ~poly sigma goals =
- let proof = Proof.start ~name ~poly sigma goals in
- let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
- { proof
- ; endline_tactic = None
- ; section_vars = None
- ; udecl
- ; initial_euctx
- }
-
-let start_dependent_proof ~name ~udecl ~poly goals =
- let proof = Proof.dependent_start ~name ~poly goals in
- let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
- { proof
- ; endline_tactic = None
- ; section_vars = None
- ; udecl
- ; initial_euctx
- }
-
-let get_used_variables pf = pf.section_vars
-let get_universe_decl pf = pf.udecl
-
-let set_used_variables ps l =
- let open Context.Named.Declaration in
- let env = Global.env () in
- let ids = List.fold_right Id.Set.add l Id.Set.empty in
- let ctx = Environ.keep_hyps env ids in
- let ctx_set =
- List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
- let vars_of = Environ.global_vars_set in
- let aux env entry (ctx, all_safe as orig) =
- match entry with
- | LocalAssum ({binder_name=x},_) ->
- if Id.Set.mem x all_safe then orig
- else (ctx, all_safe)
- | LocalDef ({binder_name=x},bo, ty) as decl ->
- if Id.Set.mem x all_safe then orig else
- let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
- if Id.Set.subset vars all_safe
- then (decl :: ctx, Id.Set.add x all_safe)
- else (ctx, all_safe) in
- let ctx, _ =
- Environ.fold_named_context aux env ~init:(ctx,ctx_set) in
- if not (Option.is_empty ps.section_vars) then
- CErrors.user_err Pp.(str "Used section variables can be declared only once");
- (* EJGA: This is always empty thus we should modify the type *)
- (ctx, []), { ps with section_vars = Some (Context.Named.to_vars ctx) }
-
-let get_open_goals ps =
- let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
- List.length goals +
- List.fold_left (+) 0
- (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
- List.length shelf
-
-type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
-
-let private_poly_univs =
- let b = ref true in
- let _ = Goptions.(declare_bool_option {
- optdepr = false;
- optkey = ["Private";"Polymorphic";"Universes"];
- optread = (fun () -> !b);
- optwrite = ((:=) b);
- })
- in
- fun () -> !b
-
-let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
- (fpl : closed_proof_output Future.computation) ps =
- let { section_vars; proof; udecl; initial_euctx } = ps in
- let Proof.{ name; poly; entry } = Proof.data proof in
- let opaque = match opaque with Opaque -> true | Transparent -> false in
- let constrain_variables ctx =
- UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
- in
- let fpl, univs = Future.split2 fpl 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. *)
- let subst_evar k =
- 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 uctx) in
-
- let make_body =
- if poly || now then
- let make_body t (c, eff) =
- let body = c in
- let allow_deferred =
- not poly && (keep_body_ucst_separate ||
- not (Safe_typing.empty_private_constants = eff.Evd.seff_private))
- in
- let typ = if allow_deferred then t else nf t in
- let used_univs_body = Vars.universes_of_constr body in
- 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 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. *)
- let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
- let ctx_body = UState.restrict ctx used_univs in
- let univs = UState.check_mono_univ_decl ctx_body udecl in
- (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 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
- (UState.context_set universes)
- (UState.context_set typus)
- in
- (udecl, typ), ((body, ubody), eff)
- else
- (* Since the proof is computed now, we can simply have 1 set of
- constraints in which we merge the ones for the body and the ones
- for the typ. We recheck the declaration after restricting with
- 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 uctx used_univs in
- let univs = UState.check_univ_decl ~poly ctx udecl in
- (univs, typ), ((body, Univ.ContextSet.empty), eff)
- in
- fun t p -> Future.split2 (Future.chain p (make_body t))
- else
- fun t p ->
- (* Already checked the univ_decl for the type universes when starting the proof. *)
- 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) ->
- (* Deferred proof, we already checked the universe declaration with
- the initial universes, ensure that the final universes respect
- the declaration as well. If the declaration is non-extensible,
- this will prevent the body from adding universes and constraints. *)
- let univs = Future.force univs in
- let univs = constrain_variables univs in
- let used_univs = Univ.LSet.union
- (Vars.universes_of_constr t)
- (Vars.universes_of_constr pt)
- in
- let univs = UState.restrict univs used_univs in
- let univs = UState.check_mono_univ_decl univs udecl in
- (pt,univs),eff)
- in
- let entry_fn p (_, t) =
- let t = EConstr.Unsafe.to_constr t in
- let univstyp, body = make_body t p in
- let univs, typ = Future.force univstyp in
- 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; uctx; udecl }
-
-let return_proof ?(allow_partial=false) ps =
- let { proof } = ps in
- if allow_partial then begin
- let proofs = Proof.partial_proof proof in
- let Proof.{sigma=evd} = Proof.data proof in
- let eff = Evd.eval_side_effects evd in
- (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
- side-effects... This may explain why one need to uniquize side-effects
- thereafter... *)
- let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
- proofs, Evd.evar_universe_context evd
- end else
- let Proof.{name=pid;entry} = Proof.data proof in
- let initial_goals = Proofview.initial_goals entry in
- let evd = Proof.return ~pid proof in
- let eff = Evd.eval_side_effects evd in
- let evd = Evd.minimize_universes evd in
- let proof_opt c =
- match EConstr.to_constr_opt evd c with
- | Some p -> p
- | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
- in
- (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
- side-effects... This may explain why one need to uniquize side-effects
- thereafter... *)
- (* EJGA: actually side-effects de-duplication and this codepath is
- unrelated. Duplicated side-effects arise from incorrect scheme
- generation code, the main bulk of it was mostly fixed by #9836
- but duplication can still happen because of rewriting schemes I
- think; however the code below is mostly untested, the only
- code-paths that generate several proof entries are derive and
- equations and so far there is no code in the CI that will
- actually call those and do a side-effect, TTBOMK *)
- let proofs =
- List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
- proofs, Evd.evar_universe_context evd
-
-let close_future_proof ~opaque ~feedback_id ps proof =
- close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps
-
-let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps =
- close_proof ~opaque ~keep_body_ucst_separate ~now:true
- (Future.from_val ~fix_exn (return_proof ps)) ps
-
-let update_global_env =
- map_proof (fun p ->
- let { Proof.sigma } = Proof.data p in
- let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
- let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in
- p)
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
deleted file mode 100644
index e1c75c0649..0000000000
--- a/tactics/proof_global.mli
+++ /dev/null
@@ -1,99 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* 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) *)
-(************************************************************************)
-
-(** State for interactive proofs. *)
-
-type t
-
-(* Should be moved into a proper view *)
-val get_proof : t -> Proof.t
-val get_proof_name : t -> Names.Id.t
-val get_used_variables : t -> Names.Id.Set.t option
-
-(** Get the universe declaration associated to the current proof. *)
-val get_universe_decl : t -> UState.universe_decl
-
-(** Get initial universe state *)
-val get_initial_euctx : t -> UState.t
-
-val compact_the_proof : t -> t
-
-(** When a proof is closed, it is reified into a [proof_object] *)
-type proof_object =
- { name : Names.Id.t
- (** name of the proof *)
- ; entries : Evd.side_effects Declare.proof_entry list
- (** list of the proof terms (in a form suitable for definitions). *)
- ; uctx: UState.t
- (** universe state *)
- ; udecl : UState.universe_decl
- (** universe declaration *)
- }
-
-type opacity_flag = Opaque | Transparent
-
-(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
- name [name] with goals [goals] (a list of pairs of environment and
- conclusion); [poly] determines if the proof is universe
- polymorphic. The proof is started in the evar map [sigma] (which
- can typically contain universe constraints), and with universe
- bindings [udecl]. *)
-val start_proof
- : name:Names.Id.t
- -> udecl:UState.universe_decl
- -> poly:bool
- -> Evd.evar_map
- -> (Environ.env * EConstr.types) list
- -> t
-
-(** Like [start_proof] except that there may be dependencies between
- initial goals. *)
-val start_dependent_proof
- : name:Names.Id.t
- -> udecl:UState.universe_decl
- -> poly:bool
- -> Proofview.telescope
- -> t
-
-(** Update the proofs global environment after a side-effecting command
- (e.g. a sublemma definition) has been run inside it. Assumes
- there_are_pending_proofs. *)
-val update_global_env : t -> t
-
-(* Takes a function to add to the exceptions data relative to the
- state in which the proof was built *)
-val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> proof_object
-
-(* Intermediate step necessary to delegate the future.
- * Both access the current proof state. The former is supposed to be
- * chained with a computation that completed the proof *)
-
-type closed_proof_output
-
-(* If allow_partial is set (default no) then an incomplete proof
- * is allowed (no error), and a warn is given if the proof is complete. *)
-val return_proof : ?allow_partial:bool -> t -> closed_proof_output
-val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t ->
- closed_proof_output Future.computation -> proof_object
-
-val get_open_goals : t -> int
-
-val map_proof : (Proof.t -> Proof.t) -> t -> t
-val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a
-val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
-
-(** Sets the tactic to be used when a tactic line is closed with [...] *)
-val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
-
-(** Sets the section variables assumed by the proof, returns its closure
- * (w.r.t. type dependencies and let-ins covered by it) + a list of
- * ids to be cleared *)
-val set_used_variables : t ->
- Names.Id.t list -> (Constr.named_context * Names.lident list) * t
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index 250c80d9a5..f681e4e99e 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -37,7 +37,7 @@ let warn_native_compute_disabled =
strbrk "native_compute disabled at configure time; falling back to vm_compute.")
let cbv_native env sigma c =
- if Coq_config.native_compiler then
+ if Flags.get_native_compiler () then
let ctyp = Retyping.get_type_of env sigma c in
Nativenorm.native_norm env sigma c ctyp
else
@@ -53,13 +53,8 @@ let whd_cbn flags env sigma t =
let strong_cbn flags =
strong_with_flags whd_cbn flags
-let simplIsCbn = ref (false)
-let () = Goptions.(declare_bool_option {
- optdepr = false;
- optkey = ["SimplIsCbn"];
- optread = (fun () -> !simplIsCbn);
- optwrite = (fun a -> simplIsCbn:=a);
-})
+let simplIsCbn =
+ Goptions.declare_bool_option_and_ref ~depr:false ~key:["SimplIsCbn"] ~value:false
let set_strategy_one ref l =
let k =
@@ -228,10 +223,10 @@ let reduction_of_red_expr env =
else (e_red red_product,DEFAULTcast)
| Hnf -> (e_red hnf_constr,DEFAULTcast)
| Simpl (f,o) ->
- let whd_am = if !simplIsCbn then whd_cbn (make_flag f) else whd_simpl in
- let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in
+ let whd_am = if simplIsCbn () then whd_cbn (make_flag f) else whd_simpl in
+ let am = if simplIsCbn () then strong_cbn (make_flag f) else simpl in
let () =
- if not (!simplIsCbn || List.is_empty f.rConst) then
+ if not (simplIsCbn () || List.is_empty f.rConst) then
warn_simpl_unfolding_modifiers () in
(contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
| Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 8f6844079b..07f9def2c8 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -368,6 +368,9 @@ module New = struct
Proofview.Unsafe.tclNEWGOALS tl <*>
Proofview.tclUNIT ans
+ let tclTHENSLASTn t1 repeat l =
+ tclTHENS3PARTS t1 [||] repeat l
+
let tclTHENLASTn t1 l =
tclTHENS3PARTS t1 [||] (tclUNIT()) l
let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|]
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 9ec558f1ad..01565169ca 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -180,6 +180,7 @@ module New : sig
middle. Raises an error if the number of resulting subgoals is
strictly less than [n+m] *)
val tclTHENS3PARTS : unit tactic -> unit tactic array -> unit tactic -> unit tactic array -> unit tactic
+ val tclTHENSLASTn : unit tactic -> unit tactic -> unit tactic array -> unit tactic
val tclTHENSFIRSTn : unit tactic -> unit tactic array -> unit tactic -> unit tactic
val tclTHENFIRSTn : unit tactic -> unit tactic array -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 30ca024a2f..e4809332c5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1223,7 +1223,7 @@ let rec intros_move = function
or a term with bindings *)
let tactic_infer_flags with_evar = {
- Pretyping.use_typeclasses = true;
+ Pretyping.use_typeclasses = Pretyping.UseTC;
Pretyping.solve_unification_constraints = true;
Pretyping.fail_evar = not with_evar;
Pretyping.expand_evars = true;
@@ -1368,7 +1368,7 @@ let clenv_refine_in with_evars targetid id sigma0 clenv tac =
if not with_evars && occur_meta clenv.evd new_hyp_typ then
error_uninstantiated_metas new_hyp_typ clenv;
let new_hyp_prf = clenv_value clenv in
- let exact_tac = Proofview.V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf)) in
+ let exact_tac = Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in
let naming = NamingMustBe (CAst.make targetid) in
let with_clear = do_replace (Some id) naming in
Tacticals.New.tclTHEN
@@ -1670,7 +1670,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
| Some (p,pt) ->
Tacticals.New.tclTHENS
(assert_before_gen false (NamingAvoid avoid) pt)
- [Proofview.V82.tactic (refiner ~check:true EConstr.Unsafe.(to_constr p));
+ [refiner ~check:true EConstr.Unsafe.(to_constr p);
(* Might be ill-typed due to forbidden elimination. *)
Tacticals.New.onLastHypId (tac (not isrec))]
end)))
@@ -2763,8 +2763,8 @@ let pose_tac na c =
let id = make_annot id Sorts.Relevant in
let nhyps = EConstr.push_named_context_val (NamedDecl.LocalDef (id, c, t)) hyps in
let (sigma, ev) = Evarutil.new_pure_evar nhyps sigma concl in
- let inst = Array.map_of_list (fun d -> mkVar (get_id d)) (named_context env) in
- let body = mkEvar (ev, Array.append [|mkRel 1|] inst) in
+ let inst = List.map (fun d -> mkVar (get_id d)) (named_context env) in
+ let body = mkEvar (ev, mkRel 1 :: inst) in
(sigma, mkLetIn (map_annot Name.mk_name id, c, t, body))
end
end
@@ -4499,7 +4499,7 @@ let check_expected_type env sigma (elimc,bl) elimt =
if n == 0 then error "Scheme cannot be applied.";
let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in
let sigma = solve_evar_clause env sigma true cl bl in
- let (_,u,_) = destProd sigma cl.cl_concl in
+ let (_,u,_) = destProd sigma (whd_all env sigma cl.cl_concl) in
fun t -> match Evarconv.unify_leq_delay env sigma t u with
| _sigma -> true
| exception Evarconv.UnableToUnify _ -> false
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 0c4e496650..36d61feed1 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,7 +1,4 @@
DeclareScheme
-Declare
-Proof_global
-Pfedit
Dnet
Dn
Btermdn
@@ -20,7 +17,7 @@ Elim
Equality
Contradiction
Inv
-Leminv
+DeclareUctx
Hints
Auto
Eauto
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 18:35:25 +0000