aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml6
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/class_tactics.ml20
-rw-r--r--tactics/contradiction.ml21
-rw-r--r--tactics/eauto.ml10
-rw-r--r--tactics/elimschemes.ml12
-rw-r--r--tactics/elimschemes.mli2
-rw-r--r--tactics/eqschemes.ml2
-rw-r--r--tactics/equality.ml17
-rw-r--r--tactics/hints.ml6
-rw-r--r--tactics/hipattern.ml8
-rw-r--r--tactics/inv.ml4
-rw-r--r--tactics/leminv.ml6
-rw-r--r--tactics/taccoerce.ml344
-rw-r--r--tactics/taccoerce.mli96
-rw-r--r--tactics/tactic_matching.ml2
-rw-r--r--tactics/tacticals.ml8
-rw-r--r--tactics/tactics.ml90
-rw-r--r--tactics/tactics.mllib1
19 files changed, 134 insertions, 523 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6c1f38d48b..962af4b5c5 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -10,7 +10,7 @@
*)
open Pp
open Util
-open Errors
+open CErrors
open Names
open Vars
open Termops
@@ -222,7 +222,7 @@ let tclLOG (dbg,depth,trace) pp tac =
Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
out
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
iraise reraise
end
@@ -234,7 +234,7 @@ let tclLOG (dbg,depth,trace) pp tac =
trace := (depth, Some pp) :: !trace;
out
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
trace := (depth, None) :: !trace;
iraise reraise
end
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 9ae0ab90b2..4750056480 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -13,7 +13,7 @@ open Tacticals
open Tactics
open Term
open Termops
-open Errors
+open CErrors
open Util
open Mod_subst
open Locus
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 316a79482f..8d6c085e63 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -13,7 +13,7 @@
*)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -382,7 +382,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
if cl.cl_strict then
Evd.evars_of_term concl
else Evar.Set.empty
- with e when Errors.noncritical e -> Evar.Set.empty
+ with e when CErrors.noncritical e -> Evar.Set.empty
in
let hintl =
List.map_append
@@ -485,7 +485,7 @@ let is_unique env concl =
try
let (cl,u), args = dest_class_app env concl in
cl.cl_unique
- with e when Errors.noncritical e -> false
+ with e when CErrors.noncritical e -> false
(** Sort the undefined variables from the least-dependent to most dependent. *)
let top_sort evm undefs =
@@ -533,7 +533,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
| Ind (i,_) -> is_class (IndRef i)
| _ ->
let env' = Environ.push_rel_context ctx env in
- let ty' = whd_betadeltaiota env' ar in
+ let ty' = whd_all env' ar in
if not (Term.eq_constr ty' ar) then iscl env' ty'
else false
in
@@ -1288,7 +1288,7 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
~depth dbs =
let dbs = List.map_filter
(fun db -> try Some (searchtable_map db)
- with e when Errors.noncritical e -> None)
+ with e when CErrors.noncritical e -> None)
dbs
in
let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
@@ -1444,7 +1444,7 @@ let resolve_typeclass_evars debug depth unique env evd filter split fail =
let evd =
try Evarconv.consider_remaining_unif_problems
~ts:(Typeclasses.classes_transparent_state ()) env evd
- with e when Errors.noncritical e -> evd
+ with e when CErrors.noncritical e -> evd
in
resolve_all_evars debug depth unique env
(initial_select_evars filter) evd split fail
@@ -1500,9 +1500,11 @@ let head_of_constr h c =
let c = head_of_constr c in
letin_tac None (Name h) c None Locusops.allHyps
-let not_evar c = match kind_of_term c with
-| Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
-| _ -> Proofview.tclUNIT ()
+let not_evar c =
+ Proofview.tclEVARMAP >>= fun sigma ->
+ match Evarutil.kind_of_term_upto sigma c with
+ | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
+ | _ -> Proofview.tclUNIT ()
let is_ground c gl =
if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 26166bd834..445a104d60 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -42,6 +42,8 @@ let absurd c = absurd c
(* Contradiction *)
+let use_negated_unit_or_eq_type () = Flags.version_strictly_greater Flags.V8_5
+
(** [f] does not assume its argument to be [nf_evar]-ed. *)
let filter_hyp f tac =
let rec seek = function
@@ -62,11 +64,26 @@ let contradiction_context =
| d :: rest ->
let id = get_id d in
let typ = nf_evar sigma (get_type d) in
- let typ = whd_betadeltaiota env sigma typ in
+ let typ = whd_all env sigma typ in
if is_empty_type typ then
simplest_elim (mkVar id)
else match kind_of_term typ with
| Prod (na,t,u) when is_empty_type u ->
+ let is_unit_or_eq =
+ if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type t
+ else None in
+ Tacticals.New.tclORELSE
+ (match is_unit_or_eq with
+ | Some _ ->
+ let hd,args = decompose_app t in
+ let (ind,_ as indu) = destInd hd in
+ let nparams = Inductiveops.inductive_nparams_env env ind in
+ let params = Util.List.firstn nparams args in
+ let p = applist ((mkConstructUi (indu,1)), params) in
+ (* Checking on the fly that it type-checks *)
+ simplest_elim (mkApp (mkVar id,[|p|]))
+ | None ->
+ Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type."))
(Proofview.tclORELSE
(Proofview.Goal.enter { enter = begin fun gl ->
let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
@@ -84,7 +101,7 @@ let contradiction_context =
end }
let is_negation_of env sigma typ t =
- match kind_of_term (whd_betadeltaiota env sigma t) with
+ match kind_of_term (whd_all env sigma t) with
| Prod (na,t,u) ->
let u = nf_evar sigma u in
is_empty_type u && is_conv_leq env sigma typ t
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 93c201bf18..ba9a2d95c8 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -29,9 +29,9 @@ open Proofview.Notations
let eauto_unif_flags = auto_flags_of_state full_transparent_state
let e_give_exact ?(flags=eauto_unif_flags) c =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let t1 = Tacmach.New.pf_unsafe_type_of gl c in
- let t2 = Tacmach.New.pf_concl gl in
+ let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
if occur_existential t1 || occur_existential t2 then
Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
else exact_check c
@@ -231,8 +231,8 @@ module SearchProblem = struct
(* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
(lgls, cost, pptac) :: aux tacl
- with e when Errors.noncritical e ->
- let e = Errors.push e in
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
Refiner.catch_failerror e; aux tacl
in aux l
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index de28189023..93073fdc7e 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -52,19 +52,21 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
let u = Univ.UContext.instance ctx in
let ctxset = Univ.ContextSet.of_context ctx in
let ectx = Evd.evar_universe_context_of ctxset in
- let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
+ let sigma = Evd.merge_universe_context sigma ectx in
+ let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in
(c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants
let build_induction_scheme_in_type dep sort ind =
let env = Global.env () in
+ let sigma = Evd.from_env env in
let ctx =
let mib,mip = Inductive.lookup_mind_specif env ind in
Declareops.inductive_context mib
in
let u = Univ.UContext.instance ctx in
let ctxset = Univ.ContextSet.of_context ctx in
- let ectx = Evd.evar_universe_context_of ctxset in
- let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
+ let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context_of ctxset) in
+ let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in
c, Evd.evar_universe_context sigma
let rect_scheme_kind_from_type =
@@ -95,6 +97,10 @@ let rec_scheme_kind_from_prop =
declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop"
(optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet)
+let rec_scheme_kind_from_type =
+ declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type"
+ (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet)
+
let rec_dep_scheme_kind_from_type =
declare_individual_scheme_object "_rec" ~aux:"_rec_from_type"
(optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet)
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index c36797059e..77f927f2df 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -13,9 +13,11 @@ open Ind_tables
val rect_scheme_kind_from_prop : individual scheme_kind
val ind_scheme_kind_from_prop : individual scheme_kind
val rec_scheme_kind_from_prop : individual scheme_kind
+val rect_scheme_kind_from_type : individual scheme_kind
val rect_dep_scheme_kind_from_type : individual scheme_kind
val ind_scheme_kind_from_type : individual scheme_kind
val ind_dep_scheme_kind_from_type : individual scheme_kind
+val rec_scheme_kind_from_type : individual scheme_kind
val rec_dep_scheme_kind_from_type : individual scheme_kind
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index a03489c805..1a45217a4a 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -44,7 +44,7 @@
natural expectation of the user.
*)
-open Errors
+open CErrors
open Util
open Names
open Term
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 35be1fcb6e..3e5b7b65ff 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -400,7 +400,8 @@ let type_of_clause cls gl = match cls with
let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
- let isatomic = isProd (whd_zeta hdcncl) in
+ let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+ let isatomic = isProd (whd_zeta evd hdcncl) in
let dep_fun = if isatomic then dependent else dependent_no_evar in
let type_of_cls = type_of_clause cls gl in
let dep = dep_proof_ok && dep_fun c type_of_cls in
@@ -628,7 +629,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
in
match evd with
| None ->
- tclFAIL 0 (str"Terms do not have convertible types.")
+ tclFAIL 0 (str"Terms do not have convertible types")
| Some evd ->
let e = build_coq_eq () in
let sym = build_coq_eq_sym () in
@@ -720,8 +721,8 @@ let find_positions env sigma t1 t2 =
then [(List.rev posn,t1,t2)] else []
in
let rec findrec sorts posn t1 t2 =
- let hd1,args1 = whd_betadeltaiota_stack env sigma t1 in
- let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in
+ let hd1,args1 = whd_all_stack env sigma t1 in
+ let hd2,args2 = whd_all_stack env sigma t2 in
match (kind_of_term hd1, kind_of_term hd2) with
| Construct (sp1,_), Construct (sp2,_)
when Int.equal (List.length args1) (constructor_nallargs_env env sp1)
@@ -859,7 +860,7 @@ let descend_then env sigma head dirn =
List.map build_branch
(List.interval 1 (Array.length mip.mind_consnames)) in
let ci = make_case_info env ind RegularStyle in
- mkCase (ci, p, head, Array.of_list brl)))
+ Inductiveops.make_case_or_project env indf ci p head (Array.of_list brl)))
(* Now we need to construct the discriminator, given a discriminable
position. This boils down to:
@@ -1283,7 +1284,7 @@ let build_injector env sigma dflt c cpath =
(*
let try_delta_expand env sigma t =
- let whdt = whd_betadeltaiota env sigma t in
+ let whdt = whd_all env sigma t in
let rec hd_rec c =
match kind_of_term c with
| Construct _ -> whdt
@@ -1690,7 +1691,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
&& List.exists (fun y -> occur_var_in_decl env y dcl) deps
then
let id_dest = if !regular_subst_tactic then dest else MoveLast in
- (dest,(if is_local_assum dcl then deps else id::deps), (id_dest,id)::allhyps)
+ (dest,id::deps,(id_dest,id)::allhyps)
else
(MoveBefore id,deps,allhyps))
hyps
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2c2b76412f..8f3eb5eb51 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -8,7 +8,7 @@
open Pp
open Util
-open Errors
+open CErrors
open Names
open Vars
open Term
@@ -1273,7 +1273,7 @@ let pr_hint h = match h.obj with
try
let (_, env) = Pfedit.get_current_goal_context () in
env
- with e when Errors.noncritical e -> Global.env ()
+ with e when CErrors.noncritical e -> Global.env ()
in
(str "(*external*) " ++ Pptactic.pr_glb_generic env tac)
@@ -1334,7 +1334,7 @@ let pr_applicable_hint () =
let pts = get_pftreestate () in
let glss = Proof.V82.subgoals pts in
match glss.Evd.it with
- | [] -> Errors.error "No focused goal."
+ | [] -> CErrors.error "No focused goal."
| g::_ ->
pr_hint_term (Goal.V82.concl glss.Evd.sigma g)
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 4c2c84d23b..7b52a9cee6 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -409,7 +409,7 @@ let rec first_match matcher = function
let match_eq eqn (ref, hetero) =
let ref =
try Lazy.force ref
- with e when Errors.noncritical e -> raise PatternMatchingFailure
+ with e when CErrors.noncritical e -> raise PatternMatchingFailure
in
match kind_of_term eqn with
| App (c, [|t; x; y|]) ->
@@ -464,7 +464,7 @@ let match_eq_nf gls eqn (ref, hetero) =
match Id.Map.bindings (pf_matches gls pat eqn) with
| [(m1,t);(m2,x);(m3,y)] ->
assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
- (t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y)
+ (t,pf_whd_all gls x,pf_whd_all gls y)
| _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms")
let dest_nf_eq gls eqn =
@@ -509,7 +509,7 @@ let coq_eqdec ~sum ~rev =
let eqn = mkGAppRef coq_eq_ref (List.map mkGPatVar ["X1"; "X2"; "X3"]) in
let args = [eqn; mkGAppRef coq_not_ref [eqn]] in
let args = if rev then List.rev args else args in
- mkPattern (mkGAppRef sum [eqn; mkGAppRef coq_not_ref [eqn]])
+ mkPattern (mkGAppRef sum args)
)
(** { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } *)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 852c2ee7cb..bda16b01c0 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -440,7 +440,7 @@ let raw_inversion inv_kind id status names =
try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
with UserError _ ->
let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
- Errors.errorlabstrm "" msg
+ CErrors.errorlabstrm "" msg
in
let IndType (indf,realargs) = find_rectype env sigma t in
let evdref = ref sigma in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 70782ec648..642bf520b1 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -114,7 +114,7 @@ let max_prefix_sign lid sign =
| id::l -> snd (max_rec (id, sign_prefix id sign) l)
*)
let rec add_prods_sign env sigma t =
- match kind_of_term (whd_betadeltaiota env sigma t) with
+ match kind_of_term (whd_all env sigma t) with
| Prod (na,c1,b) ->
let id = id_of_name_using_hdchar env t na in
let b'= subst1 (mkVar id) b in
@@ -167,7 +167,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in
(pty,goal)
in
- let npty = nf_betadeltaiota env sigma pty in
+ let npty = nf_all env sigma pty in
let extenv = push_named (LocalAssum (p,npty)) env in
extenv, goal
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
deleted file mode 100644
index 0110510d35..0000000000
--- a/tactics/taccoerce.ml
+++ /dev/null
@@ -1,344 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Util
-open Names
-open Term
-open Pattern
-open Misctypes
-open Genarg
-open Stdarg
-open Constrarg
-open Geninterp
-
-exception CannotCoerceTo of string
-
-let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
- let wit = Genarg.create_arg "constr_context" in
- let () = register_val0 wit None in
- wit
-
-(* includes idents known to be bound and references *)
-let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
- let wit = Genarg.create_arg "constr_under_binders" in
- let () = register_val0 wit None in
- wit
-
-(** All the types considered here are base types *)
-let val_tag wit = match val_tag wit with
-| Val.Base t -> t
-| _ -> assert false
-
-let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
- let Val.Dyn (t, _) = v in
- match Val.eq t (val_tag wit) with
- | None -> false
- | Some Refl -> true
-
-let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
- let Val.Dyn (t', x) = v in
- match Val.eq t t' with
- | None -> None
- | Some Refl -> Some x
-
-let in_gen wit v = Val.Dyn (val_tag wit, v)
-let out_gen wit v = match prj (val_tag wit) v with None -> assert false | Some x -> x
-
-module Value =
-struct
-
-type t = Val.t
-
-let normalize v = v
-
-let of_constr c = in_gen (topwit wit_constr) c
-
-let to_constr v =
- let v = normalize v in
- if has_type v (topwit wit_constr) then
- let c = out_gen (topwit wit_constr) v in
- Some c
- else if has_type v (topwit wit_constr_under_binders) then
- let vars, c = out_gen (topwit wit_constr_under_binders) v in
- match vars with [] -> Some c | _ -> None
- else None
-
-let of_uconstr c = in_gen (topwit wit_uconstr) c
-
-let to_uconstr v =
- let v = normalize v in
- if has_type v (topwit wit_uconstr) then
- Some (out_gen (topwit wit_uconstr) v)
- else None
-
-let of_int i = in_gen (topwit wit_int) i
-
-let to_int v =
- let v = normalize v in
- if has_type v (topwit wit_int) then
- Some (out_gen (topwit wit_int) v)
- else None
-
-let to_list v = prj Val.typ_list v
-
-let to_option v = prj Val.typ_opt v
-
-let to_pair v = prj Val.typ_pair v
-
-end
-
-let is_variable env id =
- Id.List.mem id (Termops.ids_of_named_context (Environ.named_context env))
-
-(* Transforms an id into a constr if possible, or fails with Not_found *)
-let constr_of_id env id =
- Term.mkVar (let _ = Environ.lookup_named id env in id)
-
-(* Gives the constr corresponding to a Constr_context tactic_arg *)
-let coerce_to_constr_context v =
- let v = Value.normalize v in
- if has_type v (topwit wit_constr_context) then
- out_gen (topwit wit_constr_context) v
- else raise (CannotCoerceTo "a term context")
-
-(* Interprets an identifier which must be fresh *)
-let coerce_var_to_ident fresh env v =
- let v = Value.normalize v in
- let fail () = raise (CannotCoerceTo "a fresh identifier") in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) -> id
- | _ -> fail ()
- else if has_type v (topwit wit_var) then
- out_gen (topwit wit_var) v
- else match Value.to_constr v with
- | None -> fail ()
- | Some c ->
- (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *)
- if isVar c && not (fresh && is_variable env (destVar c)) then
- destVar c
- else fail ()
-
-
-(* Interprets, if possible, a constr to an identifier which may not
- be fresh but suitable to be given to the fresh tactic. Works for
- vars, constants, inductive, constructors and sorts. *)
-let coerce_to_ident_not_fresh g env v =
-let id_of_name = function
- | Names.Anonymous -> Id.of_string "x"
- | Names.Name x -> x in
- let v = Value.normalize v in
- let fail () = raise (CannotCoerceTo "an identifier") in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) -> id
- | _ -> fail ()
- else if has_type v (topwit wit_var) then
- out_gen (topwit wit_var) v
- else
- match Value.to_constr v with
- | None -> fail ()
- | Some c ->
- match Constr.kind c with
- | Var id -> id
- | Meta m -> id_of_name (Evd.meta_name g m)
- | Evar (kn,_) ->
- begin match Evd.evar_ident kn g with
- | None -> fail ()
- | Some id -> id
- end
- | Const (cst,_) -> Label.to_id (Constant.label cst)
- | Construct (cstr,_) ->
- let ref = Globnames.ConstructRef cstr in
- let basename = Nametab.basename_of_global ref in
- basename
- | Ind (ind,_) ->
- let ref = Globnames.IndRef ind in
- let basename = Nametab.basename_of_global ref in
- basename
- | Sort s ->
- begin
- match s with
- | Prop _ -> Label.to_id (Label.make "Prop")
- | Type _ -> Label.to_id (Label.make "Type")
- end
- | _ -> fail()
-
-
-let coerce_to_intro_pattern env v =
- let v = Value.normalize v in
- if has_type v (topwit wit_intro_pattern) then
- snd (out_gen (topwit wit_intro_pattern) v)
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
- IntroNaming (IntroIdentifier id)
- else match Value.to_constr v with
- | Some c when isVar c ->
- (* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
- (* but also in "destruct H as (H,H')" *)
- IntroNaming (IntroIdentifier (destVar c))
- | _ -> raise (CannotCoerceTo "an introduction pattern")
-
-let coerce_to_intro_pattern_naming env v =
- match coerce_to_intro_pattern env v with
- | IntroNaming pat -> pat
- | _ -> raise (CannotCoerceTo "a naming introduction pattern")
-
-let coerce_to_hint_base v =
- let v = Value.normalize v in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) -> Id.to_string id
- | _ -> raise (CannotCoerceTo "a hint base name")
- else raise (CannotCoerceTo "a hint base name")
-
-let coerce_to_int v =
- let v = Value.normalize v in
- if has_type v (topwit wit_int) then
- out_gen (topwit wit_int) v
- else raise (CannotCoerceTo "an integer")
-
-let coerce_to_constr env v =
- let v = Value.normalize v in
- let fail () = raise (CannotCoerceTo "a term") in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) ->
- (try ([], constr_of_id env id) with Not_found -> fail ())
- | _ -> fail ()
- else if has_type v (topwit wit_constr) then
- let c = out_gen (topwit wit_constr) v in
- ([], c)
- else if has_type v (topwit wit_constr_under_binders) then
- out_gen (topwit wit_constr_under_binders) v
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
- (try [], constr_of_id env id with Not_found -> fail ())
- else fail ()
-
-let coerce_to_uconstr env v =
- let v = Value.normalize v in
- if has_type v (topwit wit_uconstr) then
- out_gen (topwit wit_uconstr) v
- else
- raise (CannotCoerceTo "an untyped term")
-
-let coerce_to_closed_constr env v =
- let ids,c = coerce_to_constr env v in
- let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in
- c
-
-let coerce_to_evaluable_ref env v =
- let fail () = raise (CannotCoerceTo "an evaluable reference") in
- let v = Value.normalize v in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id
- | _ -> fail ()
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
- if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
- else fail ()
- else if has_type v (topwit wit_ref) then
- let open Globnames in
- let r = out_gen (topwit wit_ref) v in
- match r with
- | VarRef var -> EvalVarRef var
- | ConstRef c -> EvalConstRef c
- | IndRef _ | ConstructRef _ -> fail ()
- else
- let ev = match Value.to_constr v with
- | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c))
- | Some c when isVar c -> EvalVarRef (destVar c)
- | _ -> fail ()
- in
- if Tacred.is_evaluable env ev then ev else fail ()
-
-let coerce_to_constr_list env v =
- let v = Value.to_list v in
- match v with
- | Some l ->
- let map v = coerce_to_closed_constr env v in
- List.map map l
- | None -> raise (CannotCoerceTo "a term list")
-
-let coerce_to_intro_pattern_list loc env v =
- match Value.to_list v with
- | None -> raise (CannotCoerceTo "an intro pattern list")
- | Some l ->
- let map v = (loc, coerce_to_intro_pattern env v) in
- List.map map l
-
-let coerce_to_hyp env v =
- let fail () = raise (CannotCoerceTo "a variable") in
- let v = Value.normalize v in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id
- | _ -> fail ()
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
- if is_variable env id then id else fail ()
- else match Value.to_constr v with
- | Some c when isVar c -> destVar c
- | _ -> fail ()
-
-let coerce_to_hyp_list env v =
- let v = Value.to_list v in
- match v with
- | Some l ->
- let map n = coerce_to_hyp env n in
- List.map map l
- | None -> raise (CannotCoerceTo "a variable list")
-
-(* Interprets a qualified name *)
-let coerce_to_reference env v =
- let v = Value.normalize v in
- match Value.to_constr v with
- | Some c ->
- begin
- try Globnames.global_of_constr c
- with Not_found -> raise (CannotCoerceTo "a reference")
- end
- | None -> raise (CannotCoerceTo "a reference")
-
-(* Quantified named or numbered hypothesis or hypothesis in context *)
-(* (as in Inversion) *)
-let coerce_to_quantified_hypothesis v =
- let v = Value.normalize v in
- if has_type v (topwit wit_intro_pattern) then
- let v = out_gen (topwit wit_intro_pattern) v in
- match v with
- | _, IntroNaming (IntroIdentifier id) -> NamedHyp id
- | _ -> raise (CannotCoerceTo "a quantified hypothesis")
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
- NamedHyp id
- else if has_type v (topwit wit_int) then
- AnonHyp (out_gen (topwit wit_int) v)
- else match Value.to_constr v with
- | Some c when isVar c -> NamedHyp (destVar c)
- | _ -> raise (CannotCoerceTo "a quantified hypothesis")
-
-(* Quantified named or numbered hypothesis or hypothesis in context *)
-(* (as in Inversion) *)
-let coerce_to_decl_or_quant_hyp env v =
- let v = Value.normalize v in
- if has_type v (topwit wit_int) then
- AnonHyp (out_gen (topwit wit_int) v)
- else
- try coerce_to_quantified_hypothesis v
- with CannotCoerceTo _ ->
- raise (CannotCoerceTo "a declared or quantified hypothesis")
-
-let coerce_to_int_or_var_list v =
- match Value.to_list v with
- | None -> raise (CannotCoerceTo "an int list")
- | Some l ->
- let map n = ArgArg (coerce_to_int n) in
- List.map map l
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
deleted file mode 100644
index 0b67f8726e..0000000000
--- a/tactics/taccoerce.mli
+++ /dev/null
@@ -1,96 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Util
-open Names
-open Term
-open Misctypes
-open Pattern
-open Genarg
-open Geninterp
-
-(** Coercions from highest level generic arguments to actual data used by Ltac
- interpretation. Those functions examinate dynamic types and try to return
- something sensible according to the object content. *)
-
-exception CannotCoerceTo of string
-(** Exception raised whenever a coercion failed. *)
-
-(** {5 High-level access to values}
-
- The [of_*] functions cast a given argument into a value. The [to_*] do the
- converse, and return [None] if there is a type mismatch.
-
-*)
-
-module Value :
-sig
- type t = Val.t
-
- val normalize : t -> t
- (** Eliminated the leading dynamic type casts. *)
-
- val of_constr : constr -> t
- val to_constr : t -> constr option
- val of_uconstr : Glob_term.closed_glob_constr -> t
- val to_uconstr : t -> Glob_term.closed_glob_constr option
- val of_int : int -> t
- val to_int : t -> int option
- val to_list : t -> t list option
- val to_option : t -> t option option
- val to_pair : t -> (t * t) option
-end
-
-(** {5 Coercion functions} *)
-
-val coerce_to_constr_context : Value.t -> constr
-
-val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t
-
-val coerce_to_ident_not_fresh : Evd.evar_map -> Environ.env -> Value.t -> Id.t
-
-val coerce_to_intro_pattern : Environ.env -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
-
-val coerce_to_intro_pattern_naming :
- Environ.env -> Value.t -> intro_pattern_naming_expr
-
-val coerce_to_hint_base : Value.t -> string
-
-val coerce_to_int : Value.t -> int
-
-val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders
-
-val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr
-
-val coerce_to_closed_constr : Environ.env -> Value.t -> constr
-
-val coerce_to_evaluable_ref :
- Environ.env -> Value.t -> evaluable_global_reference
-
-val coerce_to_constr_list : Environ.env -> Value.t -> constr list
-
-val coerce_to_intro_pattern_list :
- Loc.t -> Environ.env -> Value.t -> Tacexpr.intro_patterns
-
-val coerce_to_hyp : Environ.env -> Value.t -> Id.t
-
-val coerce_to_hyp_list : Environ.env -> Value.t -> Id.t list
-
-val coerce_to_reference : Environ.env -> Value.t -> Globnames.global_reference
-
-val coerce_to_quantified_hypothesis : Value.t -> quantified_hypothesis
-
-val coerce_to_decl_or_quant_hyp : Environ.env -> Value.t -> quantified_hypothesis
-
-val coerce_to_int_or_var_list : Value.t -> int or_var list
-
-(** {5 Missing generic arguments} *)
-
-val wit_constr_context : (Empty.t, Empty.t, constr) genarg_type
-
-val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type
diff --git a/tactics/tactic_matching.ml b/tactics/tactic_matching.ml
index 2144b75e74..004492e780 100644
--- a/tactics/tactic_matching.ml
+++ b/tactics/tactic_matching.ml
@@ -103,7 +103,7 @@ let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) =
(merged, Id.Map.merge merge lcm lm)
let matching_error =
- Errors.UserError ("tactic matching" , Pp.str "No matching clauses for match.")
+ CErrors.UserError ("tactic matching" , Pp.str "No matching clauses for match.")
let imatching_error = (matching_error, Exninfo.null)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 46145d1116..87fdcf14d4 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -521,7 +521,7 @@ module New = struct
try
let () = check_evars env sigma_final sigma sigma_initial in
tclUNIT x
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
tclZERO e
else
tclUNIT x
@@ -540,7 +540,7 @@ module New = struct
Proofview.tclOR
(Proofview.tclTIMEOUT n t)
begin function (e, info) -> match e with
- | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (Errors.print e)))
+ | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e)))
| e -> Proofview.tclZERO ~info e
end
@@ -551,7 +551,7 @@ module New = struct
let hyps = Proofview.Goal.hyps gl in
try
List.nth hyps (m-1)
- with Failure _ -> Errors.error "No such assumption."
+ with Failure _ -> CErrors.error "No such assumption."
let nLastDecls gl n =
try List.firstn n (Proofview.Goal.hyps gl)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cf842d6f19..2d901c2dbc 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -313,7 +313,18 @@ let apply_clear_request clear_flag dft c =
else Tacticals.New.tclIDTAC
(* Moving hypotheses *)
-let move_hyp id dest = Proofview.V82.tactic (Tacmach.move_hyp id dest)
+let move_hyp id dest =
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let ty = Proofview.Goal.raw_concl gl in
+ let store = Proofview.Goal.extra gl in
+ let sign = named_context_val env in
+ let sign' = move_hyp_in_named_context id dest sign in
+ let env = reset_with_named_context sign' env in
+ Refine.refine ~unsafe:true { run = begin fun sigma ->
+ Evarutil.new_evar env sigma ~principal:true ~store ty
+ end }
+ end }
(* Renaming hypotheses *)
let rename_hyp repl =
@@ -350,7 +361,7 @@ let rename_hyp repl =
let () =
try
let elt = Id.Set.choose (Id.Set.inter dst mods) in
- Errors.errorlabstrm "" (pr_id elt ++ str " is already used")
+ CErrors.errorlabstrm "" (pr_id elt ++ str " is already used")
with Not_found -> ()
in
(** All is well *)
@@ -366,7 +377,7 @@ let rename_hyp repl =
let nctx = Environ.val_of_named_context nhyps in
let instance = List.map (mkVar % get_id) hyps in
Refine.refine ~unsafe:true { run = begin fun sigma ->
- Evarutil.new_evar_instance nctx sigma nconcl ~store instance
+ Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance
end }
end }
@@ -537,7 +548,7 @@ let fix ido n = match ido with
mutual_fix id n [] 0
let rec check_is_mutcoind env sigma cl =
- let b = whd_betadeltaiota env sigma cl in
+ let b = whd_all env sigma cl in
match kind_of_term b with
| Prod (na, c1, b) ->
let open Context.Rel.Declaration in
@@ -774,15 +785,15 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in
if not b then
if
- isSort (whd_betadeltaiota env sigma t1) &&
- isSort (whd_betadeltaiota env sigma t2)
+ isSort (whd_all env sigma t1) &&
+ isSort (whd_all env sigma t2)
then (mayneedglobalcheck := true; sigma)
else
errorlabstrm "convert-check-hyp" (str "Types are incompatible.")
else sigma
end
else
- if not (isSort (whd_betadeltaiota env sigma t1)) then
+ if not (isSort (whd_all env sigma t1)) then
errorlabstrm "convert-check-hyp" (str "Not a type.")
else sigma
@@ -869,14 +880,17 @@ let reduction_clause redexp cl =
(None, bind_red_expr_occurrences occs nbcl redexp)) cl
let reduce redexp cl =
+ let trace () = Pp.(hov 2 (Pptactic.pr_atomic_tactic (Global.env()) (TacReduce (redexp,cl)))) in
+ Proofview.Trace.name_tactic trace begin
Proofview.Goal.enter { enter = begin fun gl ->
- let cl = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
- let redexps = reduction_clause redexp cl in
+ let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
+ let redexps = reduction_clause redexp cl' in
let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
Tacticals.New.tclMAP (fun (where,redexp) ->
e_reduct_option ~check
(Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps
end }
+ end
(* Unfolding occurrences of a constant *)
@@ -1204,7 +1218,7 @@ let cut c =
try
(** Backward compat: ensure that [c] is well-typed. *)
let typ = Typing.unsafe_type_of env sigma c in
- let typ = whd_betadeltaiota env sigma typ in
+ let typ = whd_all env sigma typ in
match kind_of_term typ with
| Sort _ -> true
| _ -> false
@@ -1270,7 +1284,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
let naming = NamingMustBe (dloc,targetid) in
let with_clear = do_replace (Some id) naming in
Tacticals.New.tclTHEN
- (Proofview.Unsafe.tclEVARS clenv.evd)
+ (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
(if sidecond_first then
Tacticals.New.tclTHENFIRST
(assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac
@@ -1472,7 +1486,7 @@ let default_elim with_evars clear_flag (c,_ as cx) =
begin function (e, info) -> match e with
| IsNonrec ->
(* For records, induction principles aren't there by default
- anymore. Instead, we do a case analysis instead. *)
+ anymore. Instead, we do a case analysis. *)
general_case_analysis with_evars clear_flag cx
| e -> Proofview.tclZERO ~info e
end
@@ -1807,8 +1821,8 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) =
let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in
let rec aux clause =
try progress_with_clause flags innerclause clause
- with e when Errors.noncritical e ->
- let e = Errors.push e in
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
try aux (clenv_push_prod clause)
with NotExtensibleClause -> iraise e
in
@@ -1838,8 +1852,8 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
clear idstoclear;
tac id
])
- with e when with_destruct && Errors.noncritical e ->
- let (e, info) = Errors.push e in
+ with e when with_destruct && CErrors.noncritical e ->
+ let (e, info) = CErrors.push e in
(descend_in_conjunctions [targetid]
(fun b id -> aux (id::idstoclear) b (mkVar id))
(e, info) c)
@@ -1987,7 +2001,7 @@ let check_is_type env sigma ty =
try
let _ = Typing.e_sort_of env evdref ty in
!evdref
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
raise (DependsOnBody None)
let check_decl env sigma decl =
@@ -2001,7 +2015,7 @@ let check_decl env sigma decl =
| LocalDef (_,c,_) -> Typing.e_check env evdref c ty
in
!evdref
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
let id = get_id decl in
raise (DependsOnBody (Some id))
@@ -2293,8 +2307,8 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let type_of = Tacmach.New.pf_unsafe_type_of gl in
- let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in
- let t = whd_betadeltaiota (type_of (mkVar id)) in
+ let whd_all = Tacmach.New.pf_apply whd_all gl in
+ let t = whd_all (type_of (mkVar id)) in
let eqtac, thin = match match_with_equality_type t with
| Some (hdcncl,[_;lhs;rhs]) ->
if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then
@@ -2665,10 +2679,15 @@ let letin_tac with_eq id c ty occs =
let env = Proofview.Goal.env gl in
let ccl = Proofview.Goal.concl gl in
let abs = AbstractExact (id,c,ty,occs,true) in
- let (id,_,depdecls,lastlhyp,ccl,_) = make_abstraction env sigma ccl abs in
- (* We keep the original term to match *)
+ let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in
+ (* We keep the original term to match but record the potential side-effects
+ of unifying universes. *)
+ let Sigma (c, sigma, p) = match res with
+ | None -> Sigma.here c sigma
+ | Some (Sigma (_, sigma, p)) -> Sigma (c, sigma, p)
+ in
let tac = letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty in
- Sigma.here tac sigma
+ Sigma (tac, sigma, p)
end }
let letin_pat_tac with_eq id c occs =
@@ -3880,7 +3899,7 @@ let compute_elim_sig ?elimc elimt =
| Some (LocalAssum (_,ind)) ->
let indhd,indargs = decompose_app ind in
try {!res with indref = Some (global_of_constr indhd) }
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
error "Cannot find the inductive type of the inductive scheme."
let compute_scheme_signature scheme names_info ind_type_guess =
@@ -4253,7 +4272,7 @@ let check_enough_applied env sigma elim =
| None ->
(* No eliminator given *)
fun u ->
- let t,_ = decompose_app (whd_betadeltaiota env sigma u) in isInd t
+ let t,_ = decompose_app (whd_all env sigma u) in isInd t
| Some elimc ->
let elimt = Retyping.get_type_of env sigma (fst elimc) in
let scheme = compute_elim_sig ~elimc elimt in
@@ -4573,7 +4592,7 @@ let maybe_betadeltaiota_concl allowred gl =
if not allowred then concl
else
let env = Proofview.Goal.env gl in
- whd_betadeltaiota env sigma concl
+ whd_all env sigma concl
let reflexivity_red allowred =
Proofview.Goal.enter { enter = begin fun gl ->
@@ -4851,7 +4870,7 @@ let abstract_subproof id gk tac =
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) = Errors.push src in
+ let (_, info) = CErrors.push src in
iraise (e, info)
in
let const, args =
@@ -4860,8 +4879,13 @@ let abstract_subproof id gk tac =
in
let cd = Entries.DefinitionEntry const in
let decl = (cd, IsProof Lemma) in
- (** ppedrot: seems legit to have abstracted subproofs as local*)
- let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in
+ let cst () =
+ (** do not compute the implicit arguments, it may be costly *)
+ let () = Impargs.make_implicit_args false in
+ (** ppedrot: seems legit to have abstracted subproofs as local*)
+ Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl
+ in
+ let cst = Impargs.with_implicit_protection cst () in
(* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *)
let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in
let evd = Evd.set_universe_context evd ectx in
@@ -4911,7 +4935,7 @@ let unify ?(state=full_transparent_state) x y =
let sigma = Sigma.to_evar_map sigma in
let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in
Sigma.Unsafe.of_pair (Proofview.tclUNIT (), sigma)
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
Sigma.here (Tacticals.New.tclFAIL 0 (str"Not unifiable")) sigma
end }
@@ -4944,8 +4968,8 @@ module New = struct
let reduce_after_refine =
reduce
- (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]})
- {onhyps=None; concl_occs=AllOccurrences }
+ (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]})
+ {onhyps=Some []; concl_occs=AllOccurrences }
let refine ?unsafe c =
Refine.refine ?unsafe c <*>
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 48722f655a..093302608e 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -12,7 +12,6 @@ Equality
Contradiction
Inv
Leminv
-Taccoerce
Hints
Auto
Eauto
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 05:53:21 +0000