summaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
commit9ebf44d84754adc5b64fcf612c6816c02c80462d (patch)
treebf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /tactics
parent9043add656177eeac1491a73d2f3ab92bec0013c (diff)
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml9
-rw-r--r--tactics/autorewrite.ml26
-rw-r--r--tactics/btermdn.ml4
-rw-r--r--tactics/class_tactics.ml54
-rw-r--r--tactics/contradiction.ml5
-rw-r--r--tactics/contradiction.mli2
-rw-r--r--tactics/eauto.ml11
-rw-r--r--tactics/elim.mli3
-rw-r--r--tactics/elimschemes.ml6
-rw-r--r--tactics/eqdecide.ml12
-rw-r--r--tactics/eqschemes.ml43
-rw-r--r--tactics/equality.ml63
-rw-r--r--tactics/equality.mli18
-rw-r--r--tactics/hints.ml241
-rw-r--r--tactics/hints.mli76
-rw-r--r--tactics/hipattern.ml12
-rw-r--r--tactics/hipattern.mli2
-rw-r--r--tactics/ind_tables.ml10
-rw-r--r--tactics/inv.ml33
-rw-r--r--tactics/inv.mli6
-rw-r--r--tactics/leminv.ml9
-rw-r--r--tactics/leminv.mli2
-rw-r--r--tactics/tacticals.ml73
-rw-r--r--tactics/tacticals.mli11
-rw-r--r--tactics/tactics.ml296
-rw-r--r--tactics/tactics.mli44
-rw-r--r--tactics/term_dnet.ml4
-rw-r--r--tactics/term_dnet.mli2
28 files changed, 630 insertions, 447 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0c0d9bcf..d7de6c4f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -8,8 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-module CVars = Vars
-
open Pp
open Util
open Names
@@ -81,15 +79,14 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
let clenv, c =
if poly then
(** Refresh the instance of the hint *)
- let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
- let map c = CVars.subst_univs_level_constr subst c in
+ 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. *)
let clenv = {
templval = Evd.map_fl emap clenv.templval;
templtyp = Evd.map_fl emap clenv.templtyp;
- evd = Evd.map_metas map evd;
+ evd = Evd.map_metas emap evd;
env = Proofview.Goal.env gl;
} in
clenv, emap c
@@ -102,7 +99,7 @@ let unify_resolve poly flags ((c : raw_hint), clenv) =
Proofview.Goal.enter begin fun gl ->
let clenv, c = connect_hint_clenv poly c clenv gl in
let clenv = clenv_unique_resolver ~flags clenv gl in
- Clenvtac.clenv_refine false clenv
+ Clenvtac.clenv_refine clenv
end
let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index c3857e6b..c8fd0b7a 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -30,7 +30,7 @@ let subst_hint subst hint =
let cst' = subst_mps subst hint.rew_lemma in
let typ' = subst_mps subst hint.rew_type in
let pat' = subst_mps subst hint.rew_pat in
- let t' = Option.smartmap (Genintern.generic_substitute subst) hint.rew_tac in
+ let t' = Option.Smart.map (Genintern.generic_substitute subst) hint.rew_tac in
if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else
{ hint with
rew_lemma = cst'; rew_type = typ';
@@ -93,7 +93,7 @@ let one_base general_rewrite_maybe_in tac_main bas =
let try_rewrite dir ctx c tc =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
- let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
+ let subst, ctx' = UnivGen.fresh_universe_context_set_instance ctx in
let c' = Vars.subst_univs_level_constr subst c in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
@@ -228,7 +228,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
if metas then eqclause
else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
in
- let (equiv, args) = decompose_app (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in
+ let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
| x::y::z ->
@@ -236,17 +236,19 @@ let decompose_applied_relation metas env sigma c ctype left2right =
| _ -> raise Not_found
in
try
- let others,(c1,c2) = split_last_two args in
- let ty1, ty2 =
- Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2)
- in
- let ty = EConstr.Unsafe.to_constr ty in
- let ty1 = EConstr.Unsafe.to_constr ty1 in
+ let others,(c1,c2) = split_last_two args in
+ let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in
+ (* XXX: It looks like mk_clenv_from_env should be fixed instead? *)
+ let open EConstr in
+ let hyp_ty = Unsafe.to_constr ty in
+ let hyp_car = Unsafe.to_constr ty1 in
+ let hyp_prf = Unsafe.to_constr @@ Clenv.clenv_value eqclause in
+ let hyp_rel = Unsafe.to_constr @@ mkApp (equiv, Array.of_list others) in
+ let hyp_left = Unsafe.to_constr @@ c1 in
+ let hyp_right = Unsafe.to_constr @@ c2 in
(* if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
(* else *)
- Some { hyp_cl=eqclause; hyp_prf=EConstr.Unsafe.to_constr (Clenv.clenv_value eqclause); hyp_ty = ty;
- hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others);
- hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; }
+ Some { hyp_cl=eqclause; hyp_prf; hyp_ty; hyp_car; hyp_rel; hyp_l2r=left2right; hyp_left; hyp_right; }
with Not_found -> None
in
match find_rel ctype with
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 8e50c977..aca7f6c6 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -9,7 +9,7 @@
(************************************************************************)
open Util
-open Term
+open Constr
open EConstr
open Names
open Pattern
@@ -22,7 +22,7 @@ open Globnames
let dnet_depth = ref 8
type term_label =
-| GRLabel of global_reference
+| GRLabel of GlobRef.t
| ProdLabel
| LambdaLabel
| SortLabel
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 73b649e5..29797240 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -18,6 +18,7 @@ open CErrors
open Util
open Names
open Term
+open Constr
open Termops
open EConstr
open Tacmach
@@ -206,7 +207,7 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls)
with e -> Proofview.tclZERO e
in resolve >>= fun clenv' ->
- Clenvtac.clenv_refine with_evars ~with_classes:false clenv'
+ Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
end
let unify_e_resolve poly flags = begin fun gls (c,_,clenv) ->
@@ -226,7 +227,7 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
Refine.refine ~typecheck:false begin fun sigma ->
let sigma, term, ty =
if poly then
- let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
+ let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
let map c = Vars.subst_univs_level_constr subst c in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
sigma, map c, map t
@@ -476,7 +477,7 @@ let is_Prop env sigma concl =
match EConstr.kind sigma ty with
| Sort s ->
begin match ESorts.kind sigma s with
- | Prop Null -> true
+ | Prop -> true
| _ -> false
end
| _ -> false
@@ -546,12 +547,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
let hints = build_subclasses ~check:false env sigma (VarRef id) empty_hint_info in
(List.map_append
(fun (path,info,c) ->
- let info =
- { info with Vernacexpr.hint_pattern =
- Option.map (Constrintern.intern_constr_pattern env sigma)
- info.Vernacexpr.hint_pattern }
- in
- make_resolves env sigma ~name:(PathHints path)
+ make_resolves env sigma ~name:(PathHints path)
(true,false,not !Flags.quiet) info false
(IsConstr (EConstr.of_constr c,Univ.ContextSet.empty)))
hints)
@@ -653,17 +649,6 @@ module Search = struct
Evd.add sigma gl evi')
sigma goals
- let fail_if_nonclass info =
- Proofview.Goal.enter begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
- if is_class_type sigma (Proofview.Goal.concl gl) then
- Proofview.tclUNIT ()
- else (if !typeclasses_debug > 1 then
- Feedback.msg_debug (pr_depth info.search_depth ++
- str": failure due to non-class subgoal " ++
- pr_ev sigma (Proofview.Goal.goal gl));
- Proofview.tclZERO NoApplicableEx) end
-
(** The general hint application tactic.
tac1 + tac2 .... The choice of OR or ORELSE is determined
depending on the dependencies of the goal and the unique/Prop
@@ -708,8 +693,9 @@ module Search = struct
let msg =
match fst ie with
| Pretype_errors.PretypeError (env, evd, Pretype_errors.CannotUnify (x,y,_)) ->
- str"Cannot unify " ++ print_constr_env env evd x ++ str" and " ++
- print_constr_env env evd y
+ str"Cannot unify " ++
+ Printer.pr_econstr_env env evd x ++ str" and " ++
+ Printer.pr_econstr_env env evd y
| ReachedLimitEx -> str "Proof-search reached its limit."
| NoApplicableEx -> str "Proof-search failed."
| e -> CErrors.iprint ie
@@ -802,13 +788,8 @@ module Search = struct
in
if path_matches derivs [] then aux e tl
else
- let filter =
- if false (* in 8.6, still allow non-class subgoals
- info.search_only_classes *) then fail_if_nonclass info
- else Proofview.tclUNIT ()
- in
ortac
- (with_shelf (tac <*> filter) >>= fun s ->
+ (with_shelf tac >>= fun s ->
let i = !idx in incr idx; result s i None)
(fun e' ->
if CErrors.noncritical (fst e') then
@@ -872,12 +853,9 @@ module Search = struct
let search_tac_gl ?st only_classes dep hints depth i sigma gls gl :
unit Proofview.tactic =
let open Proofview in
- if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then
- Tacticals.New.tclZEROMSG (str"Not a subgoal for a class")
- else
- let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
- let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
- search_tac hints depth 1 info
+ let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
+ let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
+ search_tac hints depth 1 info
let search_tac ?(st=full_transparent_state) only_classes dep hints depth =
let open Proofview in
@@ -1030,8 +1008,8 @@ module Intpart = Unionfind.Make(Evar.Set)(Evar.Map)
let deps_of_constraints cstrs evm p =
List.iter (fun (_, _, x, y) ->
- let evx = Evarutil.undefined_evars_of_term evm (EConstr.of_constr x) in
- let evy = Evarutil.undefined_evars_of_term evm (EConstr.of_constr y) in
+ let evx = Evarutil.undefined_evars_of_term evm x in
+ let evy = Evarutil.undefined_evars_of_term evm y in
Intpart.union_set (Evar.Set.union evx evy) p)
cstrs
@@ -1076,7 +1054,7 @@ let error_unresolvable env comp evd =
| Some s -> Evar.Set.mem ev s
in
let fold ev evi (found, accu) =
- let ev_class = class_of_constr evd (EConstr.of_constr evi.evar_concl) in
+ let ev_class = class_of_constr evd evi.evar_concl in
if not (Option.is_empty ev_class) && is_part ev then
(* focus on one instance if only one was searched for *)
if not found then (true, Some ev)
@@ -1174,7 +1152,7 @@ let solve_inst env evd filter unique split fail =
let _ =
Hook.set Typeclasses.solve_all_instances_hook solve_inst
-let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
+let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in
let (gl,t,sigma) =
Goal.V82.mk_goal sigma nc gl Store.empty in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c285f21e..e12063fd 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -8,13 +8,12 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Term
+open Constr
open EConstr
open Hipattern
open Tactics
open Coqlib
open Reductionops
-open Misctypes
open Proofview.Notations
module NamedDecl = Context.Named.Declaration
@@ -120,7 +119,7 @@ let contradiction_term (c,lbind as cl) =
else
Proofview.tclORELSE
begin
- if lbind = NoBindings then
+ if lbind = Tactypes.NoBindings then
filter_hyp (fun c -> is_negation_of env sigma typ c)
(fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
else
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 2b3a9475..4bb3263f 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -9,7 +9,7 @@
(************************************************************************)
open EConstr
-open Misctypes
+open Tactypes
val absurd : constr -> unit Proofview.tactic
val contradiction : constr with_bindings option -> unit Proofview.tactic
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index dc310c54..80d07c5c 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -12,7 +12,7 @@ open Pp
open CErrors
open Util
open Names
-open Term
+open Constr
open Termops
open EConstr
open Proof_type
@@ -70,11 +70,10 @@ let first_goal gls =
(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
let apply_tac_list tac glls =
- let (sigr,lg) = unpackage glls in
- match lg with
+ match glls.it with
| (g1::rest) ->
- let gl = apply_sig_tac sigr tac g1 in
- repackage sigr (gl@rest)
+ let pack = tac (re_sig g1 glls.sigma) in
+ re_sig (pack.it @ rest) pack.sigma
| _ -> user_err Pp.(str "apply_tac_list")
let one_step l gl =
@@ -90,7 +89,7 @@ let rec prolog l n gl =
let out_term env = function
| IsConstr (c, _) -> c
- | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr))
+ | IsGlobRef gr -> EConstr.of_constr (fst (UnivGen.fresh_global_instance env gr))
let prolog_tac l n =
Proofview.V82.tactic begin fun gl ->
diff --git a/tactics/elim.mli b/tactics/elim.mli
index d6b67e5b..ddfac3f2 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -11,12 +11,11 @@
open Names
open EConstr
open Tacticals
-open Misctypes
open Tactypes
(** Eliminations tactics. *)
-val introCaseAssumsThen : evars_flag ->
+val introCaseAssumsThen : Tactics.evars_flag ->
(intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
branch_args -> unit Proofview.tactic
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 6bd4866c..3b69d992 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -44,10 +44,10 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
mib.mind_nparams_rec
else
mib.mind_nparams in
- let sigma, sort = Evd.fresh_sort_in_family env sigma sort in
+ let sigma, sort = Evd.fresh_sort_in_family sigma sort in
let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in
- let sigma, nf = Evarutil.nf_evars_and_universes sigma in
- (nf c', Evd.evar_universe_context sigma), eff
+ let sigma = Evd.minimize_universes sigma in
+ (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff
else
let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
let sigma, c = build_induction_scheme env sigma pind dep sort in
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index b0deeed1..832014a6 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -17,18 +17,18 @@
open Util
open Names
open Namegen
-open Term
+open Constr
open EConstr
open Declarations
open Tactics
open Tacticals.New
open Auto
open Constr_matching
-open Misctypes
open Hipattern
open Proofview.Notations
open Tacmach.New
open Coqlib
+open Tactypes
(* This file containts the implementation of the tactics ``Decide
Equality'' and ``Compare''. They can be used to decide the
@@ -58,14 +58,14 @@ let clear_last =
let choose_eq eqonleft =
if eqonleft then
- left_with_bindings false Misctypes.NoBindings
+ left_with_bindings false NoBindings
else
- right_with_bindings false Misctypes.NoBindings
+ right_with_bindings false NoBindings
let choose_noteq eqonleft =
if eqonleft then
- right_with_bindings false Misctypes.NoBindings
+ right_with_bindings false NoBindings
else
- left_with_bindings false Misctypes.NoBindings
+ left_with_bindings false NoBindings
(* A surgical generalize which selects the right occurrences by hand *)
(* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 477de645..ea5ff4a6 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -78,7 +78,7 @@ let build_dependent_inductive ind (mib,mip) =
Context.Rel.to_extended_list mkRel mip.mind_nrealdecls mib.mind_params_ctxt
@ Context.Rel.to_extended_list mkRel 0 realargs)
-let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na
+let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na
let name_assumption env = function
| LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
| LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
@@ -102,15 +102,20 @@ let get_coq_eq ctx =
let eq = Globnames.destIndRef Coqlib.glob_eq in
(* Do not force the lazy if they are not defined *)
let eq, ctx = with_context_set ctx
- (Universes.fresh_inductive_instance (Global.env ()) eq) in
+ (UnivGen.fresh_inductive_instance (Global.env ()) eq) in
mkIndU eq, mkConstructUi (eq,1), ctx
with Not_found ->
user_err Pp.(str "eq not found.")
let univ_of_eq env eq =
- let eq = EConstr.of_constr eq in
- match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with
- | Prod (_,t,_) -> (match Constr.kind t with Sort (Type u) -> u | _ -> assert false)
+ let open EConstr in
+ let eq = of_constr eq in
+ let sigma = Evd.from_env env in
+ match kind sigma (Retyping.get_type_of env sigma eq) with
+ | Prod (_,t,_) -> (match kind sigma t with
+ Sort k ->
+ (match ESorts.kind sigma k with Type u -> u | _ -> assert false)
+ | _ -> assert false)
| _ -> assert false
(**********************************************************************)
@@ -192,7 +197,7 @@ let get_non_sym_eq_data env (ind,u) =
(**********************************************************************)
let build_sym_scheme env ind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ 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 cstr n =
@@ -241,11 +246,11 @@ let sym_scheme_kind =
let const_of_scheme kind env ind ctx =
let sym_scheme, eff = (find_scheme kind ind) in
let sym, ctx = with_context_set ctx
- (Universes.fresh_constant_instance (Global.env()) sym_scheme) in
+ (UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in
mkConstU sym, ctx, eff
let build_sym_involutive_scheme env ind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ 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
@@ -353,7 +358,7 @@ let sym_involutive_scheme_kind =
(**********************************************************************)
let build_l2r_rew_scheme dep env ind kind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ 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
@@ -392,7 +397,7 @@ let build_l2r_rew_scheme dep env ind kind =
rel_vect (nrealargs+4) nrealargs;
rel_vect 1 nrealargs;
[|mkRel 1|]]) in
- let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+ let s, ctx' = UnivGen.fresh_sort_in_family kind in
let ctx = Univ.ContextSet.union ctx ctx' in
let s = mkSort s in
let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -469,7 +474,7 @@ let build_l2r_rew_scheme dep env ind kind =
(**********************************************************************)
let build_l2r_forward_rew_scheme dep env ind kind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ 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 cstr n p =
@@ -495,7 +500,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
let realsign_ind_P n aP =
name_context env ((LocalAssum (Name varH,aP))::realsign_P n) in
- let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+ let s, ctx' = UnivGen.fresh_sort_in_family kind in
let ctx = Univ.ContextSet.union ctx ctx' in
let s = mkSort s in
let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -561,7 +566,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
(**********************************************************************)
let build_r2l_forward_rew_scheme dep env ind kind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) =
get_non_sym_eq_data env indu in
let cstr n =
@@ -573,7 +578,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
let applied_ind = build_dependent_inductive indu specif in
let realsign_ind =
name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
- let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+ let s, ctx' = UnivGen.fresh_sort_in_family kind in
let ctx = Univ.ContextSet.union ctx ctx' in
let s = mkSort s in
let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -620,7 +625,9 @@ let build_r2l_forward_rew_scheme dep env ind kind =
(**********************************************************************)
let fix_r2l_forward_rew_scheme (c, ctx') =
- let t = Retyping.get_type_of (Global.env()) Evd.empty (EConstr.of_constr c) in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in
let t = EConstr.Unsafe.to_constr t in
let ctx,_ = decompose_prod_assum t in
match ctx with
@@ -630,7 +637,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
(mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p)
(mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp)
(mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind)
- (EConstr.Unsafe.to_constr (Reductionops.whd_beta Evd.empty
+ (EConstr.Unsafe.to_constr (Reductionops.whd_beta sigma
(EConstr.of_constr (applist (c,
Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
in c', ctx'
@@ -755,7 +762,7 @@ let rew_r2l_scheme_kind =
let build_congr env (eq,refl,ctx) ind =
let (ind,u as indu), ctx = with_context_set ctx
- (Universes.fresh_inductive_instance env ind) in
+ (UnivGen.fresh_inductive_instance env ind) in
let (mib,mip) = lookup_mind_specif env ind in
if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then
error "Not an inductive type with a single constructor.";
@@ -778,7 +785,7 @@ let build_congr env (eq,refl,ctx) ind =
let varH = fresh env (Id.of_string "H") in
let varf = fresh env (Id.of_string "f") in
let ci = make_case_info (Global.env()) ind RegularStyle in
- let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in
+ let uni, ctx = UnivGen.extend_context (UnivGen.new_global_univ ()) ctx in
let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in
let c =
my_it_mkLambda_or_LetIn paramsctxt
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 5821717d..0e392157 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -15,6 +15,7 @@ open Util
open Names
open Nameops
open Term
+open Constr
open Termops
open EConstr
open Vars
@@ -41,7 +42,7 @@ open Ind_tables
open Eqschemes
open Locus
open Locusops
-open Misctypes
+open Tactypes
open Proofview.Notations
open Unification
open Context.Named.Declaration
@@ -153,7 +154,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
let c1 = args.(arglen - 2) in
let c2 = args.(arglen - 1) in
let try_occ (evd', c') =
- Clenvtac.clenv_pose_dependent_evars true {eqclause with evd = evd'}
+ Clenvtac.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'}
in
let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
let occs =
@@ -545,6 +546,12 @@ let apply_special_clear_request clear_flag f =
e when catchable_exception e -> tclIDTAC
end
+type multi =
+ | Precisely of int
+ | UpTo of int
+ | RepeatStar
+ | RepeatPlus
+
let general_multi_rewrite with_evars l cl tac =
let do1 l2r f =
Proofview.Goal.enter begin fun gl ->
@@ -935,7 +942,7 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function
let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
let newc = mkRel(cnum_nlams-argnum) in
let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in
- kont sigma subval (false_0,mkSort (Prop Null))
+ kont sigma subval (false_0,mkProp)
(* Note: discrimination could be more clever: if some elimination is
not allowed because of a large impredicative constructor in the
@@ -1036,7 +1043,7 @@ let onEquality with_evars tac (c,lbindc) =
let t = type_of c in
let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
- let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
+ let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in
let eqn = clenv_type eq_clause' in
let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in
tclTHEN
@@ -1108,8 +1115,6 @@ let make_tuple env sigma (rterm,rty) lind =
let p = mkLambda (na, a, rty) in
let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
let sigma, sig_term = Evd.fresh_global env sigma sigdata.typ in
- let exist_term = EConstr.of_constr exist_term in
- let sig_term = EConstr.of_constr sig_term in
sigma,
(applist(exist_term,[a;p;(mkRel lind);rterm]),
applist(sig_term,[a;p]))
@@ -1178,35 +1183,35 @@ let minimal_free_rels_rec env sigma =
let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
let sigdata = find_sigma_data env sort_of_ty in
- let evdref = ref (Evd.clear_metas sigma) in
- let rec sigrec_clausal_form siglen p_i =
+ let rec sigrec_clausal_form sigma siglen p_i =
if Int.equal siglen 0 then
(* is the default value typable with the expected type *)
let dflt_typ = unsafe_type_of env sigma dflt in
try
- let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
- let () =
- evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in
- dflt
+ let sigma = Evarconv.the_conv_x_leq env dflt_typ p_i sigma in
+ let sigma =
+ Evarconv.solve_unif_constraints_with_heuristics env sigma in
+ sigma, dflt
with Evarconv.UnableToUnify _ ->
user_err Pp.(str "Cannot solve a unification problem.")
else
- let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
+ let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with
| (_sigS,[a;p]) -> (a, p)
| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in
- let ev = Evarutil.e_new_evar env evdref a in
+ let sigma, ev = Evarutil.new_evar env sigma a in
let rty = beta_applist sigma (p_i_minus_1,[ev]) in
- let tuple_tail = sigrec_clausal_form (siglen-1) rty in
- let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in
+ let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in
+ let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in
match evopt with
| Some w ->
- let w_type = unsafe_type_of env !evdref w in
- if Evarconv.e_cumul env evdref w_type a then
- let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
- let exist_term = EConstr.of_constr exist_term in
- applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
- else
+ let w_type = unsafe_type_of env sigma w in
+ begin match Evarconv.cumul env sigma w_type a with
+ | Some sigma ->
+ let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
+ sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+ | None ->
user_err Pp.(str "Cannot solve a unification problem.")
+ end
| None ->
(* This at least happens if what has been detected as a
dependency is not one; use an evasive error message;
@@ -1216,8 +1221,9 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
unsolved evars would mean not binding rel *)
user_err Pp.(str "Cannot solve a unification problem.")
in
- let scf = sigrec_clausal_form siglen ty in
- !evdref, Evarutil.nf_evar !evdref scf
+ let sigma = Evd.clear_metas sigma in
+ let sigma, scf = sigrec_clausal_form sigma siglen ty in
+ sigma, Evarutil.nf_evar sigma scf
(* The problem is to build a destructor (a generalization of the
predecessor) which, when applied to a term made of constructors
@@ -1372,7 +1378,6 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in
let injfun = mkNamedLambda e t injbody in
let sigma,congr = Evd.fresh_global env sigma eq.congr in
- let congr = EConstr.of_constr congr in
let pf = applist(congr,[t;resty;injfun;t1;t2]) in
let sigma, pf_typ = Typing.type_of env sigma pf in
let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
@@ -1783,7 +1788,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
try
let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
let u = EInstance.kind sigma u in
- let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
+ let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
match EConstr.kind sigma x, EConstr.kind sigma y with
| Var z, _ when not (is_evaluable env (EvalVarRef z)) ->
@@ -1809,9 +1814,9 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else
match EConstr.kind sigma x, EConstr.kind sigma y with
- | Var x', _ when not (dependent sigma x y) && not (is_evaluable env (EvalVarRef x')) ->
+ | Var x', _ when not (Termops.local_occur_var sigma x' y) && not (is_evaluable env (EvalVarRef x')) ->
subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
- | _, Var y' when not (dependent sigma y x) && not (is_evaluable env (EvalVarRef y')) ->
+ | _, Var y' when not (Termops.local_occur_var sigma y' x) && not (is_evaluable env (EvalVarRef y')) ->
subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
| _ ->
Proofview.tclUNIT ()
@@ -1834,7 +1839,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
try
let lbeq,u,(_,x,y) = find_eq_data_decompose c in
let u = EInstance.kind sigma u in
- let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
+ let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
if EConstr.eq_constr sigma x y then failwith "caught";
diff --git a/tactics/equality.mli b/tactics/equality.mli
index c0be917a..6f3e08ea 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -15,8 +15,8 @@ open EConstr
open Environ
open Ind_tables
open Locus
-open Misctypes
open Tactypes
+open Tactics
(*i*)
type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
@@ -61,6 +61,12 @@ val general_rewrite_in :
val general_rewrite_clause :
orientation -> evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> clause -> unit Proofview.tactic
+type multi =
+ | Precisely of int
+ | UpTo of int
+ | RepeatStar
+ | RepeatPlus
+
val general_multi_rewrite :
evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list ->
clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
@@ -80,20 +86,20 @@ val discrConcl : unit Proofview.tactic
val discrHyp : Id.t -> unit Proofview.tactic
val discrEverywhere : evars_flag -> unit Proofview.tactic
val discr_tac : evars_flag ->
- constr with_bindings destruction_arg option -> unit Proofview.tactic
+ constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
(* Below, if flag is [None], it takes the value from the dynamic value of the option *)
val inj : inj_flags option -> intro_patterns option -> evars_flag ->
clear_flag -> constr with_bindings -> unit Proofview.tactic
val injClause : inj_flags option -> intro_patterns option -> evars_flag ->
- constr with_bindings destruction_arg option -> unit Proofview.tactic
+ constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
val injHyp : inj_flags option -> clear_flag -> Id.t -> unit Proofview.tactic
val injConcl : inj_flags option -> unit Proofview.tactic
val simpleInjClause : inj_flags option -> evars_flag ->
- constr with_bindings destruction_arg option -> unit Proofview.tactic
+ constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
-val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic
-val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic
+val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
+val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
val make_iterated_tuple :
env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 500abc5b..43a450ea 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -12,7 +12,7 @@ open Pp
open Util
open CErrors
open Names
-open Term
+open Constr
open Evd
open EConstr
open Vars
@@ -23,17 +23,16 @@ open Libobject
open Namegen
open Libnames
open Smartlocate
-open Misctypes
open Termops
open Inductiveops
open Typing
open Decl_kinds
+open Typeclasses
open Pattern
open Patternops
open Clenv
open Tacred
open Printer
-open Vernacexpr
module NamedDecl = Context.Named.Declaration
@@ -94,13 +93,14 @@ let secvars_of_hyps hyps =
else pred
let empty_hint_info =
- let open Vernacexpr in
{ hint_priority = None; hint_pattern = None }
(************************************************************************)
(* 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 *)
@@ -115,7 +115,7 @@ type 'a hints_path_atom_gen =
(* For forward hints, their names is the list of projections *)
| PathAny
-type hints_path_atom = global_reference hints_path_atom_gen
+type hints_path_atom = GlobRef.t hints_path_atom_gen
type 'a hints_path_gen =
| PathAtom of 'a hints_path_atom_gen
@@ -125,11 +125,11 @@ type 'a hints_path_gen =
| PathEmpty
| PathEpsilon
-type pre_hints_path = Libnames.reference hints_path_gen
-type hints_path = global_reference hints_path_gen
+type pre_hints_path = Libnames.qualid hints_path_gen
+type hints_path = GlobRef.t hints_path_gen
type hint_term =
- | IsGlobRef of global_reference
+ | IsGlobRef of GlobRef.t
| IsConstr of constr * Univ.ContextSet.t
type 'a with_uid = {
@@ -153,9 +153,33 @@ type 'a with_metadata = {
type full_hint = hint with_metadata
-type hint_entry = global_reference option *
+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 *)
+ | ModeOutput (* Anything *)
+
+type 'a hints_transparency_target =
+ | HintsVariables
+ | 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
@@ -275,16 +299,16 @@ let strip_params env sigma c =
match EConstr.kind sigma c with
| App (f, args) ->
(match EConstr.kind sigma f with
- | Const (p,_) ->
- let cb = lookup_constant p env in
- (match cb.Declarations.const_proj with
- | Some pb ->
- let n = pb.Declarations.proj_npars in
- if Array.length args > n then
- mkApp (mkProj (Projection.make p false, args.(n)),
- Array.sub args (n+1) (Array.length args - (n + 1)))
- else c
- | None -> c)
+ | Const (cst,_) ->
+ (match Recordops.find_primitive_projection cst with
+ | Some p ->
+ let p = Projection.make p false in
+ let npars = Projection.npars p in
+ if Array.length args > npars then
+ mkApp (mkProj (p, args.(npars)),
+ Array.sub args (npars+1) (Array.length args - (npars + 1)))
+ else c
+ | None -> c)
| _ -> c)
| _ -> c
@@ -308,7 +332,7 @@ let instantiate_hint env sigma p =
{ p with code = { p.code with obj = code } }
let hints_path_atom_eq h1 h2 = match h1, h2 with
-| PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2
+| PathHints l1, PathHints l2 -> List.equal GlobRef.equal l1 l2
| PathAny, PathAny -> true
| _ -> false
@@ -365,7 +389,7 @@ let path_seq p p' =
let rec path_derivate hp hint =
let rec derivate_atoms hints hints' =
match hints, hints' with
- | gr :: grs, gr' :: grs' when eq_gr gr gr' -> derivate_atoms grs grs'
+ | gr :: grs, gr' :: grs' when GlobRef.equal gr gr' -> derivate_atoms grs grs'
| [], [] -> PathEpsilon
| [], hints -> PathEmpty
| grs, [] -> PathAtom (PathHints grs)
@@ -448,7 +472,7 @@ let subst_path_atom subst p =
| PathAny -> p
| PathHints grs ->
let gr' gr = fst (subst_global subst gr) in
- let grs' = List.smartmap gr' grs in
+ let grs' = List.Smart.map gr' grs in
if grs' == grs then p else PathHints grs'
let rec subst_hints_path subst hp =
@@ -474,28 +498,28 @@ module Hint_db :
sig
type t
val empty : ?name:hint_db_name -> transparent_state -> bool -> t
-val find : global_reference -> t -> search_entry
+val find : GlobRef.t -> t -> search_entry
val map_none : secvars:Id.Pred.t -> t -> full_hint list
-val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list
+val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
val map_existential : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
val map_eauto : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
val map_auto : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
val add_one : env -> evar_map -> hint_entry -> t -> t
val add_list : env -> evar_map -> hint_entry list -> t -> t
-val remove_one : global_reference -> t -> t
-val remove_list : global_reference list -> t -> t
-val iter : (global_reference option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
+val remove_one : GlobRef.t -> t -> t
+val remove_list : GlobRef.t list -> t -> t
+val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
val use_dn : t -> bool
val transparent_state : t -> transparent_state
val set_transparent_state : t -> transparent_state -> t
val add_cut : hints_path -> t -> t
-val add_mode : global_reference -> hint_mode array -> t -> t
+val add_mode : GlobRef.t -> hint_mode array -> t -> t
val cut : t -> hints_path
val unfolds : t -> Id.Set.t * Cset.t
-val fold : (global_reference option -> hint_mode array list -> full_hint list -> 'a -> 'a) ->
+val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) ->
t -> 'a -> 'a
end =
@@ -510,7 +534,7 @@ struct
hintdb_map : search_entry Constr_map.t;
(* A list of unindexed entries starting with an unfoldable constant
or with no associated pattern. *)
- hintdb_nopat : (global_reference option * stored_data) list;
+ hintdb_nopat : (GlobRef.t option * stored_data) list;
hintdb_name : string option;
}
@@ -654,7 +678,7 @@ struct
let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l
- let remove_sdl p sdl = List.smartfilter p sdl
+ let remove_sdl p sdl = List.filter p sdl
let remove_he st p se =
let sl1' = remove_sdl p se.sentry_nopat in
@@ -664,9 +688,9 @@ struct
let remove_list grs db =
let filter (_, h) =
- match h.name with PathHints [gr] -> not (List.mem_f eq_gr gr grs) | _ -> true in
+ match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in
let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
- let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
+ let hintnopat = List.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
{ db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
let remove_one gr db = remove_list [gr] db
@@ -792,7 +816,7 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
match EConstr.kind sigma cty with
| Prod _ -> failwith "make_exact_entry"
| _ ->
- let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr sigma cty) in
+ let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty) in
let hd =
try head_pattern_bound pat
with BoundPattern -> failwith "make_exact_entry"
@@ -814,12 +838,12 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c
let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
let ce = mk_clenv_from_env env sigma' None (c,cty) in
let c' = clenv_type (* ~reduce:false *) ce in
- let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma c') in
+ let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in
let hd =
try head_pattern_bound pat
with BoundPattern -> failwith "make_apply_entry" in
let miss = clenv_missing ce in
- let nmiss = List.length (clenv_missing ce) in
+ let nmiss = List.length miss in
let secvars = secvars_of_constr env sigma c in
let pri = match info.hint_priority with None -> nb_hyp sigma' cty + nmiss | Some p -> p in
let pat = match info.hint_pattern with
@@ -862,20 +886,6 @@ let pr_hint_term env sigma ctx = function
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
pr_econstr_env env sigma c
-(** We need an object to record the side-effect of registering
- global universes associated with a hint. *)
-let cache_context_set (_,c) =
- Global.push_context_set false c
-
-let input_context_set : Univ.ContextSet.t -> Libobject.obj =
- let open Libobject in
- declare_object
- { (default_object "Global universe context") with
- cache_function = cache_context_set;
- load_function = (fun _ -> cache_context_set);
- discharge_function = (fun (_,a) -> Some a);
- classify_function = (fun a -> Keep a) }
-
let warn_polymorphic_hint =
CWarnings.create ~name:"polymorphic-hint" ~category:"automation"
(fun hint -> strbrk"Using polymorphic hint " ++ hint ++
@@ -886,7 +896,7 @@ let fresh_global_or_constr env sigma poly cr =
let isgr, (c, ctx) =
match cr with
| IsGlobRef gr ->
- let (c, ctx) = Universes.fresh_global_instance env gr in
+ let (c, ctx) = UnivGen.fresh_global_instance env gr in
true, (EConstr.of_constr c, ctx)
| IsConstr (c, ctx) -> false, (c, ctx)
in
@@ -895,7 +905,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);
- Lib.add_anonymous_leaf (input_context_set ctx);
+ Declare.declare_universe_context false ctx;
(c, Univ.ContextSet.empty)
end
@@ -1005,15 +1015,19 @@ let add_hint dbname hintlist =
let db' = Hint_db.add_list env sigma hintlist db in
searchtable_add (dbname,db')
-let add_transparency dbname grs b =
+let add_transparency dbname target b =
let db = get_db dbname in
- let st = Hint_db.transparent_state db in
+ let (ids, csts as st) = Hint_db.transparent_state db in
let st' =
- List.fold_left (fun (ids, csts) gr ->
- match gr with
- | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts)
- | EvalVarRef v -> (if b then Id.Pred.add else Id.Pred.remove) v ids, csts)
- st grs
+ match target with
+ | HintsVariables -> (if b then Id.Pred.full else Id.Pred.empty), csts
+ | HintsConstants -> ids, if b then Cpred.full else Cpred.empty
+ | HintsReferences grs ->
+ List.fold_left (fun (ids, csts) gr ->
+ match gr with
+ | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts)
+ | EvalVarRef v -> (if b then Id.Pred.add else Id.Pred.remove) v ids, csts)
+ st grs
in searchtable_add (dbname, Hint_db.set_transparent_state db st')
let remove_hint dbname grs =
@@ -1023,11 +1037,11 @@ let remove_hint dbname grs =
type hint_action =
| CreateDB of bool * transparent_state
- | AddTransparency of evaluable_global_reference list * bool
+ | AddTransparency of evaluable_global_reference hints_transparency_target * bool
| AddHints of hint_entry list
- | RemoveHints of global_reference list
+ | RemoveHints of GlobRef.t list
| AddCut of hints_path
- | AddMode of global_reference * hint_mode array
+ | AddMode of GlobRef.t * hint_mode array
let add_cut dbname path =
let db = get_db dbname in
@@ -1075,8 +1089,8 @@ let subst_autohint (subst, obj) =
in if gr' == gr then gr else gr'
in
let subst_hint (k,data as hint) =
- let k' = Option.smartmap subst_key k in
- let pat' = Option.smartmap (subst_pattern subst) data.pat in
+ let k' = Option.Smart.map subst_key k in
+ let pat' = Option.Smart.map (subst_pattern subst) data.pat in
let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
let code' = match data.code.obj with
| Res_pf (c,t,ctx) ->
@@ -1113,14 +1127,22 @@ let subst_autohint (subst, obj) =
in
let action = match obj.hint_action with
| CreateDB _ -> obj.hint_action
- | AddTransparency (grs, b) ->
- let grs' = List.smartmap (subst_evaluable_reference subst) grs in
- if grs == grs' then obj.hint_action else AddTransparency (grs', b)
+ | AddTransparency (target, b) ->
+ let target' =
+ match target with
+ | HintsVariables -> target
+ | HintsConstants -> target
+ | HintsReferences grs ->
+ let grs' = List.Smart.map (subst_evaluable_reference subst) grs in
+ if grs == grs' then target
+ else HintsReferences grs'
+ in
+ if target' == target then obj.hint_action else AddTransparency (target', b)
| AddHints hintlist ->
- let hintlist' = List.smartmap subst_hint hintlist in
+ let hintlist' = List.Smart.map subst_hint hintlist in
if hintlist' == hintlist then obj.hint_action else AddHints hintlist'
| RemoveHints grs ->
- let grs' = List.smartmap (subst_global_reference subst) grs in
+ let grs' = List.Smart.map (subst_global_reference subst) grs in
if grs == grs' then obj.hint_action else RemoveHints grs'
| AddCut path ->
let path' = subst_hints_path subst path in
@@ -1228,15 +1250,15 @@ let add_trivials env sigma l local dbnames =
type hnf = bool
-type hint_info = (patvar list * constr_pattern) hint_info_gen
+type nonrec hint_info = hint_info
type hints_entry =
| HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
| HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
- | HintsTransparencyEntry of evaluable_global_reference list * bool
- | HintsModeEntry of global_reference * hint_mode list
+ | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
+ | HintsModeEntry of GlobRef.t * hint_mode list
| HintsExternEntry of hint_info * Genarg.glob_generic_argument
let default_prepare_hint_ident = Id.of_string "H"
@@ -1273,20 +1295,53 @@ let prepare_hint check (poly,local) env init (sigma,c) =
subst := (evar,mkVar id)::!subst;
mkNamedLambda id t (iter (replace_term sigma evar (mkVar id) c)) in
let c' = iter c in
- if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c';
+ let env = Global.env () in
+ let empty_sigma = Evd.from_env env in
+ if check then Pretyping.check_evars env empty_sigma sigma c';
let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
if poly then IsConstr (c', diff)
else if local then IsConstr (c', diff)
- else (Lib.add_anonymous_leaf (input_context_set diff);
+ else (Declare.declare_universe_context false diff;
IsConstr (c', Univ.ContextSet.empty))
+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 (Lazy.force coq_iff_ref) t in
+ let sign,ccl = decompose_prod_assum sigma t in
+ let (a,b) = match snd (decompose_app sigma ccl) with
+ | [a;b] -> (a,b)
+ | _ -> assert false in
+ let p =
+ if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
+ 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 (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
+ let id =
+ Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
+ in
+ let ctx = Evd.const_univ_entry ~poly sigma in
+ let c = EConstr.to_constr sigma c in
+ let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
+ let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
+ (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c))
+
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
- prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ prepare_hint true (poly,false) env sigma (evd,c) in
let fref r =
let gr = global_with_alias r in
Dumpglob.add_glob ?loc:r.CAst.loc gr;
@@ -1305,18 +1360,25 @@ let interp_hints poly =
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 (lhints, b) ->
- HintsTransparencyEntry (List.map fr lhints, b)
+ | 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_reference qid) "ind";
+ Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind";
List.init (nconstructors ind)
(fun i -> let c = (ind,i+1) in
let gr = ConstructRef c in
@@ -1325,14 +1387,14 @@ let interp_hints poly =
PathHints [gr], IsGlobRef gr)
in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
| HintsExtern (pri, patcom, tacexp) ->
- let pat = Option.map fp patcom in
+ 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 local dbnames0 h =
+let add_hints ~local dbnames0 h =
if String.List.mem "nocore" dbnames0 then
user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
@@ -1367,12 +1429,10 @@ let expand_constructor_hints env sigma lems =
(* builds a hint database from a constr signature *)
(* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
-let add_hint_lemmas env sigma eapply lems hint_db =
+let constructor_hints env sigma eapply lems =
let lems = expand_constructor_hints env sigma lems in
- let hintlist' =
- List.map_append (fun (poly, lem) ->
- make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems in
- Hint_db.add_list env sigma hintlist' hint_db
+ List.map_append (fun (poly, lem) ->
+ make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems
let make_local_hint_db env sigma ts eapply lems =
let map c = c env sigma in
@@ -1383,8 +1443,9 @@ let make_local_hint_db env sigma ts eapply lems =
| Some ts -> ts
in
let hintlist = List.map_append (make_resolve_hyp env sigma) sign in
- add_hint_lemmas env sigma eapply lems
- (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false))
+ Hint_db.empty ts false
+ |> Hint_db.add_list env sigma hintlist
+ |> Hint_db.add_list env sigma (constructor_hints env sigma eapply lems)
let make_local_hint_db env sigma ?ts eapply lems =
make_local_hint_db env sigma ts eapply lems
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 1811150c..9bf6c175 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -12,29 +12,29 @@ open Util
open Names
open EConstr
open Environ
-open Globnames
open Decl_kinds
open Evd
-open Misctypes
open Tactypes
open Clenv
open Pattern
-open Vernacexpr
+open Typeclasses
(** {6 General functions. } *)
exception Bound
-val decompose_app_bound : evar_map -> constr -> global_reference * constr array
+val decompose_app_bound : evar_map -> constr -> GlobRef.t * constr array
type debug = Debug | Info | Off
val secvars_of_hyps : ('c, 't) Context.Named.pt -> Id.Pred.t
-val empty_hint_info : 'a hint_info_gen
+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 *)
@@ -51,7 +51,7 @@ type 'a hints_path_atom_gen =
(* For forward hints, their names is the list of projections *)
| PathAny
-type hints_path_atom = global_reference hints_path_atom_gen
+type hints_path_atom = GlobRef.t hints_path_atom_gen
type hint_db_name = string
type 'a with_metadata = private {
@@ -72,6 +72,30 @@ 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 *)
+ | ModeOutput (* Anything *)
+
+type 'a hints_transparency_target =
+ | HintsVariables
+ | 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
@@ -80,8 +104,8 @@ type 'a hints_path_gen =
| PathEmpty
| PathEpsilon
-type pre_hints_path = Libnames.reference hints_path_gen
-type hints_path = global_reference hints_path_gen
+type pre_hints_path = Libnames.qualid hints_path_gen
+type hints_path = GlobRef.t hints_path_gen
val normalize_path : hints_path -> hints_path
val path_matches : hints_path -> hints_path_atom list -> bool
@@ -91,15 +115,15 @@ val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t
val pp_hints_path : hints_path -> Pp.t
val pp_hint_mode : hint_mode -> Pp.t
val glob_hints_path_atom :
- Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen
+ Libnames.qualid hints_path_atom_gen -> GlobRef.t hints_path_atom_gen
val glob_hints_path :
- Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen
+ Libnames.qualid hints_path_gen -> GlobRef.t hints_path_gen
module Hint_db :
sig
type t
val empty : ?name:hint_db_name -> transparent_state -> bool -> t
- val find : global_reference -> t -> search_entry
+ val find : GlobRef.t -> t -> search_entry
(** All hints which have no pattern.
* [secvars] represent the set of section variables that
@@ -107,27 +131,27 @@ module Hint_db :
val map_none : secvars:Id.Pred.t -> t -> full_hint list
(** All hints associated to the reference *)
- val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list
+ val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
(** All hints associated to the reference, respecting modes if evars appear in the
arguments, _not_ using the discrimination net. *)
val map_existential : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
(** All hints associated to the reference, respecting modes if evars appear in the
arguments and using the discrimination net. *)
- val map_eauto : evar_map -> secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list
+ val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list
(** All hints associated to the reference, respecting modes if evars appear in the
arguments. *)
val map_auto : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
val add_one : env -> evar_map -> hint_entry -> t -> t
val add_list : env -> evar_map -> hint_entry list -> t -> t
- val remove_one : global_reference -> t -> t
- val remove_list : global_reference list -> t -> t
- val iter : (global_reference option ->
+ val remove_one : GlobRef.t -> t -> t
+ val remove_list : GlobRef.t list -> t -> t
+ val iter : (GlobRef.t option ->
hint_mode array list -> full_hint list -> unit) -> t -> unit
val use_dn : t -> bool
@@ -144,10 +168,8 @@ type hint_db = Hint_db.t
type hnf = bool
-type hint_info = (patvar list * constr_pattern) hint_info_gen
-
type hint_term =
- | IsGlobRef of global_reference
+ | IsGlobRef of GlobRef.t
| IsConstr of constr * Univ.ContextSet.t
type hints_entry =
@@ -156,8 +178,8 @@ type hints_entry =
| HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
- | HintsTransparencyEntry of evaluable_global_reference list * bool
- | HintsModeEntry of global_reference * hint_mode list
+ | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
+ | HintsModeEntry of GlobRef.t * hint_mode list
| HintsExternEntry of hint_info * Genarg.glob_generic_argument
val searchtable_map : hint_db_name -> hint_db
@@ -171,7 +193,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit
val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit
-val remove_hints : bool -> hint_db_name list -> global_reference list -> unit
+val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit
val current_db_names : unit -> String.Set.t
@@ -179,7 +201,7 @@ val current_pure_db : unit -> hint_db list
val interp_hints : polymorphic -> hints_expr -> hints_entry
-val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
+val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit
val prepare_hint : bool (* Check no remaining evars *) ->
(bool * bool) (* polymorphic or monomorphic, local or global *) ->
@@ -264,7 +286,7 @@ val rewrite_db : hint_db_name
val pr_searchtable : env -> evar_map -> Pp.t
val pr_applicable_hint : unit -> Pp.t
-val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t
+val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
val pr_hint_db : Hint_db.t -> Pp.t
@@ -274,3 +296,5 @@ val pr_hint : env -> evar_map -> hint -> Pp.t
(** Hook for changing the initialization of auto *)
val add_hints_init : (unit -> unit) -> unit
+type nonrec hint_info = hint_info
+[@@ocaml.deprecated "Use [Typeclasses.hint_info]"]
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index b012a7ec..7da059ae 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -12,7 +12,7 @@ open Pp
open CErrors
open Util
open Names
-open Term
+open Constr
open Termops
open EConstr
open Inductiveops
@@ -263,7 +263,9 @@ open Evar_kinds
let mkPattern c = snd (Patternops.pattern_of_glob_constr c)
let mkGApp f args = DAst.make @@ GApp (f, args)
let mkGHole = DAst.make @@
- GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None)
+ GHole (QuestionMark {
+ Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Define false;
+ }, Namegen.IntroAnonymous, None)
let mkGProd id c1 c2 = DAst.make @@
GProd (Name (Id.of_string id), Explicit, c1, c2)
let mkGArrow c1 c2 = DAst.make @@
@@ -294,13 +296,13 @@ let match_with_equation env sigma t =
let (hdapp,args) = destApp sigma t in
match EConstr.kind sigma hdapp with
| Ind (ind,u) ->
- if eq_gr (IndRef ind) glob_eq then
+ if GlobRef.equal (IndRef ind) glob_eq then
Some (build_coq_eq_data()),hdapp,
PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if eq_gr (IndRef ind) glob_identity then
+ else if GlobRef.equal (IndRef ind) glob_identity then
Some (build_coq_identity_data()),hdapp,
PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if eq_gr (IndRef ind) glob_jmeq then
+ else if GlobRef.equal (IndRef ind) glob_jmeq then
Some (build_coq_jmeq_data()),hdapp,
HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
else
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 0697d0f1..f04cda12 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -144,7 +144,7 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool
(** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns
[t,u,T] and a boolean telling if equality is on the left side *)
-val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr
+val match_eqdec : Environ.env -> evar_map -> constr -> bool * GlobRef.t * constr * constr * constr
(** Match a negation *)
val is_matching_not : Environ.env -> evar_map -> constr -> bool
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 62ead57f..e4013152 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -53,7 +53,7 @@ let subst_one_scheme subst (ind,const) =
(subst_ind subst ind,subst_constant subst const)
let subst_scheme (subst,(kind,l)) =
- (kind,Array.map (subst_one_scheme subst) l)
+ (kind,Array.Smart.map (subst_one_scheme subst) l)
let discharge_scheme (_,(kind,l)) =
Some (kind,Array.map (fun (ind,const) ->
@@ -123,7 +123,7 @@ let define internal id c p univs =
let fd = declare_constant ~internal in
let id = compute_name internal id in
let ctx = UState.minimize univs in
- let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in
+ let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
let univs =
if p then Polymorphic_const_entry (UState.context ctx)
else Monomorphic_const_entry (UState.context_set ctx)
@@ -154,7 +154,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
| None -> add_suffix mib.mind_packets.(i).mind_typename suff in
let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in
declare_scheme kind [|ind,const|];
- const, Safe_typing.add_private
+ const, Safe_typing.concat_private
(Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff
let define_individual_scheme kind mode names (mind,i as ind) =
@@ -174,7 +174,7 @@ let define_mutual_scheme_base kind suff f mode names mind =
let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
declare_scheme kind schemes;
consts,
- Safe_typing.add_private
+ Safe_typing.concat_private
(Safe_typing.private_con_of_scheme
~kind (Global.safe_env()) (Array.to_list schemes))
eff
@@ -187,7 +187,7 @@ let define_mutual_scheme kind mode names mind =
let find_scheme_on_env_too kind ind =
let s = String.Map.find kind (Indmap.find ind !scheme_map) in
- s, Safe_typing.add_private
+ s, Safe_typing.concat_private
(Safe_typing.private_con_of_scheme
~kind (Global.safe_env()) [ind, s])
Safe_typing.empty_private_constants
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 067fc894..43786c8e 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -14,6 +14,7 @@ open Util
open Names
open Term
open Termops
+open Constr
open EConstr
open Vars
open Namegen
@@ -25,7 +26,7 @@ open Tacticals.New
open Tactics
open Elim
open Equality
-open Misctypes
+open Tactypes
open Proofview.Notations
module NamedDecl = Context.Named.Declaration
@@ -64,6 +65,11 @@ let var_occurs_in_pf gl id =
type inversion_status = Dep of constr option | NoDep
+type inversion_kind =
+ | SimpleInversion
+ | FullInversion
+ | FullInversionClear
+
let compute_eqn env sigma n i ai =
(mkRel (n-i),get_type_of env sigma (mkRel (n-i)))
@@ -88,7 +94,7 @@ let make_inv_predicate env evd indf realargs id status concl =
| Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*)
| None ->
let sort = get_sort_family_of env !evd concl in
- let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in
+ let sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd sort in
let p = make_arity env !evd true indf sort in
let evd',(p,ptyp) = Unification.abstract_list_all env
!evd p concl (realargs@[mkVar id])
@@ -119,12 +125,10 @@ let make_inv_predicate env evd indf realargs id status concl =
in
let eq_term = eqdata.Coqlib.eq in
let eq = Evarutil.evd_comb1 (Evd.fresh_global env) evd eq_term in
- let eq = EConstr.of_constr eq in
let eqn = applist (eq,[eqnty;lhs;rhs]) in
let eqns = (Anonymous, lift n eqn) :: eqns in
let refl_term = eqdata.Coqlib.refl in
let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in
- let refl_term = EConstr.of_constr refl_term in
let refl = mkApp (refl_term, [|eqnty; rhs|]) in
let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in
let args = refl :: args in
@@ -289,7 +293,7 @@ let error_too_many_names pats =
str "Unexpected " ++
str (String.plural (List.length pats) "introduction pattern") ++
str ": " ++ pr_enum (Miscprint.pr_intro_pattern
- (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++
+ (fun c -> Printer.pr_econstr_env env sigma (snd (c env (Evd.from_env env))))) pats ++
str ".")
let get_names (allow_conj,issimple) ({CAst.loc;v=pat} as x) = match pat with
@@ -328,7 +332,7 @@ let rec tclMAP_i allow_conj n tacfun = function
(tacfun (get_names allow_conj a))
(tclMAP_i allow_conj (n-1) tacfun l)
-let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
+let remember_first_eq id x = if !x == Logic.MoveLast then x := Logic.MoveAfter id
(* invariant: ProjectAndApply is responsible for erasing the clause
which it is given as input
@@ -371,7 +375,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
[if as_mode then clear [id] else tclIDTAC;
(tclMAP_i (false,false) neqns (function (idopt,_) ->
tclTRY (tclTHEN
- (intro_move_avoid idopt avoid MoveLast)
+ (intro_move_avoid idopt avoid Logic.MoveLast)
(* try again to substitute and if still not a variable after *)
(* decomposition, arbitrarily try to rewrite RL !? *)
(tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id))))))
@@ -400,7 +404,7 @@ let nLastDecls i tac =
let rewrite_equations as_mode othin neqns names ba =
Proofview.Goal.enter begin fun gl ->
let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
- let first_eq = ref MoveLast in
+ let first_eq = ref Logic.MoveLast in
let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in
match othin with
| Some thin ->
@@ -412,20 +416,20 @@ let rewrite_equations as_mode othin neqns names ba =
(nLastDecls neqns (fun ctx -> clear (ids_of_named_context ctx)));
tclMAP_i (true,false) neqns (fun (idopt,names) ->
(tclTHEN
- (intro_move_avoid idopt avoid MoveLast)
+ (intro_move_avoid idopt avoid Logic.MoveLast)
(onLastHypId (fun id ->
tclTRY (projectAndApply as_mode thin avoid id first_eq names depids)))))
names;
tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *)
let idopt = if as_mode then Some (NamedDecl.get_id d) else None in
- intro_move idopt (if thin then MoveLast else !first_eq))
+ intro_move idopt (if thin then Logic.MoveLast else !first_eq))
nodepids;
(tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)]
| None ->
(* simple inversion *)
if as_mode then
tclMAP_i (false,true) neqns (fun (idopt,_) ->
- intro_move idopt MoveLast) names
+ intro_move idopt Logic.MoveLast) names
else
(tclTHENLIST
[tclDO neqns intro;
@@ -465,7 +469,7 @@ let raw_inversion inv_kind id status names =
make_inv_predicate env evdref indf realargs id status concl in
let sigma = !evdref in
let (cut_concl,case_tac) =
- if status != NoDep && (dependent sigma c concl) then
+ if status != NoDep && (local_occur_var sigma id concl) then
Reductionops.beta_applist sigma (elim_predicate, realargs@[c]),
case_then_using
else
@@ -491,11 +495,12 @@ let raw_inversion inv_kind id status names =
(* Error messages of the inversion tactics *)
let wrap_inv_error id = function (e, info) -> match e with
| Indrec.RecursionSchemeError
- (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) ->
+ (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Set as k),i)) ->
Proofview.tclENV >>= fun env ->
+ Proofview.tclEVARMAP >>= fun sigma ->
tclZEROMSG (
(strbrk "Inversion would require case analysis on sort " ++
- pr_sort Evd.empty k ++
+ pr_sort sigma k ++
strbrk " which is not allowed for inductive definition " ++
pr_inductive env (fst i) ++ str "."))
| e -> Proofview.tclZERO ~info e
diff --git a/tactics/inv.mli b/tactics/inv.mli
index c63d57af..bbd1f335 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -10,11 +10,15 @@
open Names
open EConstr
-open Misctypes
open Tactypes
type inversion_status = Dep of constr option | NoDep
+type inversion_kind =
+ | SimpleInversion
+ | FullInversion
+ | FullInversionClear
+
val inv_clause :
inversion_kind -> or_and_intro_pattern option -> Id.t list ->
quantified_hypothesis -> unit Proofview.tactic
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index a4cdc159..caf4c1ec 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -12,9 +12,9 @@ open Pp
open CErrors
open Util
open Names
-open Term
open Termops
open Environ
+open Constr
open EConstr
open Vars
open Namegen
@@ -232,9 +232,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let c = fill_holes pfterm in
(* warning: side-effect on ownSign *)
let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
- let invProof = EConstr.Unsafe.to_constr invProof in
- let p = Evarutil.nf_evars_universes sigma invProof in
- p, sigma
+ 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 env sigma t sort dep inv_op in
@@ -252,7 +251,7 @@ 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 env sigma com in
- let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort 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
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 2337a790..f42e5a8b 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -11,7 +11,7 @@
open Names
open EConstr
open Constrexpr
-open Misctypes
+open Tactypes
val lemInv_clause :
quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 958a205a..596feeec 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -159,8 +159,6 @@ type branch_assumptions = {
ba : branch_args; (* the branch args *)
assums : named_context} (* the list of assumptions introduced *)
-open Misctypes
-
let fix_empty_or_and_pattern nv l =
(* 1- The syntax does not distinguish between "[ ]" for one clause with no
names and "[ ]" for no clause at all *)
@@ -194,7 +192,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns =
if not (Int.equal p p1 || Int.equal p p2) then err1 p1 p2;
if Int.equal p p1 then
IntroAndPattern
- (List.extend branchsigns.(0) (CAst.make @@ IntroNaming IntroAnonymous) l)
+ (List.extend branchsigns.(0) (CAst.make @@ IntroNaming Namegen.IntroAnonymous) l)
else
names
else
@@ -225,7 +223,7 @@ let compute_induction_names_gen check_and branchletsigns = function
let compute_induction_names = compute_induction_names_gen true
(* Compute the let-in signature of case analysis or standard induction scheme *)
-let compute_constructor_signatures isrec ((_,k as ity),u) =
+let compute_constructor_signatures ~rec_flag ((_,k as ity),u) =
let rec analrec c recargs =
match Constr.kind c, recargs with
| Prod (_,_,c), recarg::rest ->
@@ -233,7 +231,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) =
begin match Declareops.dest_recarg recarg with
| Norec | Imbr _ -> true :: rest
| Mrec (_,j) ->
- if isrec && Int.equal j k then true :: true :: rest
+ if rec_flag && Int.equal j k then true :: true :: rest
else true :: rest
end
| LetIn (_,_,_,c), rest -> false :: analrec c rest
@@ -263,7 +261,7 @@ let pf_with_evars glsev k gls =
tclTHEN (Refiner.tclEVARS evd) (k a) gls
let pf_constr_of_global gr k =
- pf_with_evars (fun gls -> on_snd EConstr.of_constr (pf_apply Evd.fresh_global gls gr)) k
+ pf_with_evars (fun gls -> pf_apply Evd.fresh_global gls gr) k
(** Tacticals of Ltac defined directly in term of Proofview *)
module New = struct
@@ -369,9 +367,36 @@ module New = struct
tclTHENSFIRSTn t1 l (tclUNIT())
let tclTHENFIRST t1 t2 =
tclTHENFIRSTn t1 [|t2|]
+
+ let tclBINDFIRST t1 t2 =
+ t1 >>= fun ans ->
+ Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+ match gls with
+ | [] -> tclFAIL 0 (str "Expect at least one goal.")
+ | hd::tl ->
+ Proofview.Unsafe.tclSETGOALS [hd] <*> t2 ans >>= fun ans ->
+ Proofview.Unsafe.tclNEWGOALS tl <*>
+ Proofview.tclUNIT ans
+
let tclTHENLASTn t1 l =
tclTHENS3PARTS t1 [||] (tclUNIT()) l
let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|]
+
+ let option_of_failure f x = try Some (f x) with Failure _ -> None
+
+ let tclBINDLAST t1 t2 =
+ t1 >>= fun ans ->
+ Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+ match option_of_failure List.sep_last gls with
+ | None -> tclFAIL 0 (str "Expect at least one goal.")
+ | Some (last,firstn) ->
+ Proofview.Unsafe.tclSETGOALS [last] <*> t2 ans >>= fun ans ->
+ Proofview.Unsafe.tclGETGOALS >>= fun newgls ->
+ tclEVARMAP >>= fun sigma ->
+ let firstn = Proofview.Unsafe.undefined sigma firstn in
+ Proofview.Unsafe.tclSETGOALS (firstn@newgls) <*>
+ Proofview.tclUNIT ans
+
let tclTHENS t l =
tclINDEPENDENT begin
t <*>Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *)
@@ -465,11 +490,13 @@ module New = struct
Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t)
(* Select a subset of the goals *)
- let tclSELECT = function
- | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i
- | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l
- | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id
- | Vernacexpr.SelectAll -> fun tac -> tac
+ let tclSELECT = let open Goal_select in function
+ | SelectNth i -> Proofview.tclFOCUS i i
+ | SelectList l -> Proofview.tclFOCUSLIST l
+ | SelectId id -> Proofview.tclFOCUSID id
+ | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here")
+ | SelectAlreadyFocused ->
+ anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here")
(* Check that holes in arguments have been resolved *)
@@ -479,8 +506,8 @@ module New = struct
let evi = Evd.find sigma evk in
match Evd.evar_body evi with
| Evd.Evar_empty -> Some (evk,evi)
- | Evd.Evar_defined c -> match Constr.kind c with
- | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
+ | Evd.Evar_defined c -> match Constr.kind (EConstr.Unsafe.to_constr c) with
+ | Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
| _ ->
(* We make the assumption that there is no way to refine an
evar remaining after typing from the initial term given to
@@ -607,7 +634,7 @@ module New = struct
(* Find the right elimination suffix corresponding to the sort of the goal *)
(* c should be of type A1->.. An->B with B an inductive definition *)
let general_elim_then_using mk_elim
- isrec allnames tac predicate ind (c, t) =
+ rec_flag allnames tac predicate ind (c, t) =
Proofview.Goal.enter begin fun gl ->
let sigma, elim = mk_elim ind gl in
let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
@@ -628,15 +655,14 @@ module New = struct
| _ ->
let name_elim =
match EConstr.kind sigma elim with
- | Const (kn, _) -> Constant.to_string kn
- | Var id -> Id.to_string id
- | _ -> "\b"
+ | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim
+ | _ -> mt ()
in
user_err ~hdr:"Tacticals.general_elim_then_using"
- (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
+ (str "The elimination combinator " ++ name_elim ++ str " is unknown.")
in
let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
- let branchsigns = compute_constructor_signatures isrec ind in
+ let branchsigns = compute_constructor_signatures ~rec_flag ind in
let brnames = compute_induction_names_gen false branchsigns allnames in
let flags = Unification.elim_flags () in
let elimclause' =
@@ -659,7 +685,7 @@ module New = struct
in
let branchtacs = List.init (Array.length branchsigns) after_tac in
Proofview.tclTHEN
- (Clenvtac.clenv_refine false clenv')
+ (Clenvtac.clenv_refine clenv')
(Proofview.tclEXTEND [] tclIDTAC branchtacs)
end) end
@@ -682,7 +708,7 @@ module New = struct
let gl_make_elim ind = begin fun gl ->
let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
let (sigma, c) = pf_apply Evd.fresh_global gl gr in
- (sigma, EConstr.of_constr c)
+ (sigma, c)
end
let gl_make_case_dep (ind, u) = begin fun gl ->
@@ -726,8 +752,8 @@ module New = struct
let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
let isrec,mkelim =
match (Global.lookup_mind (fst (fst ind))).mind_record with
- | None -> true,gl_make_elim
- | Some _ -> false,gl_make_case_dep
+ | NotRecord -> true,gl_make_elim
+ | FakeRecord | PrimRecord _ -> false,gl_make_case_dep
in
general_elim_then_using mkelim isrec None tac None ind (c, t)
end
@@ -742,7 +768,6 @@ module New = struct
Proofview.tclEVARMAP >>= fun sigma ->
Proofview.tclENV >>= fun env ->
let (sigma, c) = Evd.fresh_global env sigma ref in
- let c = EConstr.of_constr c in
Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c
end
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index f0ebac78..1e66c2b0 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -14,7 +14,6 @@ open EConstr
open Evd
open Proof_type
open Locus
-open Misctypes
open Tactypes
(** Tacticals i.e. functions from tactics to tactics. *)
@@ -124,7 +123,7 @@ val fix_empty_or_and_pattern : int ->
delayed_open_constr or_and_intro_pattern_expr ->
delayed_open_constr or_and_intro_pattern_expr
-val compute_constructor_signatures : rec_flag -> inductive * 'a -> bool list array
+val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool list array
(** Useful for [as intro_pattern] modifier *)
val compute_induction_names :
@@ -135,7 +134,7 @@ val elimination_sort_of_hyp : Id.t -> goal sigma -> Sorts.family
val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family
val pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
-val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
+val pf_constr_of_global : GlobRef.t -> (constr -> tactic) -> tactic
(** Tacticals defined directly in term of Proofview *)
@@ -196,8 +195,10 @@ module New : sig
(** [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
+ val tclBINDFIRST : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
val tclTHENLASTn : unit tactic -> unit tactic array -> unit tactic
val tclTHENLAST : unit tactic -> unit tactic -> unit tactic
+ val tclBINDLAST : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
(* [tclTHENS t l = t <*> tclDISPATCH l] *)
val tclTHENS : unit tactic -> unit tactic list -> unit tactic
(* [tclTHENLIST [t1;…;tn]] is [t1<*>…<*>tn] *)
@@ -221,7 +222,7 @@ module New : sig
val tclCOMPLETE : 'a tactic -> 'a tactic
val tclSOLVE : unit tactic list -> unit tactic
val tclPROGRESS : unit tactic -> unit tactic
- val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic
+ val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic
val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic
@@ -266,5 +267,5 @@ module New : sig
val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
- val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic
+ val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic
end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index dfdd3237..f060e494 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -43,7 +43,7 @@ open Pretype_errors
open Unification
open Locus
open Locusops
-open Misctypes
+open Tactypes
open Proofview.Notations
open Context.Named.Declaration
@@ -128,14 +128,14 @@ let unsafe_intro env store decl b =
(sigma, mkNamedLambda_or_LetIn decl ev)
end
-let introduction ?(check=true) id =
+let introduction id =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
let hyps = named_context_val (Proofview.Goal.env gl) in
let store = Proofview.Goal.extra gl in
let env = Proofview.Goal.env gl in
- let () = if check && mem_named_context_val id hyps then
+ let () = if mem_named_context_val id hyps then
user_err ~hdr:"Tactics.introduction"
(str "Variable " ++ Id.print id ++ str " is already declared.")
in
@@ -158,9 +158,9 @@ let convert_concl ?(check=true) ty k =
let sigma =
if check then begin
ignore (Typing.unsafe_type_of env sigma ty);
- let sigma,b = Reductionops.infer_conv env sigma ty conclty in
- if not b then error "Not convertible.";
- sigma
+ match Reductionops.infer_conv env sigma ty conclty with
+ | None -> error "Not convertible."
+ | Some sigma -> sigma
end else sigma in
let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in
let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
@@ -186,11 +186,10 @@ let convert_hyp_no_check = convert_hyp ~check:false
let convert_gen pb x y =
Proofview.Goal.enter begin fun gl ->
- try
- let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in
- if b then Proofview.Unsafe.tclEVARS sigma
- else Tacticals.New.tclFAIL 0 (str "Not convertible")
- with (* Reduction.NotConvertible *) _ ->
+ match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with
+ | Some sigma -> Proofview.Unsafe.tclEVARS sigma
+ | None -> Tacticals.New.tclFAIL 0 (str "Not convertible")
+ | exception _ ->
(** FIXME: Sometimes an anomaly is raised from conversion *)
Tacticals.New.tclFAIL 0 (str "Not convertible")
end
@@ -198,32 +197,46 @@ end
let convert x y = convert_gen Reduction.CONV x y
let convert_leq x y = convert_gen Reduction.CUMUL x y
-let clear_dependency_msg env sigma id = function
+let clear_in_global_msg = function
+ | None -> mt ()
+ | Some ref -> str " implicitly in " ++ Printer.pr_global ref
+
+let clear_dependency_msg env sigma id err inglobal =
+ let pp = clear_in_global_msg inglobal in
+ match err with
| Evarutil.OccurHypInSimpleClause None ->
- Id.print id ++ str " is used in conclusion."
+ Id.print id ++ str " is used" ++ pp ++ str " in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
- Id.print id ++ strbrk " is used in hypothesis " ++ Id.print id' ++ str"."
+ Id.print id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
str "Cannot remove " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
+ | Evarutil.NoCandidatesLeft ev ->
+ str "Cannot remove " ++ Id.print id ++ str " as it would leave the existential " ++
+ Printer.pr_existential_key sigma ev ++ str" without candidates."
-let error_clear_dependency env sigma id err =
- user_err (clear_dependency_msg env sigma id err)
+let error_clear_dependency env sigma id err inglobal =
+ user_err (clear_dependency_msg env sigma id err inglobal)
-let replacing_dependency_msg env sigma id = function
+let replacing_dependency_msg env sigma id err inglobal =
+ let pp = clear_in_global_msg inglobal in
+ match err with
| Evarutil.OccurHypInSimpleClause None ->
- str "Cannot change " ++ Id.print id ++ str ", it is used in conclusion."
+ str "Cannot change " ++ Id.print id ++ str ", it is used" ++ pp ++ str " in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
str "Cannot change " ++ Id.print id ++
- strbrk ", it is used in hypothesis " ++ Id.print id' ++ str"."
+ strbrk ", it is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
str "Cannot change " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
+ | Evarutil.NoCandidatesLeft ev ->
+ str "Cannot change " ++ Id.print id ++ str " as it would leave the existential " ++
+ Printer.pr_existential_key sigma ev ++ str" without candidates."
-let error_replacing_dependency env sigma id err =
- user_err (replacing_dependency_msg env sigma id err)
+let error_replacing_dependency env sigma id err inglobal =
+ user_err (replacing_dependency_msg env sigma id err inglobal)
(* This tactic enables the user to remove hypotheses from the signature.
* Some care is taken to prevent him from removing variables that are
@@ -239,13 +252,12 @@ let clear_gen fail = function
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
- let evdref = ref sigma in
- let (hyps, concl) =
- try clear_hyps_in_evi env evdref (named_context_val env) concl ids
- with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err
+ let (sigma, hyps, concl) =
+ try clear_hyps_in_evi env sigma (named_context_val env) concl ids
+ with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal
in
let env = reset_with_named_context hyps env in
- Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Refine.refine ~typecheck:false begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true concl
end)
@@ -423,11 +435,10 @@ let get_previous_hyp_position env sigma id =
let clear_hyps2 env sigma ids sign t cl =
try
- let evdref = ref (Evd.clear_metas sigma) in
- let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
- (hyps, t, cl, !evdref)
- with Evarutil.ClearDependencyError (id,err) ->
- error_replacing_dependency env sigma id err
+ let sigma = Evd.clear_metas sigma in
+ Evarutil.clear_hyps2_in_evi env sigma sign t cl ids
+ with Evarutil.ClearDependencyError (id,err,inglobal) ->
+ error_replacing_dependency env sigma id err inglobal
let internal_cut_gen ?(check=true) dir replace id t =
Proofview.Goal.enter begin fun gl ->
@@ -439,7 +450,7 @@ let internal_cut_gen ?(check=true) dir replace id t =
let sign',t,concl,sigma =
if replace then
let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in
- let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
+ let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in
sign',t,concl,sigma
else
@@ -557,20 +568,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
end
end
-let warning_nameless_fix =
- CWarnings.create ~name:"nameless-fix" ~category:"deprecated" Pp.(fun () ->
- str "fix/cofix without a name are deprecated, please use the named version.")
-
-let fix ido n = match ido with
- | None ->
- warning_nameless_fix ();
- Proofview.Goal.enter begin fun gl ->
- let name = Proof_global.get_current_proof_name () in
- let id = new_fresh_id Id.Set.empty name gl in
- mutual_fix id n [] 0
- end
- | Some id ->
- mutual_fix id n [] 0
+let fix id n = mutual_fix id n [] 0
let rec check_is_mutcoind env sigma cl =
let b = whd_all env sigma cl in
@@ -613,16 +611,7 @@ let mutual_cofix f others j = Proofview.Goal.enter begin fun gl ->
end
end
-let cofix ido = match ido with
- | None ->
- warning_nameless_fix ();
- Proofview.Goal.enter begin fun gl ->
- let name = Proof_global.get_current_proof_name () in
- let id = new_fresh_id Id.Set.empty name gl in
- mutual_cofix id [] 0
- end
- | Some id ->
- mutual_cofix id [] 0
+let cofix id = mutual_cofix id [] 0
(**************************************************************)
(* Reduction and conversion tactics *)
@@ -802,9 +791,9 @@ let e_change_in_hyp redfun (id,where) =
(convert_hyp c)
end
-type change_arg = Ltac_pretype.patvar_map -> evar_map -> evar_map * EConstr.constr
+type change_arg = Ltac_pretype.patvar_map -> env -> evar_map -> evar_map * EConstr.constr
-let make_change_arg c pats sigma = (sigma, replace_vars (Id.Map.bindings pats) c)
+let make_change_arg c pats env sigma = (sigma, replace_vars (Id.Map.bindings pats) c)
let check_types env sigma mayneedglobalcheck deep newc origc =
let t1 = Retyping.get_type_of env sigma newc in
@@ -812,15 +801,15 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
let t2 = Retyping.get_type_of env sigma origc in
let sigma, t2 = Evarsolve.refresh_universes
~onlyalg:true (Some false) env sigma t2 in
- let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in
- if not b then
+ match infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 with
+ | None ->
if
isSort sigma (whd_all env sigma t1) &&
isSort sigma (whd_all env sigma t2)
then (mayneedglobalcheck := true; sigma)
else
user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.")
- else sigma
+ | Some sigma -> sigma
end
else
if not (isSort sigma (whd_all env sigma t1)) then
@@ -829,11 +818,11 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
(* Now we introduce different instances of the previous tacticals *)
let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
- let (sigma, t') = t sigma in
+ let (sigma, t') = t env sigma in
let sigma = check_types env sigma mayneedglobalcheck deep t' c in
- let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
- if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
- (sigma, t')
+ match infer_conv ~pb:cv_pb env sigma t' c with
+ | None -> user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
+ | Some sigma -> (sigma, t')
(* Use cumulativity only if changing the conclusion not a subterm *)
let change_on_subterm cv_pb deep t where env sigma c =
@@ -971,6 +960,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
| LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) ->
let name = find_name false (LocalDef (name,b,t)) name_flag gl in
build_intro_tac name move_flag tac
+ | Evar ev when force_flag ->
+ let sigma, t = Evardefine.define_evar_as_product sigma ev in
+ Tacticals.New.tclTHEN
+ (Proofview.Unsafe.tclEVARS sigma)
+ (intro_then_gen name_flag move_flag force_flag dep_flag tac)
| _ ->
begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct))
(* Note: red_in_concl includes betaiotazeta and this was like *)
@@ -1108,7 +1102,13 @@ let msg_quantified_hypothesis = function
pr_nth n ++
str " non dependent hypothesis"
+let warn_deprecated_intros_until_0 =
+ CWarnings.create ~name:"deprecated-intros-until-0" ~category:"tactics"
+ (fun () ->
+ strbrk"\"intros until 0\" is deprecated, use \"intros *\"; instead of \"induction 0\" and \"destruct 0\" use explicitly a name.\"")
+
let depth_of_quantified_hypothesis red h gl =
+ if h = AnonHyp 0 then warn_deprecated_intros_until_0 ();
match lookup_hypothesis_as_renamed_gen red h gl with
| Some depth -> depth
| None ->
@@ -1159,6 +1159,18 @@ let tactic_infer_flags with_evar = {
Pretyping.fail_evar = not with_evar;
Pretyping.expand_evars = true }
+type evars_flag = bool (* true = pose evars false = fail on evars *)
+type rec_flag = bool (* true = recursive false = not recursive *)
+type advanced_flag = bool (* true = advanced false = basic *)
+type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
+type 'a core_destruction_arg =
+ | ElimOnConstr of 'a
+ | ElimOnIdent of lident
+ | ElimOnAnonHyp of int
+
+type 'a destruction_arg =
+ clear_flag * 'a core_destruction_arg
let onOpenInductionArg env sigma tac = function
| clear_flag,ElimOnConstr f ->
@@ -1251,7 +1263,6 @@ let cut c =
end
let error_uninstantiated_metas t clenv =
- let t = EConstr.Unsafe.to_constr t in
let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta.")
in user_err (str "Cannot find an instance for " ++ Id.print id ++ str".")
@@ -1261,7 +1272,7 @@ let check_unresolved_evars_of_metas sigma clenv =
(* Refiner.pose_all_metas_as_evars are resolved *)
List.iter (fun (mv,b) -> match b with
| Clval (_,(c,_),_) ->
- (match Constr.kind c.rebus with
+ (match Constr.kind (EConstr.Unsafe.to_constr c.rebus) with
| Evar (evk,_) when Evd.is_undefined clenv.evd evk
&& not (Evd.mem sigma evk) ->
error_uninstantiated_metas (mkMeta mv) clenv
@@ -1281,7 +1292,7 @@ let do_replace id = function
let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
targetid id sigma0 clenv tac =
- let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in
+ let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in
let clenv =
if with_classes then
{ clenv with evd = Typeclasses.resolve_typeclasses
@@ -1438,9 +1449,7 @@ let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations
let find_ind_eliminator ind s gl =
let gr = lookup_eliminator ind s in
- let evd, c = Tacmach.New.pf_apply Evd.fresh_global gl gr in
- let c = EConstr.of_constr c in
- evd, c
+ Tacmach.New.pf_apply Evd.fresh_global gl gr
let find_eliminator c gl =
let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
@@ -1572,9 +1581,10 @@ let make_projection env sigma params cstr sign elim i n c u =
| Some proj ->
let args = Context.Rel.to_extended_vect mkRel 0 sign in
let proj =
- if Environ.is_projection proj env then
+ match Recordops.find_primitive_projection proj with
+ | Some proj ->
mkProj (Projection.make proj false, mkApp (c, args))
- else
+ | None ->
mkApp (mkConstU (proj,u), Array.append (Array.of_list params)
[|mkApp (c, args)|])
in
@@ -1639,13 +1649,11 @@ let tclORELSEOPT t k =
Proofview.tclZERO ~info e
| Some tac -> tac)
-let general_apply with_delta with_destruct with_evars clear_flag
- {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} =
+let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
+ clear_flag {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
- let flags =
- if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
(* The actual type of the theorem. It will be matched against the
goal. If this fails, then the head constant will be unfolded step by
step. *)
@@ -1654,7 +1662,12 @@ let general_apply with_delta with_destruct with_evars clear_flag
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
-
+ let ts =
+ if respect_opaque then Conv_oracle.get_transp_state (oracle env)
+ else full_transparent_state
+ in
+ let flags =
+ if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
let thm_ty0 = nf_betaiota env sigma (Retyping.get_type_of env sigma c) in
let try_apply thm_ty nprod =
try
@@ -1720,14 +1733,14 @@ let rec apply_with_bindings_gen b e = function
(general_apply b b e k cb)
(apply_with_bindings_gen b e cbl)
-let apply_with_delayed_bindings_gen b e l =
+let apply_with_delayed_bindings_gen b e l =
let one k {CAst.loc;v=f} =
Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let (sigma, cb) = f env sigma in
Tacticals.New.tclWITHHOLES e
- (general_apply b b e k CAst.(make ?loc cb)) sigma
+ (general_apply ~respect_opaque:(not b) b b e k CAst.(make ?loc cb)) sigma
end
in
let rec aux = function
@@ -1802,14 +1815,12 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
in
aux (make_clenv_binding env sigma (d,thm) lbind)
-let apply_in_once sidecond_first with_delta with_destruct with_evars naming
- id (clear_flag,{ CAst.loc; v= d,lbind}) tac =
+let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
+ with_destruct with_evars naming id (clear_flag,{ CAst.loc; v= d,lbind}) tac =
let open Context.Rel.Declaration in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
- let flags =
- if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
let t' = Tacmach.New.pf_get_hyp_typ id gl in
let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in
@@ -1817,6 +1828,12 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
+ let ts =
+ if respect_opaque then Conv_oracle.get_transp_state (oracle env)
+ else full_transparent_state
+ in
+ let flags =
+ if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
try
let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in
clenv_refine_in ~sidecond_first with_evars targetid id sigma clause
@@ -1836,14 +1853,14 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
aux [] with_destruct d
end
-let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming
- id (clear_flag,{CAst.loc;v=f}) tac =
+let apply_in_delayed_once ?(respect_opaque = false) sidecond_first with_delta
+ with_destruct with_evars naming id (clear_flag,{CAst.loc;v=f}) tac =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let (sigma, c) = f env sigma in
Tacticals.New.tclWITHHOLES with_evars
- (apply_in_once sidecond_first with_delta with_destruct with_evars
+ (apply_in_once ~respect_opaque sidecond_first with_delta with_destruct with_evars
naming id (clear_flag,CAst.(make ?loc c)) tac)
sigma
end
@@ -1911,8 +1928,8 @@ let cast_no_check cast c =
exact_no_check (mkCast (c, cast, concl))
end
-let vm_cast_no_check c = cast_no_check Term.VMcast c
-let native_cast_no_check c = cast_no_check Term.NATIVEcast c
+let vm_cast_no_check c = cast_no_check VMcast c
+let native_cast_no_check c = cast_no_check NATIVEcast c
let exact_proof c =
let open Tacmach.New in
@@ -1935,16 +1952,19 @@ let assumption =
let t = NamedDecl.get_type decl in
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
- let (sigma, is_same_type) =
- if only_eq then (sigma, EConstr.eq_constr sigma t concl)
+ let ans =
+ if only_eq then
+ if EConstr.eq_constr sigma t concl then Some sigma
+ else None
else
let env = Proofview.Goal.env gl in
infer_conv env sigma t concl
in
- if is_same_type then
+ match ans with
+ | Some sigma ->
(Proofview.Unsafe.tclEVARS sigma) <*>
exact_no_check (mkVar (NamedDecl.get_id decl))
- else arec gl only_eq rest
+ | None -> arec gl only_eq rest
in
let assumption_tac gl =
let hyps = Proofview.Goal.hyps gl in
@@ -1964,24 +1984,22 @@ let on_the_bodies = function
exception DependsOnBody of Id.t option
let check_is_type env sigma ty =
- let evdref = ref sigma in
try
- let _ = Typing.e_sort_of env evdref ty in
- !evdref
+ let sigma, _ = Typing.sort_of env sigma ty in
+ sigma
with e when CErrors.noncritical e ->
raise (DependsOnBody None)
let check_decl env sigma decl =
let open Context.Named.Declaration in
let ty = NamedDecl.get_type decl in
- let evdref = ref sigma in
try
- let _ = Typing.e_sort_of env evdref ty in
- let _ = match decl with
- | LocalAssum _ -> ()
- | LocalDef (_,c,_) -> Typing.e_check env evdref c ty
+ let sigma, _ = Typing.sort_of env sigma ty in
+ let sigma = match decl with
+ | LocalAssum _ -> sigma
+ | LocalDef (_,c,_) -> Typing.check env sigma c ty
in
- !evdref
+ sigma
with e when CErrors.noncritical e ->
let id = NamedDecl.get_id decl in
raise (DependsOnBody (Some id))
@@ -2252,7 +2270,7 @@ let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
let c = mkVar id in
let t = Tacmach.New.pf_unsafe_type_of gl c in
let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
- let branchsigns = compute_constructor_signatures false ind in
+ let branchsigns = compute_constructor_signatures ~rec_flag:false ind in
let nv_with_let = Array.map List.length branchsigns in
let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
let ll = get_and_check_or_and_pattern ?loc ll branchsigns in
@@ -2532,11 +2550,11 @@ let assert_as first hd ipat t =
(* apply in as *)
-let general_apply_in sidecond_first with_delta with_destruct with_evars
- id lemmas ipat =
+let general_apply_in ?(respect_opaque=false) sidecond_first with_delta
+ with_destruct with_evars id lemmas ipat =
let tac (naming,lemma) tac id =
- apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
- naming id lemma tac in
+ apply_in_delayed_once ~respect_opaque sidecond_first with_delta
+ with_destruct with_evars naming id lemma tac in
Proofview.Goal.enter begin fun gl ->
let destopt =
if with_evars then MoveLast (* evars would depend on the whole context *)
@@ -2567,7 +2585,7 @@ let apply_in simple with_evars id lemmas ipat =
general_apply_in false simple simple with_evars id lemmas ipat
let apply_delayed_in simple with_evars id lemmas ipat =
- general_apply_in false simple simple with_evars id lemmas ipat
+ general_apply_in ~respect_opaque:true false simple simple with_evars id lemmas ipat
(*****************************)
(* Tactics abstracting terms *)
@@ -2605,9 +2623,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
let eqdata = build_coq_eq_data () in
let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in
- let eq = EConstr.of_constr eq in
let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in
- let refl = EConstr.of_constr refl in
let eq = applist (eq,args) in
let refl = applist (refl, [t;mkVar id]) in
let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in
@@ -2663,9 +2679,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
let eqdata = build_coq_eq_data () in
let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in
- let eq = EConstr.of_constr eq in
let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in
- let refl = EConstr.of_constr refl in
let eq = applist (eq,args) in
let refl = applist (refl, [t;mkVar id]) in
let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in
@@ -3003,8 +3017,24 @@ let unfold_body x =
end
end
+let warn_cannot_remove_as_expected =
+ CWarnings.create ~name:"cannot-remove-as-expected" ~category:"tactics"
+ (fun (id,inglobal) ->
+ let pp = match inglobal with
+ | None -> mt ()
+ | Some ref -> str ", it is used implicitly in " ++ Printer.pr_global ref in
+ str "Cannot remove " ++ Id.print id ++ pp ++ str ".")
+
+let clear_for_destruct ids =
+ Proofview.tclORELSE
+ (clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids)
+ (function
+ | ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT ()
+ | e -> iraise e)
+
(* Either unfold and clear if defined or simply clear if not a definition *)
-let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
+let expand_hyp id =
+ Tacticals.New.tclTRY (unfold_body id) <*> clear_for_destruct [id]
(*****************************)
(* High-level induction *)
@@ -3420,7 +3450,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma =
type elim_scheme = {
elimc: constr with_bindings option;
elimt: types;
- indref: global_reference option;
+ indref: GlobRef.t option;
params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
nparams: int; (* number of parameters *)
predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
@@ -3782,7 +3812,10 @@ let specialize_eqs id =
let ty = Tacmach.New.pf_get_hyp_typ id gl in
let evars = ref (Proofview.Goal.sigma gl) in
let unif env evars c1 c2 =
- compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2
+ compare_upto_variables !evars c1 c2 &&
+ (match Evarconv.conv env !evars c1 c2 with
+ | Some sigma -> evars := sigma; true
+ | None -> false)
in
let rec aux in_eqs ctx acc ty =
match EConstr.kind !evars ty with
@@ -3807,7 +3840,8 @@ let specialize_eqs id =
| _ ->
if in_eqs then acc, in_eqs, ctx, ty
else
- let e = e_new_evar (push_rel_context ctx env) evars t in
+ let sigma, e = Evarutil.new_evar (push_rel_context ctx env) !evars t in
+ evars := sigma;
aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
| t -> acc, in_eqs, ctx, ty
in
@@ -4176,7 +4210,7 @@ let induction_tac with_evars params indvars elim =
let elimclause' = recolle_clenv i params indvars elimclause gl in
(* one last resolution (useless?) *)
let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
- Clenvtac.clenv_refine with_evars resolved
+ Clenvtac.clenv_refine ~with_evars resolved
end
(* Apply induction "in place" taking into account dependent
@@ -4334,7 +4368,7 @@ let check_expected_type env sigma (elimc,bl) elimt =
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
- fun t -> Evarconv.e_cumul env (ref sigma) t u
+ fun t -> Option.has_some (Evarconv.cumul env sigma t u)
let check_enough_applied env sigma elim =
(* A heuristic to decide whether the induction arg is enough applied *)
@@ -4927,9 +4961,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
let evd, ctx, concl =
(* FIXME: should be done only if the tactic succeeds *)
- let evd, nf = nf_evars_and_universes !evdref in
+ let evd = Evd.minimize_universes !evdref in
let ctx = Evd.universe_context_set evd in
- evd, ctx, nf concl
+ evd, ctx, Evarutil.nf_evars_universes evd concl
in
let concl = EConstr.of_constr concl in
let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in
@@ -4973,7 +5007,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
let evd = Evd.set_universe_context evd ectx in
let open Safe_typing in
let eff = private_con_of_con (Global.safe_env ()) cst in
- let effs = add_private eff
+ let effs = concat_private eff
Entries.(snd (Future.force const.const_entry_body)) in
let solve =
Proofview.tclEFFECTS effs <*>
@@ -5007,6 +5041,26 @@ let tclABSTRACT ?(opaque=true) name_op tac =
else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
abstract_subproof ~opaque s gk tac
+let constr_eq ~strict x y =
+ let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in
+ let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in
+ Proofview.Goal.enter begin fun gl ->
+ let env = Tacmach.New.pf_env gl in
+ let evd = Tacmach.New.project gl in
+ match EConstr.eq_constr_universes env evd x y with
+ | Some csts ->
+ let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in
+ if strict then
+ if Evd.check_constraints evd csts then Proofview.tclUNIT ()
+ else fail_universes
+ else
+ (match Evd.add_constraints evd csts with
+ | evd -> Proofview.Unsafe.tclEVARS evd
+ | exception Univ.UniverseInconsistency _ ->
+ fail_universes)
+ | None -> fail
+ end
+
let unify ?(state=full_transparent_state) x y =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 079baa3e..34b49f3b 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -16,10 +16,8 @@ open Proof_type
open Evd
open Clenv
open Redexpr
-open Globnames
open Pattern
open Unification
-open Misctypes
open Tactypes
open Locus
open Ltac_pretype
@@ -35,16 +33,16 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
(** {6 Primitive tactics. } *)
-val introduction : ?check:bool -> Id.t -> unit Proofview.tactic
+val introduction : Id.t -> unit Proofview.tactic
val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
val convert_hyp : ?check:bool -> named_declaration -> unit Proofview.tactic
val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
val mutual_fix :
Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic
-val fix : Id.t option -> int -> unit Proofview.tactic
+val fix : Id.t -> int -> unit Proofview.tactic
val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> unit Proofview.tactic
-val cofix : Id.t option -> unit Proofview.tactic
+val cofix : Id.t -> unit Proofview.tactic
val convert : constr -> constr -> unit Proofview.tactic
val convert_leq : constr -> constr -> unit Proofview.tactic
@@ -57,8 +55,8 @@ val find_intro_names : rel_context -> goal sigma -> Id.t list
val intro : unit Proofview.tactic
val introf : unit Proofview.tactic
-val intro_move : Id.t option -> Id.t move_location -> unit Proofview.tactic
-val intro_move_avoid : Id.t option -> Id.Set.t -> Id.t move_location -> unit Proofview.tactic
+val intro_move : Id.t option -> Id.t Logic.move_location -> unit Proofview.tactic
+val intro_move_avoid : Id.t option -> Id.Set.t -> Id.t Logic.move_location -> unit Proofview.tactic
(** [intro_avoiding idl] acts as intro but prevents the new Id.t
to belong to [idl] *)
@@ -92,9 +90,22 @@ val intros_clearing : bool list -> unit Proofview.tactic
val try_intros_until :
(Id.t -> unit Proofview.tactic) -> quantified_hypothesis -> unit Proofview.tactic
+type evars_flag = bool (* true = pose evars false = fail on evars *)
+type rec_flag = bool (* true = recursive false = not recursive *)
+type advanced_flag = bool (* true = advanced false = basic *)
+type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
(** Apply a tactic on a quantified hypothesis, an hypothesis in context
or a term with bindings *)
+type 'a core_destruction_arg =
+ | ElimOnConstr of 'a
+ | ElimOnIdent of lident
+ | ElimOnAnonHyp of int
+
+type 'a destruction_arg =
+ clear_flag * 'a core_destruction_arg
+
val onInductionArg :
(clear_flag -> constr with_bindings -> unit Proofview.tactic) ->
constr with_bindings destruction_arg -> unit Proofview.tactic
@@ -110,11 +121,11 @@ val use_clear_hyp_by_default : unit -> bool
(** {6 Introduction tactics with eliminations. } *)
val intro_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic
-val intro_patterns_to : evars_flag -> Id.t move_location -> intro_patterns ->
+val intro_patterns_to : evars_flag -> Id.t Logic.move_location -> intro_patterns ->
unit Proofview.tactic
-val intro_patterns_bound_to : evars_flag -> int -> Id.t move_location -> intro_patterns ->
+val intro_patterns_bound_to : evars_flag -> int -> Id.t Logic.move_location -> intro_patterns ->
unit Proofview.tactic
-val intro_pattern_to : evars_flag -> Id.t move_location -> delayed_open_constr intro_pattern_expr ->
+val intro_pattern_to : evars_flag -> Id.t Logic.move_location -> delayed_open_constr intro_pattern_expr ->
unit Proofview.tactic
(** Implements user-level "intros", with [] standing for "**" *)
@@ -134,7 +145,7 @@ val exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic
type tactic_reduction = Reductionops.reduction_function
type e_tactic_reduction = Reductionops.e_reduction_function
-type change_arg = patvar_map -> evar_map -> evar_map * constr
+type change_arg = patvar_map -> env -> evar_map -> evar_map * constr
val make_change_arg : constr -> change_arg
val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
@@ -169,7 +180,7 @@ val change :
val pattern_option :
(occurrences * constr) list -> goal_location -> unit Proofview.tactic
val reduce : red_expr -> clause -> unit Proofview.tactic
-val unfold_constr : global_reference -> unit Proofview.tactic
+val unfold_constr : GlobRef.t -> unit Proofview.tactic
(** {6 Modification of the local context. } *)
@@ -181,7 +192,7 @@ val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic
val specialize : constr with_bindings -> intro_pattern option -> unit Proofview.tactic
-val move_hyp : Id.t -> Id.t move_location -> unit Proofview.tactic
+val move_hyp : Id.t -> Id.t Logic.move_location -> unit Proofview.tactic
val rename_hyp : (Id.t * Id.t) list -> unit Proofview.tactic
val revert : Id.t list -> unit Proofview.tactic
@@ -245,7 +256,7 @@ val apply_delayed_in :
type elim_scheme = {
elimc: constr with_bindings option;
elimt: types;
- indref: global_reference option;
+ indref: GlobRef.t option;
params: rel_context; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
nparams: int; (** number of parameters *)
predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
@@ -398,6 +409,11 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -
(** {6 Other tactics. } *)
+(** Syntactic equality up to universes. With [strict] the universe
+ constraints must be already true to succeed, without [strict] they
+ are added to the evar map. *)
+val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic
+
val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 753c608a..8bdcc632 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -37,7 +37,7 @@ struct
type 't t =
| DRel
| DSort
- | DRef of global_reference
+ | DRef of GlobRef.t
| DCtx of 't * 't (* (binding list, subterm) = Prods and LetIns *)
| DLambda of 't * 't
| DApp of 't * 't (* binary app *)
@@ -290,7 +290,7 @@ struct
| Const (c,u) -> Term (DRef (ConstRef c))
| Ind (i,u) -> Term (DRef (IndRef i))
| Construct (c,u)-> Term (DRef (ConstructRef c))
- | Term.Meta _ -> assert false
+ | Meta _ -> assert false
| Evar (i,_) ->
let meta =
try Evar.Map.find i !metas
diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli
index 2c748f9c..7bce5778 100644
--- a/tactics/term_dnet.mli
+++ b/tactics/term_dnet.mli
@@ -26,7 +26,7 @@ open Mod_subst
The results returned here are perfect, since post-filtering is done
inside here.
- See lib/dnet.mli for more details.
+ See tactics/dnet.mli for more details.
*)
(** Identifiers to store (right hand side of the association) *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 01:30:38 +0000