aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES7
-rw-r--r--contrib/interface/pbp.ml2
-rw-r--r--contrib/interface/showproof.ml2
-rw-r--r--contrib/interface/xlate.ml9
-rw-r--r--parsing/pptactic.ml5
-rw-r--r--pretyping/unification.ml6
-rw-r--r--pretyping/unification.mli1
-rw-r--r--proofs/tacexpr.ml3
-rw-r--r--tactics/hiddentac.ml10
-rw-r--r--tactics/hiddentac.mli3
-rw-r--r--tactics/tacinterp.ml6
-rw-r--r--tactics/tactics.ml19
-rw-r--r--tactics/tactics.mli11
13 files changed, 55 insertions, 29 deletions
diff --git a/CHANGES b/CHANGES
index ffa6fecb46..ed4f1fa6e2 100644
--- a/CHANGES
+++ b/CHANGES
@@ -118,7 +118,8 @@ Tactics
expressions with explicit occurrences of match or fix.
- Better heuristic of lemma unfolding for apply/eapply.
- New tactics "eapply in", "erewrite", "erewrite in".
-- Unfoldable references can be given by notation rather than by name in unfold.
+- Unfoldable references can be given by notation's string rather than by name
+ in unfold.
- The "with" arguments are now typed using informations from the current goal:
allows support for coercions and more inference of implicit arguments.
- Application of "f_equal"-style lemmas works better.
@@ -137,7 +138,9 @@ Tactics
induction-inversion on instantiated inductive families à la BasicElim.
- Tactic apply now able to reason modulo unfolding of constants
(possible source of incompatibility in situations where apply may fail,
- e.g. as argument of a try or a repeat and in a ltac function).
+ e.g. as argument of a try or a repeat and in a ltac function);
+ version of apply that does not unfold is renamed into "simple apply"
+ (usable for compatibility or for automation).
- Pattern for hypotheses types in match goal are now interpreted in type_scope.
Type Classes
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index be99bdde0a..0680cc23e5 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -171,7 +171,7 @@ let make_pbp_atomic_tactic = function
| PbpRight -> TacAtom (zz, TacRight NoBindings)
| PbpIntros l -> TacAtom (zz, TacIntroPattern l)
| PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
- | PbpApply h -> TacAtom (zz, TacApply (false,(make_var h,NoBindings)))
+ | PbpApply h -> TacAtom (zz, TacApply (true,false,(make_var h,NoBindings)))
| PbpElim (hyp_name, names) ->
let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
TacAtom
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index e3f6572020..20c1cc04f5 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1202,7 +1202,7 @@ let rec natural_ntree ig ntree =
| TacExtend (_,"InductionIntro",[a]) ->
let id=(out_gen wit_ident a) in
natural_induction ig lh g gs ge id ltree true
- | TacApply (false,(c,_)) -> natural_apply ig lh g gs (snd c) ltree
+ | TacApply (_,false,(c,_)) -> natural_apply ig lh g gs (snd c) ltree
| TacExact c -> natural_exact ig lh g gs (snd c) ltree
| TacCut c -> natural_cut ig lh g gs (snd c) ltree
| TacExtend (_,"CutIntro",[a]) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 0e57982106..f442bf75ff 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1143,10 +1143,11 @@ and xlate_tac =
xlate_error "TODO: trivial using"
| TacReduce (red, l) ->
CT_reduce (xlate_red_tactic red, xlate_clause l)
- | TacApply (false,(c,bindl)) ->
+ | TacApply (true,false,(c,bindl)) ->
CT_apply (xlate_formula c, xlate_bindings bindl)
- | TacApply (true,(c,bindl)) ->
+ | TacApply (true,true,(c,bindl)) ->
CT_eapply (xlate_formula c, xlate_bindings bindl)
+ | TacApply (false,_,_) -> xlate_error "TODO: simple (e)apply"
| TacConstructor (n_or_meta, bindl) ->
let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
in CT_constructor (CT_int n, xlate_bindings bindl)
@@ -1984,7 +1985,7 @@ let rec xlate_vernac =
| VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme"
| VernacSyntacticDefinition (id, ([],c), false, _) ->
CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt None)
- | VernacSyntacticDefinition (id, _, true, _) ->
+ | VernacSyntacticDefinition (id, _, _, _) ->
xlate_error"TODO: Local abbreviations and abbreviations with parameters"
(* Modules and Module Types *)
| VernacInclude (_) -> xlate_error "TODO : Include "
@@ -2202,7 +2203,7 @@ let rec xlate_vernac =
VernacMemOption (_, _)|VernacRemoveOption (_, _)
| VernacBack _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _|
VernacSolveExistential (_, _)|VernacCanonical _ |
- VernacTacticNotation _)
+ VernacTacticNotation _ | VernacUndoTo _ | VernacRemoveName _)
-> xlate_error "TODO: vernac";;
let rec xlate_vernac_list =
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 7775dc9816..aded98828e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -672,8 +672,9 @@ and pr_atom1 = function
| TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
| TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
| TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c)
- | TacApply (ev,cb) ->
- hov 1 (str (if ev then "eapply" else "apply") ++ spc () ++
+ | TacApply (a,ev,cb) ->
+ hov 1 ((if a then str "simple " else mt()) ++
+ str (if ev then "eapply" else "apply") ++ spc () ++
pr_with_bindings cb)
| TacElim (ev,cb,cbo) ->
hov 1 (str (if ev then "eelim" else "elim") ++ pr_arg pr_with_bindings cb ++
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index bf72c9c7c5..3f260991c7 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -135,6 +135,12 @@ let default_unify_flags = {
modulo_delta = Cpred.full;
}
+let default_no_delta_unify_flags = {
+ modulo_conv_on_closed_terms = true;
+ use_metas_eagerly = true;
+ modulo_delta = Cpred.empty;
+}
+
let unify_0_with_initial_metas metas is_subterm env sigma cv_pb flags m n =
let nb = nb_rel env in
let trivial_unify pb (metasubst,_) m n =
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 4ca1d7e4f6..e0551b6257 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -21,6 +21,7 @@ type unify_flags = {
}
val default_unify_flags : unify_flags
+val default_no_delta_unify_flags : unify_flags
(* The "unique" unification fonction *)
val w_unify :
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 5ddebf3c99..595c2ec9b8 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -23,6 +23,7 @@ type direction_flag = bool (* true = Left-to-right false = right-to-right *)
type lazy_flag = bool (* true = lazy false = eager *)
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 raw_red_flag =
| FBeta
@@ -130,7 +131,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
| TacExact of 'constr
| TacExactNoCheck of 'constr
| TacVmCastNoCheck of 'constr
- | TacApply of evars_flag * 'constr with_bindings
+ | TacApply of advanced_flag * evars_flag * 'constr with_bindings
| TacElim of evars_flag * 'constr with_bindings *
'constr with_bindings option
| TacElimType of 'constr
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 60f1ccf0ca..18263127be 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -39,9 +39,9 @@ let h_exact_no_check c =
abstract_tactic (TacExactNoCheck (inj_open c)) (exact_no_check c)
let h_vm_cast_no_check c =
abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c)
-let h_apply ev cb =
- abstract_tactic (TacApply (ev,inj_open_wb cb))
- (apply_with_ebindings_gen ev cb)
+let h_apply simple ev cb =
+ abstract_tactic (TacApply (simple,ev,inj_open_wb cb))
+ (apply_with_ebindings_gen simple ev cb)
let h_elim ev cb cbo =
abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo))
(elim ev cb cbo)
@@ -123,8 +123,8 @@ let h_symmetry c = abstract_tactic (TacSymmetry c) (intros_symmetry c)
let h_transitivity c =
abstract_tactic (TacTransitivity (inj_open c)) (intros_transitivity c)
-let h_simplest_apply c = h_apply false (c,NoBindings)
-let h_simplest_eapply c = h_apply true (c,NoBindings)
+let h_simplest_apply c = h_apply false false (c,NoBindings)
+let h_simplest_eapply c = h_apply false true (c,NoBindings)
let h_simplest_elim c = h_elim false (c,NoBindings) None
let h_simplest_case c = h_case false (c,NoBindings)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 909d294cf6..84a5719374 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -34,7 +34,8 @@ val h_exact : constr -> tactic
val h_exact_no_check : constr -> tactic
val h_vm_cast_no_check : constr -> tactic
-val h_apply : evars_flag -> constr with_ebindings -> tactic
+val h_apply : advanced_flag -> evars_flag ->
+ constr with_ebindings -> tactic
val h_elim : evars_flag -> constr with_ebindings ->
constr with_ebindings option -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 536b5ebbdf..719307b116 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -645,7 +645,7 @@ let rec intern_atomic lf ist x =
| TacExact c -> TacExact (intern_constr ist c)
| TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
| TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c)
- | TacApply (ev,cb) -> TacApply (ev,intern_constr_with_bindings ist cb)
+ | TacApply (a,ev,cb) -> TacApply (a,ev,intern_constr_with_bindings ist cb)
| TacElim (ev,cb,cbo) ->
TacElim (ev,intern_constr_with_bindings ist cb,
Option.map (intern_constr_with_bindings ist) cbo)
@@ -2002,7 +2002,7 @@ and interp_atomic ist gl = function
| TacExact c -> h_exact (pf_interp_casted_constr ist gl c)
| TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c)
| TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c)
- | TacApply (ev,cb) -> h_apply ev (interp_constr_with_bindings ist gl cb)
+ | TacApply (a,ev,cb) -> h_apply a ev (interp_constr_with_bindings ist gl cb)
| TacElim (ev,cb,cbo) ->
h_elim ev (interp_constr_with_bindings ist gl cb)
(Option.map (interp_constr_with_bindings ist gl) cbo)
@@ -2336,7 +2336,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacExact c -> TacExact (subst_rawconstr subst c)
| TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c)
| TacVmCastNoCheck c -> TacVmCastNoCheck (subst_rawconstr subst c)
- | TacApply (ev,cb) -> TacApply (ev,subst_raw_with_bindings subst cb)
+ | TacApply (a,ev,cb) -> TacApply (a,ev,subst_raw_with_bindings subst cb)
| TacElim (ev,cb,cbo) ->
TacElim (ev,subst_raw_with_bindings subst cb,
Option.map (subst_raw_with_bindings subst) cbo)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e8192c177e..28e35cf97b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -545,7 +545,9 @@ let clenv_refine_in with_evars id clenv gl =
(* Resolution with missing arguments *)
-let apply_with_ebindings_gen with_evars (c,lbind) gl =
+let apply_with_ebindings_gen advanced with_evars (c,lbind) gl =
+ let flags =
+ if advanced 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. *)
@@ -555,7 +557,7 @@ let apply_with_ebindings_gen with_evars (c,lbind) gl =
let n = nb_prod thm_ty - nprod in
if n<0 then error "Apply: theorem has not enough premisses.";
let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
- Clenvtac.res_pf clause ~with_evars:with_evars gl in
+ Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in
try try_apply thm_ty0 concl_nprod
with PretypeError _|RefinerError _|UserError _|Failure _ as exn ->
let rec try_red_apply thm_ty =
@@ -573,14 +575,17 @@ let apply_with_ebindings_gen with_evars (c,lbind) gl =
else raise exn in
try_red_apply thm_ty0
-let apply_with_ebindings = apply_with_ebindings_gen false
-let eapply_with_ebindings = apply_with_ebindings_gen true
+let advanced_apply_with_ebindings = apply_with_ebindings_gen true false
+let advanced_eapply_with_ebindings = apply_with_ebindings_gen true true
+
+let apply_with_ebindings = apply_with_ebindings_gen false false
+let eapply_with_ebindings = apply_with_ebindings_gen false true
let apply_with_bindings (c,bl) =
apply_with_ebindings (c,inj_ebindings bl)
let eapply_with_bindings (c,bl) =
- apply_with_ebindings_gen true (c,inj_ebindings bl)
+ apply_with_ebindings_gen false true (c,inj_ebindings bl)
let apply c =
apply_with_ebindings (c,NoBindings)
@@ -589,7 +594,7 @@ let apply_list = function
| c::l -> apply_with_bindings (c,ImplicitBindings l)
| _ -> assert false
-(* Resolution with no reduction on the type *)
+(* Resolution with no reduction on the type (used ?) *)
let apply_without_reduce c gl =
let clause = mk_clenv_type_of gl c in
@@ -796,7 +801,7 @@ let constructor_tac expctdnumopt i lbind gl =
Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
check_number_of_constructors expctdnumopt i nconstr;
let cons = mkConstruct (ith_constructor_of_inductive mind i) in
- let apply_tac = apply_with_ebindings (cons,lbind) in
+ let apply_tac = advanced_apply_with_ebindings (cons,lbind) in
(tclTHENLIST
[convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c723c2b9a3..084aba9efa 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -172,12 +172,19 @@ val bring_hyps : named_context -> tactic
val apply : constr -> tactic
val apply_without_reduce : constr -> tactic
val apply_list : constr list -> tactic
-val apply_with_ebindings_gen : evars_flag -> constr with_ebindings -> tactic
+
+val apply_with_ebindings_gen :
+ advanced_flag -> evars_flag -> constr with_ebindings -> tactic
+
val apply_with_bindings : constr with_bindings -> tactic
-val apply_with_ebindings : constr with_ebindings -> tactic
val eapply_with_bindings : constr with_bindings -> tactic
+
+val apply_with_ebindings : constr with_ebindings -> tactic
val eapply_with_ebindings : constr with_ebindings -> tactic
+val advanced_apply_with_ebindings : constr with_ebindings -> tactic
+val advanced_eapply_with_ebindings : constr with_ebindings -> tactic
+
val cut_and_apply : constr -> tactic
val apply_in : evars_flag -> identifier -> constr with_ebindings list -> tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:20:11 +0000