aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/abstract.ml12
-rw-r--r--tactics/auto.ml77
-rw-r--r--tactics/autorewrite.ml13
-rw-r--r--tactics/class_tactics.ml4
-rw-r--r--tactics/class_tactics.mli18
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/genredexpr.ml79
-rw-r--r--tactics/hints.ml31
-rw-r--r--tactics/ind_tables.ml10
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/leminv.ml8
-rw-r--r--tactics/ppred.ml83
-rw-r--r--tactics/ppred.mli19
-rw-r--r--tactics/redexpr.ml278
-rw-r--r--tactics/redexpr.mli48
-rw-r--r--tactics/redops.ml64
-rw-r--r--tactics/redops.mli20
-rw-r--r--tactics/tacticals.ml6
-rw-r--r--tactics/tacticals.mli1
-rw-r--r--tactics/tactics.ml43
-rw-r--r--tactics/tactics.mllib4
-rw-r--r--tactics/term_dnet.ml4
22 files changed, 710 insertions, 116 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 3c262de910..3a687a6b41 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -76,7 +76,7 @@ let shrink_entry sign const =
| None -> assert false
| Some t -> t
in
- (** The body has been forced by the call to [build_constant_by_tactic] *)
+ (* The body has been forced by the call to [build_constant_by_tactic] *)
let () = assert (Future.is_over const.const_entry_body) in
let ((body, uctx), eff) = Future.force const.const_entry_body in
let (body, typ, ctx) = decompose (List.length sign) body typ [] in
@@ -140,18 +140,18 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in
let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in
let cst () =
- (** do not compute the implicit arguments, it may be costly *)
+ (* 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*)
+ (* ppedrot: seems legit to have abstracted subproofs as local*)
Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl
in
let cst = Impargs.with_implicit_protection cst () in
let inst = match const.Entries.const_entry_universes with
| Entries.Monomorphic_const_entry _ -> EInstance.empty
| Entries.Polymorphic_const_entry (_, ctx) ->
- (** We mimick what the kernel does, that is ensuring that no additional
- constraints appear in the body of polymorphic constants. Ideally this
- should be enforced statically. *)
+ (* We mimick what the kernel does, that is ensuring that no additional
+ constraints appear in the body of polymorphic constants. Ideally this
+ should be enforced statically. *)
let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in
let () = assert (Univ.ContextSet.is_empty body_uctx) in
EInstance.make (Univ.UContext.instance ctx)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 441fb68acc..2619620eb8 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -70,19 +70,19 @@ let auto_unif_flags =
(* Try unification with the precompiled clause, then use registered Apply *)
let connect_hint_clenv poly (c, _, ctx) clenv gl =
- (** [clenv] has been generated by a hint-making function, so the only relevant
- data in its evarmap is the set of metas. The [evar_reset_evd] function
- below just replaces the metas of sigma by those coming from the clenv. *)
+ (* [clenv] has been generated by a hint-making function, so the only relevant
+ data in its evarmap is the set of metas. The [evar_reset_evd] function
+ below just replaces the metas of sigma by those coming from the clenv. *)
let sigma = Tacmach.New.project gl in
let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
- (** Still, we need to update the universes *)
+ (* Still, we need to update the universes *)
let clenv, c =
if poly then
- (** Refresh the instance of the hint *)
+ (* Refresh the instance of the hint *)
let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
let emap c = Vars.subst_univs_level_constr subst c in
let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
- (** Only metas are mentioning the old universes. *)
+ (* Only metas are mentioning the old universes. *)
let clenv = {
templval = Evd.map_fl emap clenv.templval;
templtyp = Evd.map_fl emap clenv.templtyp;
@@ -211,30 +211,30 @@ let tclLOG (dbg,_,depth,trace) pp tac =
match dbg with
| Off -> tac
| Debug ->
- (* For "debug (trivial/auto)", we directly output messages *)
+ (* For "debug (trivial/auto)", we directly output messages *)
let s = String.make (depth+1) '*' in
- Proofview.V82.tactic begin fun gl ->
- try
- let out = Proofview.V82.of_tactic tac gl in
- Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
- out
- with reraise ->
- let reraise = CErrors.push reraise in
- Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
- iraise reraise
- end
+ Proofview.(tclIFCATCH (
+ tac >>= fun v ->
+ tclENV >>= fun env ->
+ tclEVARMAP >>= fun sigma ->
+ Feedback.msg_debug (str s ++ spc () ++ pp env sigma ++ str ". (*success*)");
+ tclUNIT v
+ ) tclUNIT
+ (fun (exn, info) ->
+ tclENV >>= fun env ->
+ tclEVARMAP >>= fun sigma ->
+ Feedback.msg_debug (str s ++ spc () ++ pp env sigma ++ str ". (*fail*)");
+ tclZERO ~info exn))
| Info ->
(* For "info (trivial/auto)", we store a log trace *)
- Proofview.V82.tactic begin fun gl ->
- try
- let out = Proofview.V82.of_tactic tac gl in
- trace := (depth, Some pp) :: !trace;
- out
- with reraise ->
- let reraise = CErrors.push reraise in
- trace := (depth, None) :: !trace;
- iraise reraise
- end
+ Proofview.(tclIFCATCH (
+ tac >>= fun v ->
+ trace := (depth, Some pp) :: !trace;
+ tclUNIT v
+ ) Proofview.tclUNIT
+ (fun (exn, info) ->
+ trace := (depth, None) :: !trace;
+ tclZERO ~info exn))
(** For info, from the linear trace information, we reconstitute the part
of the proof tree we're interested in. The last executed tactic
@@ -252,12 +252,12 @@ and erase_subtree depth = function
| [] -> []
| (d,_) :: l -> if Int.equal d depth then l else erase_subtree depth l
-let pr_info_atom (d,pp) =
- str (String.make d ' ') ++ pp () ++ str "."
+let pr_info_atom env sigma (d,pp) =
+ str (String.make d ' ') ++ pp env sigma ++ str "."
-let pr_info_trace = function
+let pr_info_trace env sigma = function
| (Info,_,_,{contents=(d,Some pp)::l}) ->
- Feedback.msg_info (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l))
+ Feedback.msg_info (prlist_with_sep fnl (pr_info_atom env sigma) (cleanup_info_trace d [(d,pp)] l))
| _ -> ()
let pr_info_nop = function
@@ -273,8 +273,12 @@ let pr_dbg_header = function
let tclTRY_dbg d tac =
let delay f = Proofview.tclUNIT () >>= fun () -> f () in
- let tac = delay (fun () -> pr_dbg_header d; tac) >>=
- fun () -> pr_info_trace d; Proofview.tclUNIT () in
+ let tac =
+ delay (fun () -> pr_dbg_header d; tac) >>= fun () ->
+ Proofview.tclENV >>= fun env ->
+ Proofview.tclEVARMAP >>= fun sigma ->
+ pr_info_trace env sigma d;
+ Proofview.tclUNIT () in
let after = delay (fun () -> pr_info_nop d; Proofview.tclUNIT ()) in
Tacticals.New.tclORELSE0 tac after
@@ -304,8 +308,8 @@ let exists_evaluable_reference env = function
| EvalConstRef _ -> true
| EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false
-let dbg_intro dbg = tclLOG dbg (fun () -> str "intro") intro
-let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption
+let dbg_intro dbg = tclLOG dbg (fun _ _ -> str "intro") intro
+let dbg_assumption dbg = tclLOG dbg (fun _ _ -> str "assumption") assumption
let rec trivial_fail_db dbg mod_delta db_list local_db =
let intro_tac =
@@ -389,12 +393,11 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
| Extern tacast ->
conclPattern concl p tacast
in
- let pr_hint () =
+ let pr_hint env sigma =
let origin = match dbname with
| None -> mt ()
| Some n -> str " (in " ++ str n ++ str ")"
in
- let sigma, env = Pfedit.get_current_context () in
pr_hint env sigma t ++ origin
in
tclLOG dbg pr_hint (run_hint t tactic)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 76cbdee0d5..f824552705 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -196,17 +196,12 @@ let subst_hintrewrite (subst,(rbase,list as node)) =
if list' == list then node else
(rbase,list')
-let classify_hintrewrite x = Libobject.Substitute x
-
-
(* Declaration of the Hint Rewrite library object *)
let inHintRewrite : string * HintDN.t -> Libobject.obj =
- Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with
- Libobject.cache_function = cache_hintrewrite;
- Libobject.load_function = (fun _ -> cache_hintrewrite);
- Libobject.subst_function = subst_hintrewrite;
- Libobject.classify_function = classify_hintrewrite }
-
+ let open Libobject in
+ declare_object @@ superglobal_object_nodischarge "HINT_REWRITE"
+ ~cache:cache_hintrewrite
+ ~subst:(Some subst_hintrewrite)
open Clenv
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index fd2a163f80..ba7645446d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1096,8 +1096,8 @@ let resolve_all_evars debug depth unique env p oevd do_split fail =
let initial_select_evars filter =
fun evd ev evi ->
filter ev (Lazy.from_val (snd evi.Evd.evar_source)) &&
- (** Typeclass evars can contain evars whose conclusion is not
- yet determined to be a class or not. *)
+ (* Typeclass evars can contain evars whose conclusion is not
+ yet determined to be a class or not. *)
Typeclasses.is_class_evar evd evi
let resolve_typeclass_evars debug depth unique env evd filter split fail =
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 46dff34f89..a6922213d0 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -39,20 +39,20 @@ val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
module Search : sig
val eauto_tac :
- ?st:TransparentState.t ->
+ ?st:TransparentState.t
(** The transparent_state used when working with local hypotheses *)
- ?unique:bool ->
+ -> ?unique:bool
(** Should we force a unique solution *)
- only_classes:bool ->
+ -> only_classes:bool
(** Should non-class goals be shelved and resolved at the end *)
- ?strategy:search_strategy ->
+ -> ?strategy:search_strategy
(** Is a traversing-strategy specified? *)
- depth:Int.t option ->
+ -> depth:Int.t option
(** Bounded or unbounded search *)
- dep:bool ->
+ -> dep:bool
(** Should the tactic be made backtracking on the initial goals,
- whatever their internal dependencies are. *)
- Hints.hint_db list ->
+ whatever their internal dependencies are. *)
+ -> Hints.hint_db list
(** The list of hint databases to use *)
- unit Proofview.tactic
+ -> unit Proofview.tactic
end
diff --git a/tactics/equality.ml b/tactics/equality.ml
index bdc95941b2..769e702da1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1742,7 +1742,7 @@ let subst_one_var dep_proof_ok x =
(* Find a non-recursive definition for x *)
let res =
try
- (** [is_eq_x] ensures nf_evar on its side *)
+ (* [is_eq_x] ensures nf_evar on its side *)
let hyps = Proofview.Goal.hyps gl in
let test hyp _ = is_eq_x gl x hyp in
Context.Named.fold_outside test ~init:() hyps;
diff --git a/tactics/genredexpr.ml b/tactics/genredexpr.ml
new file mode 100644
index 0000000000..8209684c37
--- /dev/null
+++ b/tactics/genredexpr.ml
@@ -0,0 +1,79 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** Reduction expressions *)
+
+(** The parsing produces initially a list of [red_atom] *)
+
+type 'a red_atom =
+ | FBeta
+ | FMatch
+ | FFix
+ | FCofix
+ | FZeta
+ | FConst of 'a list
+ | FDeltaBut of 'a list
+
+(** This list of atoms is immediately converted to a [glob_red_flag] *)
+
+type 'a glob_red_flag = {
+ rBeta : bool;
+ rMatch : bool;
+ rFix : bool;
+ rCofix : bool;
+ rZeta : bool;
+ rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
+ rConst : 'a list
+}
+
+(** Generic kinds of reductions *)
+
+type ('a,'b,'c) red_expr_gen =
+ | Red of bool
+ | Hnf
+ | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option
+ | Cbv of 'b glob_red_flag
+ | Cbn of 'b glob_red_flag
+ | Lazy of 'b glob_red_flag
+ | Unfold of 'b Locus.with_occurrences list
+ | Fold of 'a list
+ | Pattern of 'a Locus.with_occurrences list
+ | ExtraRedExpr of string
+ | CbvVm of ('b,'c) Util.union Locus.with_occurrences option
+ | CbvNative of ('b,'c) Util.union Locus.with_occurrences option
+
+type ('a,'b,'c) may_eval =
+ | ConstrTerm of 'a
+ | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
+ | ConstrContext of Names.lident * 'a
+ | ConstrTypeOf of 'a
+
+open Libnames
+open Constrexpr
+
+type r_trm = constr_expr
+type r_pat = constr_pattern_expr
+type r_cst = qualid or_by_notation
+
+type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
+
+let make0 ?dyn name =
+ let wit = Genarg.make0 name in
+ let () = Geninterp.register_val0 wit dyn in
+ wit
+
+type 'a and_short_name = 'a * Names.lident option
+
+let wit_red_expr :
+ ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen,
+ (Genintern.glob_constr_and_expr,Names.evaluable_global_reference and_short_name Locus.or_var,Genintern.glob_constr_pattern_and_expr) red_expr_gen,
+ (EConstr.t,Names.evaluable_global_reference,Pattern.constr_pattern) red_expr_gen)
+ Genarg.genarg_type =
+ make0 "redexpr"
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 77479f9efa..571ad9d160 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -210,9 +210,9 @@ let fresh_key =
let lbl = Id.of_string ("_" ^ string_of_int cur) in
let kn = Lib.make_kn lbl in
let (mp, _) = KerName.repr kn in
- (** We embed the full path of the kernel name in the label so that the
- identifier should be unique. This ensures that including two modules
- together won't confuse the corresponding labels. *)
+ (* We embed the full path of the kernel name in the label so that
+ the identifier should be unique. This ensures that including
+ two modules together won't confuse the corresponding labels. *)
let lbl = Id.of_string_soft (Printf.sprintf "%s#%i"
(ModPath.to_string mp) cur)
in
@@ -558,7 +558,7 @@ struct
let realize_tac secvars (id,tac) =
if Id.Pred.subset tac.secvars secvars then Some tac
else
- (** Warn about no longer typable hint? *)
+ (* Warn about no longer typable hint? *)
None
let head_evar sigma c =
@@ -601,7 +601,7 @@ struct
let se = find k db in
merge_entry secvars db se.sentry_nopat se.sentry_pat
- (** Precondition: concl has no existentials *)
+ (* Precondition: concl has no existentials *)
let map_auto sigma ~secvars (k,args) concl db =
let se = find k db in
let st = if db.use_dn then (Some db.hintdb_state) else None in
@@ -644,7 +644,7 @@ struct
| None ->
let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in
if not (List.exists is_present db.hintdb_nopat) then
- (** FIXME *)
+ (* FIXME *)
{ db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
else db
| Some gr ->
@@ -738,7 +738,6 @@ module Hintdbmap = String.Map
type hint_db = Hint_db.t
(** Initially created hint databases, for typeclasses and rewrite *)
-
let typeclasses_db = "typeclass_instances"
let rewrite_db = "rewrite"
@@ -1064,12 +1063,12 @@ let cache_autohint (kn, obj) =
let subst_autohint (subst, obj) =
let subst_key gr =
- let (lab'', elab') = subst_global subst gr in
- let elab' = EConstr.of_constr elab' in
- let gr' =
- (try head_constr_bound Evd.empty elab'
- with Bound -> lab'')
- in if gr' == gr then gr else gr'
+ let (gr', t) = subst_global subst gr in
+ match t with
+ | None -> gr'
+ | Some t ->
+ (try head_constr_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)
+ with Bound -> gr')
in
let subst_hint (k,data as hint) =
let k' = Option.Smart.map subst_key k in
@@ -1517,8 +1516,8 @@ let pr_hint_term env sigma cl =
let pr_applicable_hint () =
let env = Global.env () in
let pts = Proof_global.give_me_the_proof () in
- let glss,_,_,_,sigma = Proof.proof pts in
- match glss with
+ let Proof.{goals;sigma} = Proof.data pts in
+ match goals with
| [] -> CErrors.user_err Pp.(str "No focused goal.")
| g::_ ->
pr_hint_term env sigma (Goal.V82.concl sigma g)
@@ -1586,7 +1585,7 @@ let log_hint h =
let store = get_extra_data sigma in
match Store.get store hint_trace with
| None ->
- (** All calls to hint logging should be well-scoped *)
+ (* All calls to hint logging should be well-scoped *)
assert false
| Some trace ->
let trace = KNmap.add h.uid h trace in
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index a53e3bf20d..a67f5f6d6e 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -59,12 +59,10 @@ let discharge_scheme (_,(kind,l)) =
Some (kind, l)
let inScheme : string * (inductive * Constant.t) array -> obj =
- declare_object {(default_object "SCHEME") with
- cache_function = cache_scheme;
- load_function = (fun _ -> cache_scheme);
- subst_function = subst_scheme;
- classify_function = (fun obj -> Substitute obj);
- discharge_function = discharge_scheme}
+ declare_object @@ superglobal_object "SCHEME"
+ ~cache:cache_scheme
+ ~subst:(Some subst_scheme)
+ ~discharge:discharge_scheme
(**********************************************************************)
(* The table of scheme building functions *)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 6a39a10fc4..2ae37ab471 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -365,7 +365,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
let substHypIfVariable tac id =
Proofview.Goal.enter begin fun gl ->
let sigma = project gl in
- (** We only look at the type of hypothesis "id" *)
+ (* We only look at the type of hypothesis "id" *)
let hyp = pf_nf_evar gl (pf_get_hyp_typ id gl) in
let (t,t1,t2) = dest_nf_eq (pf_env gl) sigma hyp in
match (EConstr.kind sigma t1, EConstr.kind sigma t2) with
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index caf4c1eca3..356b43ec14 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -183,7 +183,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
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 env sigma t sort dep_option inv_op =
+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
@@ -201,7 +201,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
user_err ~hdr:"lemma_inversion"
(str"Computed inversion goal was not closed in initial signature.");
*)
- let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
+ let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
let pf =
fst (Proof.run_tactic env (
tclTHEN intro (onLastHypId inv_op)) pf)
@@ -217,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
invEnv ~init:Context.Named.empty
end in
let avoid = ref Id.Set.empty in
- let _,_,_,_,sigma = Proof.proof pf 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
@@ -236,7 +236,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
p, sigma
let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
- let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in
+ let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
let univs =
Evd.const_univ_entry ~poly sigma
in
diff --git a/tactics/ppred.ml b/tactics/ppred.ml
new file mode 100644
index 0000000000..dd1bcd4699
--- /dev/null
+++ b/tactics/ppred.ml
@@ -0,0 +1,83 @@
+open Util
+open Pp
+open Locus
+open Genredexpr
+open Pputils
+
+let pr_with_occurrences pr keyword (occs,c) =
+ match occs with
+ | AllOccurrences ->
+ pr c
+ | NoOccurrences ->
+ failwith "pr_with_occurrences: no occurrences"
+ | OnlyOccurrences nl ->
+ hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++
+ hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+ | AllOccurrencesBut nl ->
+ hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++
+ hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+
+exception ComplexRedFlag
+
+let pr_short_red_flag pr r =
+ if not r.rBeta || not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then
+ raise ComplexRedFlag
+ else if List.is_empty r.rConst then
+ if r.rDelta then mt () else raise ComplexRedFlag
+ else (if r.rDelta then str "-" else mt ()) ++
+ hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")
+
+let pr_red_flag pr r =
+ try pr_short_red_flag pr r
+ with ComplexRedFlag ->
+ (if r.rBeta then pr_arg str "beta" else mt ()) ++
+ (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else
+ (if r.rMatch then pr_arg str "match" else mt ()) ++
+ (if r.rFix then pr_arg str "fix" else mt ()) ++
+ (if r.rCofix then pr_arg str "cofix" else mt ())) ++
+ (if r.rZeta then pr_arg str "zeta" else mt ()) ++
+ (if List.is_empty r.rConst then
+ if r.rDelta then pr_arg str "delta"
+ else mt ()
+ else
+ pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
+ hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
+
+let pr_union pr1 pr2 = function
+ | Inl a -> pr1 a
+ | Inr b -> pr2 b
+
+let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
+ | Red false -> keyword "red"
+ | Hnf -> keyword "hnf"
+ | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f)
+ ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+ | Cbv f ->
+ if f.rBeta && f.rMatch && f.rFix && f.rCofix &&
+ f.rZeta && f.rDelta && List.is_empty f.rConst then
+ keyword "compute"
+ else
+ hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f)
+ | Lazy f ->
+ hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f)
+ | Cbn f ->
+ hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f)
+ | Unfold l ->
+ hov 1 (keyword "unfold" ++ spc() ++
+ prlist_with_sep pr_comma (pr_with_occurrences pr_ref keyword) l)
+ | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l)
+ | Pattern l ->
+ hov 1 (keyword "pattern" ++
+ pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l)
+
+ | Red true ->
+ CErrors.user_err Pp.(str "Shouldn't be accessible from user.")
+ | ExtraRedExpr s ->
+ str s
+ | CbvVm o ->
+ keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+ | CbvNative o ->
+ keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+
+let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) =
+ pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma)
diff --git a/tactics/ppred.mli b/tactics/ppred.mli
new file mode 100644
index 0000000000..b3a306a36f
--- /dev/null
+++ b/tactics/ppred.mli
@@ -0,0 +1,19 @@
+open Genredexpr
+
+val pr_with_occurrences :
+ ('a -> Pp.t) -> (string -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t
+
+val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
+val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
+
+val pr_red_expr :
+ ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
+ (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t
+
+val pr_red_expr_env : Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
+ (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
+ ('b -> Pp.t) *
+ (Environ.env -> Evd.evar_map -> 'c -> Pp.t) ->
+ (string -> Pp.t) ->
+ ('a,'b,'c) red_expr_gen -> Pp.t
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
new file mode 100644
index 0000000000..aabfae444e
--- /dev/null
+++ b/tactics/redexpr.ml
@@ -0,0 +1,278 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open Names
+open Constr
+open EConstr
+open Declarations
+open Genredexpr
+open Pattern
+open Reductionops
+open Tacred
+open CClosure
+open RedFlags
+open Libobject
+
+(* call by value normalisation function using the virtual machine *)
+let cbv_vm env sigma c =
+ if Coq_config.bytecode_compiler then
+ let ctyp = Retyping.get_type_of env sigma c in
+ Vnorm.cbv_vm env sigma c ctyp
+ else
+ compute env sigma c
+
+let warn_native_compute_disabled =
+ CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
+ (fun () ->
+ strbrk "native_compute disabled at configure time; falling back to vm_compute.")
+
+let cbv_native env sigma c =
+ if Coq_config.native_compiler then
+ let ctyp = Retyping.get_type_of env sigma c in
+ Nativenorm.native_norm env sigma c ctyp
+ else
+ (warn_native_compute_disabled ();
+ cbv_vm env sigma c)
+
+let whd_cbn flags env sigma t =
+ let (state,_) =
+ (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty))
+ in
+ Reductionops.Stack.zip ~refold:true sigma state
+
+let strong_cbn flags =
+ strong_with_flags whd_cbn flags
+
+let simplIsCbn = ref (false)
+let () = Goptions.(declare_bool_option {
+ optdepr = false;
+ optname =
+ "Plug the simpl tactic to the new cbn mechanism";
+ optkey = ["SimplIsCbn"];
+ optread = (fun () -> !simplIsCbn);
+ optwrite = (fun a -> simplIsCbn:=a);
+})
+
+let set_strategy_one ref l =
+ let k =
+ match ref with
+ | EvalConstRef sp -> ConstKey sp
+ | EvalVarRef id -> VarKey id in
+ Global.set_strategy k l;
+ match k,l with
+ ConstKey sp, Conv_oracle.Opaque ->
+ Csymtable.set_opaque_const sp
+ | ConstKey sp, _ ->
+ let cb = Global.lookup_constant sp in
+ (match cb.const_body with
+ | OpaqueDef _ ->
+ user_err ~hdr:"set_transparent_const"
+ (str "Cannot make" ++ spc () ++
+ Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++
+ spc () ++ str "transparent because it was declared opaque.");
+ | _ -> Csymtable.set_transparent_const sp)
+ | _ -> ()
+
+let cache_strategy (_,str) =
+ List.iter
+ (fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql)
+ str
+
+let subst_strategy (subs,(local,obj)) =
+ local,
+ List.Smart.map
+ (fun (k,ql as entry) ->
+ let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in
+ if ql==ql' then entry else (k,ql'))
+ obj
+
+
+let map_strategy f l =
+ let l' = List.fold_right
+ (fun (lev,ql) str ->
+ let ql' = List.fold_right
+ (fun q ql ->
+ match f q with
+ Some q' -> q' :: ql
+ | None -> ql) ql [] in
+ if List.is_empty ql' then str else (lev,ql')::str) l [] in
+ if List.is_empty l' then None else Some (false,l')
+
+let classify_strategy (local,_ as obj) =
+ if local then Dispose else Substitute obj
+
+let disch_ref ref =
+ match ref with
+ EvalConstRef c -> Some ref
+ | EvalVarRef id -> if Lib.is_in_section (GlobRef.VarRef id) then None else Some ref
+
+let discharge_strategy (_,(local,obj)) =
+ if local then None else
+ map_strategy disch_ref obj
+
+type strategy_obj =
+ bool * (Conv_oracle.level * evaluable_global_reference list) list
+
+let inStrategy : strategy_obj -> obj =
+ declare_object {(default_object "STRATEGY") with
+ cache_function = (fun (_,obj) -> cache_strategy obj);
+ load_function = (fun _ (_,obj) -> cache_strategy obj);
+ subst_function = subst_strategy;
+ discharge_function = discharge_strategy;
+ classify_function = classify_strategy }
+
+
+let set_strategy local str =
+ Lib.add_anonymous_leaf (inStrategy (local,str))
+
+(* Generic reduction: reduction functions used in reduction tactics *)
+
+type red_expr =
+ (constr, evaluable_global_reference, constr_pattern) red_expr_gen
+
+let make_flag_constant = function
+ | EvalVarRef id -> fVAR id
+ | EvalConstRef sp -> fCONST sp
+
+let make_flag env f =
+ let red = no_red in
+ let red = if f.rBeta then red_add red fBETA else red in
+ let red = if f.rMatch then red_add red fMATCH else red in
+ let red = if f.rFix then red_add red fFIX else red in
+ let red = if f.rCofix then red_add red fCOFIX else red in
+ let red = if f.rZeta then red_add red fZETA else red in
+ let red =
+ if f.rDelta then (* All but rConst *)
+ let red = red_add red fDELTA in
+ let red = red_add_transparent red
+ (Conv_oracle.get_transp_state (Environ.oracle env)) in
+ List.fold_right
+ (fun v red -> red_sub red (make_flag_constant v))
+ f.rConst red
+ else (* Only rConst *)
+ let red = red_add_transparent (red_add red fDELTA) TransparentState.empty in
+ List.fold_right
+ (fun v red -> red_add red (make_flag_constant v))
+ f.rConst red
+ in red
+
+(* table of custom reductino fonctions, not synchronized,
+ filled via ML calls to [declare_reduction] *)
+let reduction_tab = ref String.Map.empty
+
+(* table of custom reduction expressions, synchronized,
+ filled by command Declare Reduction *)
+let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction"
+
+let declare_reduction s f =
+ if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
+ then user_err ~hdr:"Redexpr.declare_reduction"
+ (str "There is already a reduction expression of name " ++ str s)
+ else reduction_tab := String.Map.add s f !reduction_tab
+
+let check_custom = function
+ | ExtraRedExpr s ->
+ if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab)
+ then user_err ~hdr:"Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s)
+ |_ -> ()
+
+let decl_red_expr s e =
+ if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
+ then user_err ~hdr:"Redexpr.decl_red_expr"
+ (str "There is already a reduction expression of name " ++ str s)
+ else begin
+ check_custom e;
+ red_expr_tab := String.Map.add s e !red_expr_tab
+ end
+
+let out_arg = function
+ | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
+ | Locus.ArgArg x -> x
+
+let out_with_occurrences (occs,c) =
+ (Locusops.occurrences_map (List.map out_arg) occs, c)
+
+let e_red f env evm c = evm, f env evm c
+
+let head_style = false (* Turn to true to have a semantics where simpl
+ only reduce at the head when an evaluable reference is given, e.g.
+ 2+n would just reduce to S(1+n) instead of S(S(n)) *)
+
+let contextualize f g = function
+ | Some (occs,c) ->
+ let l = Locusops.occurrences_map (List.map out_arg) occs in
+ let b,c,h = match c with
+ | Inl r -> true,PRef (global_of_evaluable_reference r),f
+ | Inr c -> false,c,f in
+ e_red (contextually b (l,c) (fun _ -> h))
+ | None -> e_red g
+
+let warn_simpl_unfolding_modifiers =
+ CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:"tactics"
+ (fun () ->
+ Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.")
+
+let reduction_of_red_expr env =
+ let make_flag = make_flag env in
+ let rec reduction_of_red_expr = function
+ | Red internal ->
+ if internal then (e_red try_red_product,DEFAULTcast)
+ 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 () =
+ 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)
+ | Cbn f ->
+ (e_red (strong_cbn (make_flag f)), DEFAULTcast)
+ | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast)
+ | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast)
+ | Fold cl -> (e_red (fold_commands cl),DEFAULTcast)
+ | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)
+ | ExtraRedExpr s ->
+ (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast)
+ with Not_found ->
+ (try reduction_of_red_expr (String.Map.find s !red_expr_tab)
+ with Not_found ->
+ user_err ~hdr:"Redexpr.reduction_of_red_expr"
+ (str "unknown user-defined reduction \"" ++ str s ++ str "\"")))
+ | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
+ | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
+ in
+ reduction_of_red_expr
+
+let subst_mps subst c =
+ EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
+
+let subst_red_expr subs =
+ Redops.map_red_expr_gen
+ (subst_mps subs)
+ (Mod_subst.subst_evaluable_reference subs)
+ (Patternops.subst_pattern subs)
+
+let inReduction : bool * string * red_expr -> obj =
+ declare_object
+ {(default_object "REDUCTION") with
+ cache_function = (fun (_,(_,s,e)) -> decl_red_expr s e);
+ load_function = (fun _ (_,(_,s,e)) -> decl_red_expr s e);
+ subst_function =
+ (fun (subs,(b,s,e)) -> b,s,subst_red_expr subs e);
+ classify_function =
+ (fun ((b,_,_) as obj) -> if b then Dispose else Substitute obj) }
+
+let declare_red_expr locality s expr =
+ Lib.add_anonymous_leaf (inReduction (locality,s,expr))
diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli
new file mode 100644
index 0000000000..1f65862701
--- /dev/null
+++ b/tactics/redexpr.mli
@@ -0,0 +1,48 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** Interpretation layer of redexprs such as hnf, cbv, etc. *)
+
+open Names
+open Constr
+open EConstr
+open Pattern
+open Genredexpr
+open Reductionops
+open Locus
+
+type red_expr =
+ (constr, evaluable_global_reference, constr_pattern) red_expr_gen
+
+val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
+
+val reduction_of_red_expr :
+ Environ.env -> red_expr -> e_reduction_function * cast_kind
+
+(** [true] if we should use the vm to verify the reduction *)
+
+(** Adding a custom reduction (function to be use at the ML level)
+ NB: the effect is permanent. *)
+val declare_reduction : string -> reduction_function -> unit
+
+(** Adding a custom reduction (function to be called a vernac command).
+ The boolean flag is the locality. *)
+val declare_red_expr : bool -> string -> red_expr -> unit
+
+(** Opaque and Transparent commands. *)
+
+(** Sets the expansion strategy of a constant. When the boolean is
+ true, the effect is non-synchronous (i.e. it does not survive
+ section and module closure). *)
+val set_strategy :
+ bool -> (Conv_oracle.level * evaluable_global_reference list) list -> unit
+
+(** call by value normalisation function using the virtual machine *)
+val cbv_vm : reduction_function
diff --git a/tactics/redops.ml b/tactics/redops.ml
new file mode 100644
index 0000000000..6f83ea9a34
--- /dev/null
+++ b/tactics/redops.ml
@@ -0,0 +1,64 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Genredexpr
+
+let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *)
+
+let make_red_flag l =
+ let rec add_flag red = function
+ | [] -> red
+ | FBeta :: lf -> add_flag { red with rBeta = true } lf
+ | FMatch :: lf -> add_flag { red with rMatch = true } lf
+ | FFix :: lf -> add_flag { red with rFix = true } lf
+ | FCofix :: lf -> add_flag { red with rCofix = true } lf
+ | FZeta :: lf -> add_flag { red with rZeta = true } lf
+ | FConst l :: lf ->
+ if red.rDelta then
+ CErrors.user_err Pp.(str
+ "Cannot set both constants to unfold and constants not to unfold");
+ add_flag { red with rConst = union_consts red.rConst l } lf
+ | FDeltaBut l :: lf ->
+ if red.rConst <> [] && not red.rDelta then
+ CErrors.user_err Pp.(str
+ "Cannot set both constants to unfold and constants not to unfold");
+ add_flag
+ { red with rConst = union_consts red.rConst l; rDelta = true }
+ lf
+ in
+ add_flag
+ {rBeta = false; rMatch = false; rFix = false; rCofix = false;
+ rZeta = false; rDelta = false; rConst = []}
+ l
+
+
+let all_flags =
+ {rBeta = true; rMatch = true; rFix = true; rCofix = true;
+ rZeta = true; rDelta = true; rConst = []}
+
+(** Mapping [red_expr_gen] *)
+
+let map_flags f flags =
+ { flags with rConst = List.map f flags.rConst }
+
+let map_occs f (occ,e) = (occ,f e)
+
+let map_red_expr_gen f g h = function
+ | Fold l -> Fold (List.map f l)
+ | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l)
+ | Simpl (flags,occs_o) ->
+ Simpl (map_flags g flags, Option.map (map_occs (Util.map_union g h)) occs_o)
+ | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l)
+ | Cbv flags -> Cbv (map_flags g flags)
+ | Lazy flags -> Lazy (map_flags g flags)
+ | CbvVm occs_o -> CbvVm (Option.map (map_occs (Util.map_union g h)) occs_o)
+ | CbvNative occs_o -> CbvNative (Option.map (map_occs (Util.map_union g h)) occs_o)
+ | Cbn flags -> Cbn (map_flags g flags)
+ | ExtraRedExpr _ | Red _ | Hnf as x -> x
diff --git a/tactics/redops.mli b/tactics/redops.mli
new file mode 100644
index 0000000000..7254f29b25
--- /dev/null
+++ b/tactics/redops.mli
@@ -0,0 +1,20 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Genredexpr
+
+val make_red_flag : 'a red_atom list -> 'a glob_red_flag
+
+val all_flags : 'a glob_red_flag
+
+(** Mapping [red_expr_gen] *)
+
+val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
+ ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 224cd68cf9..bfbce8f6eb 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -572,7 +572,7 @@ module New = struct
with Failure _ -> CErrors.user_err Pp.(str "Not enough hypotheses in the goal.")
let nthHypId m gl =
- (** We only use [id] *)
+ (* We only use [id] *)
nthDecl m gl |> NamedDecl.get_id
let nthHyp m gl =
mkVar (nthHypId m gl)
@@ -688,12 +688,12 @@ module New = struct
end) end
let elimination_sort_of_goal gl =
- (** Retyping will expand evars anyway. *)
+ (* Retyping will expand evars anyway. *)
let c = Proofview.Goal.concl gl in
pf_apply Retyping.get_sort_family_of gl c
let elimination_sort_of_hyp id gl =
- (** Retyping will expand evars anyway. *)
+ (* Retyping will expand evars anyway. *)
let c = pf_get_hyp_typ id gl in
pf_apply Retyping.get_sort_family_of gl c
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 2947e44f7a..201b7801c3 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -191,6 +191,7 @@ module New : sig
val tclTHENS3PARTS : unit tactic -> unit tactic array -> 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
+
(** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls]
and [tac2] to the first resulting subgoal *)
val tclTHENFIRST : unit tactic -> unit tactic -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b3ea13cf4f..1043c50f00 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -183,7 +183,7 @@ let convert_gen pb x y =
| Some sigma -> Proofview.Unsafe.tclEVARS sigma
| None -> Tacticals.New.tclFAIL 0 (str "Not convertible")
| exception _ ->
- (** FIXME: Sometimes an anomaly is raised from conversion *)
+ (* FIXME: Sometimes an anomaly is raised from conversion *)
Tacticals.New.tclFAIL 0 (str "Not convertible")
end
@@ -241,7 +241,7 @@ let clear_gen fail = function
| ids ->
Proofview.Goal.enter begin fun gl ->
let ids = List.fold_right Id.Set.add ids Id.Set.empty in
- (** clear_hyps_in_evi does not require nf terms *)
+ (* clear_hyps_in_evi does not require nf terms *)
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
@@ -307,7 +307,7 @@ let rename_hyp repl =
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
- (** Check that we do not mess variables *)
+ (* Check that we do not mess variables *)
let fold accu decl = Id.Set.add (NamedDecl.get_id decl) accu in
let vars = List.fold_left fold Id.Set.empty hyps in
let () =
@@ -322,7 +322,7 @@ let rename_hyp repl =
CErrors.user_err (Id.print elt ++ str " is already used")
with Not_found -> ()
in
- (** All is well *)
+ (* All is well *)
let make_subst (src, dst) = (src, mkVar dst) in
let subst = List.map make_subst repl in
let subst c = Vars.replace_vars subst c in
@@ -889,11 +889,7 @@ let reduce redexp cl =
let trace env sigma =
let open Printer in
let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in
- Pp.(hov 2 (Pputils.pr_red_expr_env env sigma pr str redexp))
- in
- let trace () =
- let sigma, env = Pfedit.get_current_context () in
- trace env sigma
+ Pp.(hov 2 (Ppred.pr_red_expr_env env sigma pr str redexp))
in
Proofview.Trace.name_tactic trace begin
Proofview.Goal.enter begin fun gl ->
@@ -1063,9 +1059,16 @@ let intros_replacing ids =
(* The standard for implementing Automatic Introduction *)
let auto_intros_tac ids =
- Tacticals.New.tclMAP (function
- | Name id -> intro_mustbe_force id
- | Anonymous -> intro) (List.rev ids)
+ let fold used = function
+ | Name id -> Id.Set.add id used
+ | Anonymous -> used
+ in
+ let avoid = NamingAvoid (List.fold_left fold Id.Set.empty ids) in
+ let naming = function
+ | Name id -> NamingMustBe CAst.(make id)
+ | Anonymous -> avoid
+ in
+ Tacticals.New.tclMAP (fun name -> intro_gen (naming name) MoveLast true false) (List.rev ids)
(* User-level introduction tactics *)
@@ -1235,7 +1238,7 @@ let cut c =
let concl = Proofview.Goal.concl gl in
let is_sort =
try
- (** Backward compat: ensure that [c] is well-typed. *)
+ (* Backward compat: ensure that [c] is well-typed. *)
let typ = Typing.unsafe_type_of env sigma c in
let typ = whd_all env sigma typ in
match EConstr.kind sigma typ with
@@ -1245,7 +1248,7 @@ let cut c =
in
if is_sort then
let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in
- (** Backward compat: normalize [c]. *)
+ (* Backward compat: normalize [c]. *)
let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
Refine.refine ~typecheck:false begin fun h ->
let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
@@ -1498,8 +1501,8 @@ let simplest_elim c = default_elim false None (c,NoBindings)
*)
let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
- (** The evarmap of elimclause is assumed to be an extension of hypclause, so
- we do not need to merge the universes coming from hypclause. *)
+ (* The evarmap of elimclause is assumed to be an extension of hypclause, so
+ we do not need to merge the universes coming from hypclause. *)
try clenv_fchain ~with_univs:false ~flags mv elimclause hypclause
with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
(* Set the hypothesis name in the message *)
@@ -1909,7 +1912,7 @@ let exact_no_check c =
let exact_check c =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
- (** We do not need to normalize the goal because we just check convertibility *)
+ (* We do not need to normalize the goal because we just check convertibility *)
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let sigma, ct = Typing.type_of env sigma c in
@@ -2021,7 +2024,7 @@ let clear_body ids =
let check =
try
let check (env, sigma, seen) decl =
- (** Do no recheck hypotheses that do not depend *)
+ (* Do no recheck hypotheses that do not depend *)
let sigma =
if not seen then sigma
else if List.exists (fun id -> occur_var_in_decl env sigma id decl) ids then
@@ -2848,7 +2851,7 @@ let generalize_dep ?(with_let=false) c =
in
let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous)
(cl',project gl) in
- (** Check that the generalization is indeed well-typed *)
+ (* Check that the generalization is indeed well-typed *)
let (evd, _) = Typing.type_of env evd cl'' in
let args = Context.Named.to_instance mkVar to_quantify_rev in
tclTHENLIST
@@ -3021,7 +3024,7 @@ let specialize (c,lbind) ipat =
let unfold_body x =
let open Context.Named.Declaration in
Proofview.Goal.enter begin fun gl ->
- (** We normalize the given hypothesis immediately. *)
+ (* We normalize the given hypothesis immediately. *)
let env = Proofview.Goal.env gl in
let xval = match Environ.lookup_named x env with
| LocalAssum _ -> user_err ~hdr:"unfold_body"
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 5afec74fae..1861c5b99b 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -6,6 +6,10 @@ Hipattern
Ind_tables
Eqschemes
Elimschemes
+Genredexpr
+Redops
+Redexpr
+Ppred
Tactics
Abstract
Elim
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 03d2a17eee..e273891500 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -281,7 +281,7 @@ struct
open TDnet
let pat_of_constr c : term_pattern =
- (** To each evar we associate a unique identifier. *)
+ (* To each evar we associate a unique identifier. *)
let metas = ref Evar.Map.empty in
let rec pat_of_constr c = match Constr.kind c with
| Rel _ -> Term DRel
@@ -378,7 +378,7 @@ struct
let c_id = Opt.reduce (Ident.constr_of id) in
let c_id = EConstr.of_constr c_id in
let (ctx,wc) =
- try Termops.align_prod_letin Evd.empty whole_c c_id (** FIXME *)
+ try Termops.align_prod_letin Evd.empty whole_c c_id (* FIXME *)
with Invalid_argument _ -> [],c_id in
let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
try
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 03:09:31 +0000