aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml2
-rw-r--r--pretyping/unification.ml63
-rw-r--r--pretyping/unification.mli8
-rw-r--r--proofs/clenv.ml16
-rw-r--r--proofs/clenv.mli8
-rw-r--r--proofs/clenvtac.ml20
-rw-r--r--proofs/clenvtac.mli2
-rw-r--r--tactics/auto.ml7
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/class_tactics.ml47
-rw-r--r--tactics/eauto.ml42
-rw-r--r--tactics/equality.ml28
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/rewrite.ml418
-rw-r--r--tactics/tacticals.ml3
-rw-r--r--tactics/tactics.ml48
-rw-r--r--tactics/tactics.mli15
17 files changed, 145 insertions, 106 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index ad315035a..217a8fe4f 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -370,7 +370,7 @@ let find_subsubgoal c ctyp skip submetas gls =
let se = Stack.pop stack in
try
let unifier =
- Unification.w_unify true env Reduction.CUMUL
+ Unification.w_unify env Reduction.CUMUL ~flags:Unification.elim_flags
ctyp se.se_type se.se_evd in
if n <= 0 then
{se with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 9e1ccd026..47fec1496 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -164,7 +164,8 @@ type unify_flags = {
resolve_evars : bool;
use_evars_pattern_unification : bool;
modulo_betaiota : bool;
- modulo_eta : bool
+ modulo_eta : bool;
+ allow_K_in_toplevel_higher_order_unification : bool
}
let default_unify_flags = {
@@ -175,7 +176,8 @@ let default_unify_flags = {
resolve_evars = false;
use_evars_pattern_unification = true;
modulo_betaiota = false;
- modulo_eta = true
+ modulo_eta = true;
+ allow_K_in_toplevel_higher_order_unification = false
}
let default_no_delta_unify_flags = {
@@ -186,7 +188,32 @@ let default_no_delta_unify_flags = {
resolve_evars = false;
use_evars_pattern_unification = false;
modulo_betaiota = false;
- modulo_eta = true
+ modulo_eta = true;
+ allow_K_in_toplevel_higher_order_unification = false
+}
+
+let elim_flags = {
+ modulo_conv_on_closed_terms = Some full_transparent_state;
+ use_metas_eagerly = true;
+ modulo_delta = full_transparent_state;
+ modulo_delta_types = full_transparent_state;
+ resolve_evars = false;
+ use_evars_pattern_unification = true;
+ modulo_betaiota = false;
+ modulo_eta = true;
+ allow_K_in_toplevel_higher_order_unification = true
+}
+
+let elim_no_delta_flags = {
+ modulo_conv_on_closed_terms = Some full_transparent_state;
+ use_metas_eagerly = true;
+ modulo_delta = empty_transparent_state;
+ modulo_delta_types = full_transparent_state;
+ resolve_evars = false;
+ use_evars_pattern_unification = false;
+ modulo_betaiota = false;
+ modulo_eta = true;
+ allow_K_in_toplevel_higher_order_unification = true
}
let use_evars_pattern_unification flags =
@@ -936,25 +963,28 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd =
else
res
-let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd =
+let w_unify_to_subterm_list env flags hdmeta oplist t evd =
List.fold_right
(fun op (evd,l) ->
let op = whd_meta evd op in
if isMeta op then
- if allow_K then (evd,op::l)
+ if flags.allow_K_in_toplevel_higher_order_unification then (evd,op::l)
else error_abstraction_over_meta env evd hdmeta (destMeta op)
else if occur_meta_or_existential op then
let (evd',cl) =
try
(* This is up to delta for subterms w/o metas ... *)
w_unify_to_subterm env ~flags (strip_outer_cast op,t) evd
- with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op)
+ with PretypeError (env,_,NoOccurrenceFound _) when
+ flags.allow_K_in_toplevel_higher_order_unification -> (evd,op)
in
- if not allow_K && (* ensure we found a different instance *)
+ if not flags.allow_K_in_toplevel_higher_order_unification &&
+ (* ensure we found a different instance *)
List.exists (fun op -> eq_constr op cl) l
then error_non_linear_unification env evd hdmeta cl
else (evd',cl::l)
- else if allow_K or dependent op t then
+ else if flags.allow_K_in_toplevel_higher_order_unification or dependent op t
+ then
(evd,op::l)
else
(* This is not up to delta ... *)
@@ -962,29 +992,28 @@ let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd =
oplist
(evd,[])
-let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
+let secondOrderAbstraction env flags typ (p, oplist) evd =
(* Remove delta when looking for a subterm *)
let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in
- let (evd',cllist) =
- w_unify_to_subterm_list env flags allow_K p oplist typ evd in
+ let (evd',cllist) = w_unify_to_subterm_list env flags p oplist typ evd in
let typp = Typing.meta_type evd' p in
let pred = abstract_list_all env evd' typp typ cllist in
w_merge env false flags (evd',[p,pred,(Conv,TypeProcessed)],[])
-let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
+let w_unify2 env flags cv_pb ty1 ty2 evd =
let c1, oplist1 = whd_stack evd ty1 in
let c2, oplist2 = whd_stack evd ty2 in
match kind_of_term c1, kind_of_term c2 with
| Meta p1, _ ->
(* Find the predicate *)
let evd' =
- secondOrderAbstraction env flags allow_K ty2 (p1,oplist1) evd in
+ secondOrderAbstraction env flags ty2 (p1,oplist1) evd in
(* Resume first order unification *)
w_unify_0 env cv_pb flags (nf_meta evd' ty1) ty2 evd'
| _, Meta p2 ->
(* Find the predicate *)
let evd' =
- secondOrderAbstraction env flags allow_K ty1 (p2, oplist2) evd in
+ secondOrderAbstraction env flags ty1 (p2, oplist2) evd in
(* Resume first order unification *)
w_unify_0 env cv_pb flags ty1 (nf_meta evd' ty2) evd'
| _ -> error "w_unify2"
@@ -1009,7 +1038,7 @@ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
Before, second-order was used if the type of Meta(1) and [x:A]t was
convertible and first-order otherwise. But if failed if e.g. the type of
Meta(1) had meta-variables in it. *)
-let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
+let w_unify env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
let hd1,l1 = whd_stack evd ty1 in
let hd2,l2 = whd_stack evd ty2 in
match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
@@ -1020,13 +1049,13 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
w_typed_unify env cv_pb flags ty1 ty2 evd
with ex when precatchable_exception ex ->
try
- w_unify2 env flags allow_K cv_pb ty1 ty2 evd
+ w_unify2 env flags cv_pb ty1 ty2 evd
with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e)
(* Second order case *)
| (Meta _, true, _, _ | _, _, Meta _, true) ->
(try
- w_unify2 env flags allow_K cv_pb ty1 ty2 evd
+ w_unify2 env flags cv_pb ty1 ty2 evd
with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e
| ex when precatchable_exception ex ->
try
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index cd8e70418..0f7eec692 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -18,15 +18,19 @@ type unify_flags = {
resolve_evars : bool;
use_evars_pattern_unification : bool;
modulo_betaiota : bool;
- modulo_eta : bool
+ modulo_eta : bool;
+ allow_K_in_toplevel_higher_order_unification : bool
}
val default_unify_flags : unify_flags
val default_no_delta_unify_flags : unify_flags
+val elim_flags : unify_flags
+val elim_no_delta_flags : unify_flags
+
(** The "unique" unification fonction *)
val w_unify :
- bool -> env -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map -> evar_map
+ env -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map -> evar_map
(** [w_unify_to_subterm env (c,t) m] performs unification of [c] with a
subterm of [t]. Constraints are added to [m] and the matched
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 632bf3a62..35552b8d8 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -265,20 +265,20 @@ let clenv_dependent ce = clenv_dependent_gen false ce
(******************************************************************)
-let clenv_unify allow_K ?(flags=default_unify_flags) cv_pb t1 t2 clenv =
+let clenv_unify ?(flags=default_unify_flags) cv_pb t1 t2 clenv =
{ clenv with
- evd = w_unify allow_K ~flags:flags clenv.env cv_pb t1 t2 clenv.evd }
+ evd = w_unify ~flags clenv.env cv_pb t1 t2 clenv.evd }
let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
{ clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
-let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
+let clenv_unique_resolver ?(flags=default_unify_flags) clenv gl =
let concl = Goal.V82.concl clenv.evd (sig_it gl) in
if isMeta (fst (whd_stack clenv.evd clenv.templtyp.rebus)) then
- clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) concl
- (clenv_unify_meta_types ~flags:flags clenv)
+ clenv_unify CUMUL ~flags (clenv_type clenv) concl
+ (clenv_unify_meta_types ~flags clenv)
else
- clenv_unify allow_K CUMUL ~flags:flags
+ clenv_unify CUMUL ~flags
(meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
(* [clenv_pose_metas_as_evars clenv dep_mvs]
@@ -356,7 +356,7 @@ let connect_clenv gls clenv =
In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
*)
-let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv =
+let clenv_fchain ?(flags=elim_flags) mv clenv nextclenv =
(* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
let clenv' =
{ templval = clenv.templval;
@@ -365,7 +365,7 @@ let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv
env = nextclenv.env } in
(* unify the type of the template of [nextclenv] with the type of [mv] *)
let clenv'' =
- clenv_unify allow_K ~flags:flags CUMUL
+ clenv_unify ~flags:flags CUMUL
(clenv_term clenv' nextclenv.templtyp)
(clenv_meta_type clenv' mv)
clenv' in
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index af51e6716..b685f5041 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -54,22 +54,22 @@ val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> claus
val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
val clenv_fchain :
- ?allow_K:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
+ ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
(** {6 Unification with clenvs } *)
(** Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
val clenv_unify :
- bool -> ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
+ ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
(** unifies the concl of the goal with the type of the clenv *)
val clenv_unique_resolver :
- bool -> ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
+ ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
(** same as above ([allow_K=false]) but replaces remaining metas
with fresh evars if [evars_flag] is [true] *)
val evar_clenv_unique_resolver :
- bool -> ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
+ ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
val clenv_dependent : clausenv -> metavariable list
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index e4ad27f2e..e05651952 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -81,17 +81,18 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls =
(refine (clenv_cast_meta clenv (clenv_value clenv)))
gls
-let dft = Unification.default_unify_flags
+open Unification
+
+let dft = default_unify_flags
-let res_pf clenv ?(with_evars=false) ?(allow_K=false) ?(flags=dft) gls =
- clenv_refine with_evars
- (clenv_unique_resolver allow_K ~flags:flags clenv gls) gls
+let res_pf clenv ?(with_evars=false) ?(flags=dft) gls =
+ clenv_refine with_evars (clenv_unique_resolver ~flags clenv gls) gls
let elim_res_pf_THEN_i clenv tac gls =
- let clenv' = (clenv_unique_resolver true clenv gls) in
+ let clenv' = (clenv_unique_resolver ~flags:elim_flags clenv gls) in
tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls
-let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft
+let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft
(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
@@ -99,8 +100,6 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft
d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
-open Unification
-
let fail_quick_unif_flags = {
modulo_conv_on_closed_terms = Some full_transparent_state;
use_metas_eagerly = false;
@@ -109,14 +108,15 @@ let fail_quick_unif_flags = {
resolve_evars = false;
use_evars_pattern_unification = false;
modulo_betaiota = false;
- modulo_eta = true
+ modulo_eta = true;
+ allow_K_in_toplevel_higher_order_unification = false
}
(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
let unifyTerms ?(flags=fail_quick_unif_flags) m n gls =
let env = pf_env gls in
let evd = create_goal_evar_defs (project gls) in
- let evd' = w_unify false env CONV ~flags m n evd in
+ let evd' = w_unify env CONV ~flags m n evd in
tclIDTAC {it = gls.it; sigma = evd'}
let unify ?(flags=fail_quick_unif_flags) m gls =
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index d288eddd2..49a961f5d 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -19,7 +19,7 @@ open Unification
(** Tactics *)
val unify : ?flags:unify_flags -> constr -> tactic
val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> tactic
-val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic
+val res_pf : clausenv -> ?with_evars:evars_flag -> ?flags:unify_flags -> tactic
val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
diff --git a/tactics/auto.ml b/tactics/auto.ml
index f4952cf0d..4c00a60d0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -846,7 +846,8 @@ let auto_unif_flags = {
resolve_evars = true;
use_evars_pattern_unification = false;
modulo_betaiota = false;
- modulo_eta = true
+ modulo_eta = true;
+ allow_K_in_toplevel_higher_order_unification = false
}
(* Try unification with the precompiled clause, then use registered Apply *)
@@ -857,12 +858,12 @@ let h_clenv_refine ev c clenv =
let unify_resolve_nodelta (c,clenv) gl =
let clenv' = connect_clenv gl clenv in
- let clenv'' = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gl in
+ let clenv'' = clenv_unique_resolver ~flags:auto_unif_flags clenv' gl in
h_clenv_refine false c clenv'' gl
let unify_resolve flags (c,clenv) gl =
let clenv' = connect_clenv gl clenv in
- let clenv'' = clenv_unique_resolver false ~flags clenv' gl in
+ let clenv'' = clenv_unique_resolver ~flags clenv' gl in
h_clenv_refine false c clenv'' gl
let unify_resolve_gen = function
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 73f8fde29..55e23d342 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -246,7 +246,7 @@ type hypinfo = {
let evd_convertible env evd x y =
try
- ignore(Unification.w_unify true env Reduction.CONV x y evd); true
+ ignore(Unification.w_unify ~flags:Unification.elim_flags env Reduction.CONV x y evd); true
(* try ignore(Evarconv.the_conv_x env x y evd); true *)
with _ -> false
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 870e05e4b..3b193f6d9 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -80,7 +80,8 @@ let auto_unif_flags = {
resolve_evars = false;
use_evars_pattern_unification = true;
modulo_betaiota = true;
- modulo_eta = true
+ modulo_eta = true;
+ allow_K_in_toplevel_higher_order_unification = false
}
let rec eq_constr_mod_evars x y =
@@ -103,12 +104,12 @@ END
let unify_e_resolve flags (c,clenv) gls =
let clenv' = connect_clenv gls clenv in
- let clenv' = clenv_unique_resolver false ~flags clenv' gls in
+ let clenv' = clenv_unique_resolver ~flags clenv' gls in
Clenvtac.clenv_refine true ~with_classes:false clenv' gls
let unify_resolve flags (c,clenv) gls =
let clenv' = connect_clenv gls clenv in
- let clenv' = clenv_unique_resolver false ~flags clenv' gls in
+ let clenv' = clenv_unique_resolver ~flags clenv' gls in
Clenvtac.clenv_refine false ~with_classes:false clenv' gls
let clenv_of_prods nprods (c, clenv) gls =
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index a14cf6287..2e7e9c3b2 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -93,7 +93,7 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
let unify_e_resolve flags (c,clenv) gls =
let clenv' = connect_clenv gls clenv in
- let _ = clenv_unique_resolver false ~flags clenv' gls in
+ let _ = clenv_unique_resolver ~flags clenv' gls in
h_simplest_eapply c gls
let rec e_trivial_fail_db db_list local_db goal =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 822198c7c..3b734b4c6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -88,7 +88,9 @@ let rewrite_unif_flags = {
Unification.resolve_evars = true;
Unification.use_evars_pattern_unification = true;
Unification.modulo_betaiota = false;
- Unification.modulo_eta = true
+ Unification.modulo_eta = true;
+ Unification.allow_K_in_toplevel_higher_order_unification = false
+ (* allow_K does not matter in practice because calls w_typed_unify *)
}
let side_tac tac sidetac =
@@ -120,11 +122,27 @@ let instantiate_lemma env sigma gl c ty l l2r concl =
let eqclause = Clenv.make_clenv_binding gl (c,t) l in
[eqclause]
-let rewrite_elim with_evars c e ?(allow_K=true) =
- general_elim_clause_gen (elimination_clause_scheme with_evars allow_K) c e
+let rewrite_conv_closed_unif_flags = {
+ Unification.modulo_conv_on_closed_terms = Some full_transparent_state;
+ Unification.use_metas_eagerly = true;
+ Unification.modulo_delta = empty_transparent_state;
+ Unification.modulo_delta_types = full_transparent_state;
+ Unification.resolve_evars = false;
+ Unification.use_evars_pattern_unification = true;
+ Unification.modulo_betaiota = false;
+ Unification.modulo_eta = true;
+ Unification.allow_K_in_toplevel_higher_order_unification = false
+}
+
+let rewrite_elim with_evars c e =
+ general_elim_clause_gen
+ (elimination_clause_scheme with_evars ~flags:rewrite_conv_closed_unif_flags)
+ c e
let rewrite_elim_in with_evars id c e =
- general_elim_clause_gen (elimination_in_clause_scheme with_evars id) c e
+ general_elim_clause_gen
+ (elimination_in_clause_scheme with_evars
+ ~flags:rewrite_conv_closed_unif_flags id) c e
(* Ad hoc asymmetric general_elim_clause *)
let general_elim_clause with_evars cls rew elim =
@@ -134,7 +152,7 @@ let general_elim_clause with_evars cls rew elim =
(* was tclWEAK_PROGRESS which only fails for tactics generating one
subgoal and did not fail for useless conditional rewritings generating
an extra condition *)
- tclNOTSAMEGOAL (rewrite_elim with_evars rew elim ~allow_K:false)
+ tclNOTSAMEGOAL (rewrite_elim with_evars rew elim)
| Some id -> rewrite_elim_in with_evars id rew elim)
with Pretype_errors.PretypeError (env,evd,
Pretype_errors.NoOccurrenceFound (c', _)) ->
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 95814302d..a6915461d 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -271,7 +271,7 @@ let lemInv id c gls =
try
let clause = mk_clenv_type_of gls c in
let clause = clenv_constrain_last_binding (mkVar id) clause in
- Clenvtac.res_pf clause ~allow_K:true gls
+ Clenvtac.res_pf clause ~flags:Unification.elim_flags gls
with
| NoSuchBinding ->
errorlabstrm ""
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index f0ca4ae50..41ed88d2f 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -308,7 +308,8 @@ let rewrite_unif_flags = {
Unification.resolve_evars = true;
Unification.use_evars_pattern_unification = true;
Unification.modulo_betaiota = false;
- Unification.modulo_eta = true
+ Unification.modulo_eta = true;
+ Unification.allow_K_in_toplevel_higher_order_unification = true
}
let rewrite2_unif_flags =
@@ -319,7 +320,8 @@ let rewrite2_unif_flags =
Unification.resolve_evars = true;
Unification.use_evars_pattern_unification = true;
Unification.modulo_betaiota = true;
- Unification.modulo_eta = true
+ Unification.modulo_eta = true;
+ Unification.allow_K_in_toplevel_higher_order_unification = true
}
let general_rewrite_unif_flags () =
@@ -331,13 +333,12 @@ let general_rewrite_unif_flags () =
Unification.resolve_evars = true;
Unification.use_evars_pattern_unification = true;
Unification.modulo_betaiota = true;
- Unification.modulo_eta = true }
+ Unification.modulo_eta = true;
+ Unification.allow_K_in_toplevel_higher_order_unification = true }
let convertible env evd x y =
Reductionops.is_conv env evd x y
-let allowK = true
-
let refresh_hypinfo env sigma hypinfo =
if hypinfo.abs = None then
let {l2r=l2r; c=c;cl=cl;flags=flags} = hypinfo in
@@ -356,11 +357,10 @@ let unify_eqn env sigma hypinfo t =
let env', prf, c1, c2, car, rel =
match abs with
| Some (absprf, absprfty) ->
- let env' = clenv_unify allowK ~flags:rewrite_unif_flags CONV left t cl in
+ let env' = clenv_unify ~flags:rewrite_unif_flags CONV left t cl in
env', prf, c1, c2, car, rel
| None ->
- let env' =
- clenv_unify allowK ~flags:!hypinfo.flags CONV left t cl
+ let env' = clenv_unify ~flags:!hypinfo.flags CONV left t cl
in
let env' = Clenvtac.clenv_pose_dependent_evars true env' in
(* let env' = Clenv.clenv_pose_metas_as_evars env' (Evd.undefined_metas env'.evd) in *)
@@ -1018,7 +1018,7 @@ module Strategies =
with _ -> error "fold: the term is not unfoldable !"
in
try
- let sigma = Unification.w_unify true env CONV ~flags:Unification.default_unify_flags unfolded t sigma in
+ let sigma = Unification.w_unify env CONV ~flags:Unification.elim_flags unfolded t sigma in
let c' = Evarutil.nf_evar sigma c in
Some (Some { rew_car = ty; rew_from = t; rew_to = c';
rew_prf = RewCast DEFAULTcast;
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index e2e6e3a71..11625cbdf 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -363,7 +363,8 @@ let general_elim_then_using mk_elim
match predicate with
| None -> elimclause'
| Some p ->
- clenv_unify true Reduction.CONV (mkMeta pmv) p elimclause'
+ clenv_unify ~flags:Unification.elim_flags
+ Reduction.CONV (mkMeta pmv) p elimclause'
in
elim_res_pf_THEN_i elimclause' branchtacs gl
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f191bacf2..060cd94a8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -704,27 +704,15 @@ let index_of_ind_arg t =
| None -> error "Could not find inductive argument of elimination scheme."
in aux None 0 t
-let elim_flags = {
- modulo_conv_on_closed_terms = Some full_transparent_state;
- use_metas_eagerly = true;
- modulo_delta = empty_transparent_state;
- modulo_delta_types = full_transparent_state;
- resolve_evars = false;
- use_evars_pattern_unification = true;
- modulo_betaiota = false;
- modulo_eta = true
-}
-
-let elimination_clause_scheme with_evars allow_K i elimclause indclause gl =
+let elimination_clause_scheme with_evars ?(flags=elim_flags) i elimclause indclause gl =
let indmv =
(match kind_of_term (nth_arg i elimclause.templval.rebus) with
| Meta mv -> mv
| _ -> errorlabstrm "elimination_clause"
(str "The type of elimination clause is not well-formed."))
in
- let elimclause' = clenv_fchain ~flags:elim_flags indmv elimclause indclause in
- res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K ~flags:elim_flags
- gl
+ let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
+ res_pf elimclause' ~with_evars:with_evars ~flags gl
(*
* Elimination tactic with bindings and using an arbitrary
@@ -753,8 +741,8 @@ let general_elim_clause elimtac (c,lbindc) elim gl =
let indclause = make_clenv_binding gl (c,t) lbindc in
general_elim_clause_gen elimtac indclause elim gl
-let general_elim with_evars c e ?(allow_K=true) =
- general_elim_clause (elimination_clause_scheme with_evars allow_K) c e
+let general_elim with_evars c e =
+ general_elim_clause (elimination_clause_scheme with_evars) c e
(* Elimination tactic with bindings but using the default elimination
* constant associated with the type. *)
@@ -770,7 +758,6 @@ let default_elim with_evars (c,_ as cx) gl =
let elim_in_context with_evars c = function
| Some elim ->
general_elim with_evars c {elimindex = Some (-1); elimbody = elim}
- ~allow_K:true
| None -> default_elim with_evars c
let elim with_evars (c,lbindc as cx) elim =
@@ -795,13 +782,13 @@ let simplest_elim c = default_elim false (c,NoBindings)
(e.g. it could replace id:A->B->C by id:C, knowing A/\B)
*)
-let clenv_fchain_in id elim_flags mv elimclause hypclause =
- try clenv_fchain ~allow_K:false ~flags:elim_flags mv elimclause hypclause
+let clenv_fchain_in id ?(flags=elim_flags) mv elimclause hypclause =
+ try clenv_fchain ~flags mv elimclause hypclause
with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
(* Set the hypothesis name in the message *)
raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
-let elimination_in_clause_scheme with_evars id i elimclause indclause gl =
+let elimination_in_clause_scheme with_evars ?(flags=elim_flags) id i elimclause indclause gl =
let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
let hypmv =
try match list_remove indmv (clenv_independent elimclause) with
@@ -809,12 +796,11 @@ let elimination_in_clause_scheme with_evars id i elimclause indclause gl =
| _ -> failwith ""
with Failure _ -> errorlabstrm "elimination_clause"
(str "The type of elimination clause is not well-formed.") in
- let elimclause' = clenv_fchain indmv elimclause indclause in
+ let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
let hyp = mkVar id in
let hyp_typ = pf_type_of gl hyp in
let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
- let elimclause'' =
- clenv_fchain_in id elim_flags hypmv elimclause' hypclause in
+ let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
let new_hyp_typ = clenv_type elimclause'' in
if eq_constr hyp_typ new_hyp_typ then
errorlabstrm "general_rewrite_in"
@@ -1008,8 +994,7 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
let apply_in_once sidecond_first with_delta with_destruct with_evars id
(loc,(d,lbind)) gl0 =
- let flags =
- if with_delta then default_unify_flags else default_no_delta_unify_flags in
+ let flags = if with_delta then elim_flags else elim_no_delta_flags in
let t' = pf_get_hyp_typ gl0 id in
let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in
let rec aux with_destruct c gl =
@@ -2857,7 +2842,7 @@ let induction_tac_felim with_evars indvars nparams elim gl =
(* elimclause' is built from elimclause by instanciating all args and params. *)
let elimclause' = recolle_clenv nparams indvars elimclause gl in
(* one last resolution (useless?) *)
- let resolved = clenv_unique_resolver true elimclause' gl in
+ let resolved = clenv_unique_resolver ~flags:elim_flags elimclause' gl in
clenv_refine with_evars resolved gl
(* Apply induction "in place" replacing the hypothesis on which
@@ -2953,7 +2938,7 @@ let induction_tac with_evars elim (varname,lbind) typ gl =
let elimclause =
make_clenv_binding gl
(mkCast (elimc,DEFAULTcast,elimt),elimt) lbindelimc in
- elimination_clause_scheme with_evars true i elimclause indclause gl
+ elimination_clause_scheme with_evars i elimclause indclause gl
let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
inhyps gl =
@@ -3176,9 +3161,9 @@ let elim_scheme_type elim t gl =
| Meta mv ->
let clause' =
(* t is inductive, then CUMUL or CONV is irrelevant *)
- clenv_unify true Reduction.CUMUL t
+ clenv_unify ~flags:elim_flags Reduction.CUMUL t
(clenv_meta_type clause mv) clause in
- res_pf clause' ~allow_K:true gl
+ res_pf clause' ~flags:elim_flags gl
| _ -> anomaly "elim_scheme_type"
let elim_type t gl =
@@ -3480,7 +3465,6 @@ let unify ?(state=full_transparent_state) x y gl =
modulo_delta = state;
modulo_conv_on_closed_terms = Some state}
in
- let evd = w_unify false (pf_env gl) Reduction.CONV
- ~flags x y (project gl)
+ let evd = w_unify (pf_env gl) Reduction.CONV ~flags x y (project gl)
in tclEVARS evd gl
with _ -> tclFAIL 0 (str"Not unifiable") gl
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index a2dd6e411..c52c14587 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -26,6 +26,7 @@ open Nametab
open Glob_term
open Pattern
open Termops
+open Unification
(** Main tactics. *)
@@ -248,19 +249,19 @@ type eliminator = {
elimbody : constr with_bindings
}
-val elimination_clause_scheme : evars_flag ->
- bool -> int -> clausenv -> clausenv -> tactic
+val elimination_clause_scheme : evars_flag -> ?flags:unify_flags ->
+ int -> clausenv -> clausenv -> tactic
-val elimination_in_clause_scheme : evars_flag -> identifier -> int ->
- clausenv -> clausenv -> tactic
+val elimination_in_clause_scheme : evars_flag -> ?flags:unify_flags ->
+ identifier -> int -> clausenv -> clausenv -> tactic
val general_elim_clause_gen : (int -> Clenv.clausenv -> 'a -> tactic) ->
'a -> eliminator -> tactic
val general_elim : evars_flag ->
- constr with_bindings -> eliminator -> ?allow_K:bool -> tactic
-val general_elim_in : evars_flag ->
- identifier -> constr with_bindings -> eliminator -> tactic
+ constr with_bindings -> eliminator -> tactic
+val general_elim_in : evars_flag -> identifier ->
+ constr with_bindings -> eliminator -> tactic
val default_elim : evars_flag -> constr with_bindings -> tactic
val simplest_elim : constr -> tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 19:33:59 +0000