aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli17
-rw-r--r--CHANGES2
-rw-r--r--dev/doc/changes.md6
-rw-r--r--plugins/funind/invfun.ml9
-rw-r--r--plugins/ltac/extratactics.ml430
-rw-r--r--plugins/ssr/ssrelim.ml2
-rw-r--r--tactics/eqdecide.ml8
-rw-r--r--tactics/equality.ml93
-rw-r--r--tactics/equality.mli24
-rw-r--r--tactics/inv.ml2
-rw-r--r--test-suite/bugs/closed/5281.v6
-rw-r--r--vernac/auto_ind_decl.ml17
12 files changed, 139 insertions, 77 deletions
diff --git a/API/API.mli b/API/API.mli
index a41009fa2..5e41464c8 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5337,6 +5337,11 @@ sig
| Naive
| FirstSolved
| AllMatches
+ type inj_flags = {
+ keep_proof_equalities : bool; (* One may want it or not *)
+ injection_in_context : bool; (* For regularity; one may want it from ML code but not interactively *)
+ injection_pattern_l2r_order : bool; (* Compatibility option: no reason not to want it *)
+ }
val build_selector :
Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types ->
@@ -5345,20 +5350,20 @@ sig
val general_rewrite :
orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag ->
?tac:(unit Proofview.tactic * conditions) -> EConstr.constr -> unit Proofview.tactic
- val inj : Tactypes.intro_patterns option -> Misctypes.evars_flag ->
+ val inj : inj_flags option -> Tactypes.intro_patterns option -> Misctypes.evars_flag ->
Misctypes.clear_flag -> EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic
val general_multi_rewrite :
Misctypes.evars_flag -> (bool * Misctypes.multi * Misctypes.clear_flag * Tactypes.delayed_open_constr_with_bindings) list ->
Locus.clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
val replace_in_clause_maybe_by : EConstr.constr -> EConstr.constr -> Locus.clause -> unit Proofview.tactic option -> unit Proofview.tactic
val replace_term : bool option -> EConstr.constr -> Locus.clause -> unit Proofview.tactic
- val dEq : Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
+ val dEq : keep_proofs:bool option -> Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
val discr_tac : Misctypes.evars_flag ->
EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
- val injClause : Tactypes.intro_patterns option -> Misctypes.evars_flag ->
+ val injClause : inj_flags option -> Tactypes.intro_patterns option -> Misctypes.evars_flag ->
EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
- val simpleInjClause : Misctypes.evars_flag ->
+ val simpleInjClause : inj_flags option -> Misctypes.evars_flag ->
EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option ->
unit Proofview.tactic
val rewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic
@@ -5392,8 +5397,8 @@ sig
?tac:(unit Proofview.tactic * conditions) -> EConstr.constr Misctypes.with_bindings -> Misctypes.evars_flag -> unit Proofview.tactic
val discriminable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val discrHyp : Names.Id.t -> unit Proofview.tactic
- val injectable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
- val injHyp : Misctypes.clear_flag -> Names.Id.t -> unit Proofview.tactic
+ val injectable : Environ.env -> Evd.evar_map -> keep_proofs:(bool option) -> EConstr.constr -> EConstr.constr -> bool
+ val injHyp : inj_flags option -> Misctypes.clear_flag -> Names.Id.t -> unit Proofview.tactic
val subst_gen : bool -> Names.Id.t list -> unit Proofview.tactic
end
diff --git a/CHANGES b/CHANGES
index 640ab4aa5..7a326c589 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,8 @@ Tactics
such as "x := 5 : Z" (see BZ#148). This could be disabled via
Unset Omega UseLocalDefs.
- The tactic "romega" is also aware now of the bodies of context variables.
+- Tactic "decide equality" now able to manage constructors which
+ contain proofs.
Changes from 8.7+beta2 to 8.7.0
===============================
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 8a2a2fffc..6ade6576f 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -32,6 +32,12 @@ We renamed the following datatypes:
- `Pp.std_ppcmds` -> `Pp.t`
+Some tactics and related functions now support static configurability, e.g.:
+
+- injectable, dEq, etc. takes an argument ~keep_proofs which,
+ - if None, tells to behave as told with the flag Keep Proof Equalities
+ - if Some b, tells to keep proof equalities iff b is true
+
## Changes between Coq 8.6 and Coq 8.7
### Ocaml
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 9cb2a0a3f..93317fce1 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -570,6 +570,11 @@ let rec reflexivity_with_destruct_cases g =
with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity
in
let eq_ind = make_eq () in
+ let my_inj_flags = Some {
+ Equality.keep_proof_equalities = false;
+ injection_in_context = false; (* for compatibility, necessary *)
+ injection_pattern_l2r_order = false; (* probably does not matter; except maybe with dependent hyps *)
+ } in
let discr_inject =
Tacticals.onAllHypsAndConcl (
fun sc g ->
@@ -580,8 +585,8 @@ let rec reflexivity_with_destruct_cases g =
| App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind ->
if Equality.discriminable (pf_env g) (project g) t1 t2
then Proofview.V82.of_tactic (Equality.discrHyp id) g
- else if Equality.injectable (pf_env g) (project g) t1 t2
- then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite] g
+ else if Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2
+ then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id);thin [id];intros_with_rewrite] g
else tclIDTAC g
| _ -> tclIDTAC g
)
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index a7aebf9e1..65c186a41 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -91,12 +91,12 @@ let elimOnConstrWithHoles tac with_evars c =
(fun c -> tac with_evars (Some (None,ElimOnConstr c)))
TACTIC EXTEND simplify_eq
- [ "simplify_eq" ] -> [ dEq false None ]
-| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq false c ]
+ [ "simplify_eq" ] -> [ dEq ~keep_proofs:None false None ]
+| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) false c ]
END
TACTIC EXTEND esimplify_eq
-| [ "esimplify_eq" ] -> [ dEq true None ]
-| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq true c ]
+| [ "esimplify_eq" ] -> [ dEq ~keep_proofs:None true None ]
+| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) true c ]
END
let discr_main c = elimOnConstrWithHoles discr_tac false c
@@ -117,31 +117,31 @@ let discrHyp id =
discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings)))
let injection_main with_evars c =
- elimOnConstrWithHoles (injClause None) with_evars c
+ elimOnConstrWithHoles (injClause None None) with_evars c
TACTIC EXTEND injection
-| [ "injection" ] -> [ injClause None false None ]
-| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) false c ]
+| [ "injection" ] -> [ injClause None None false None ]
+| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) false c ]
END
TACTIC EXTEND einjection
-| [ "einjection" ] -> [ injClause None true None ]
-| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) true c ]
+| [ "einjection" ] -> [ injClause None None true None ]
+| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) true c ]
END
TACTIC EXTEND injection_as
| [ "injection" "as" intropattern_list(ipat)] ->
- [ injClause (Some ipat) false None ]
+ [ injClause None (Some ipat) false None ]
| [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] ->
- [ mytclWithHoles (injClause (Some ipat)) false c ]
+ [ mytclWithHoles (injClause None (Some ipat)) false c ]
END
TACTIC EXTEND einjection_as
| [ "einjection" "as" intropattern_list(ipat)] ->
- [ injClause (Some ipat) true None ]
+ [ injClause None (Some ipat) true None ]
| [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] ->
- [ mytclWithHoles (injClause (Some ipat)) true c ]
+ [ mytclWithHoles (injClause None (Some ipat)) true c ]
END
TACTIC EXTEND simple_injection
-| [ "simple" "injection" ] -> [ simpleInjClause false None ]
-| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles simpleInjClause false c ]
+| [ "simple" "injection" ] -> [ simpleInjClause None false None ]
+| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles (simpleInjClause None) false c ]
END
let injHyp id =
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 832044909..26b5c5767 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -396,7 +396,7 @@ let revtoptac n0 gl =
let equality_inj l b id c gl =
let msg = ref "" in
- try Proofview.V82.of_tactic (Equality.inj l b None c) gl
+ try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
with
| Ploc.Exc(_,CErrors.UserError (_,s))
| CErrors.UserError (_,s)
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index d912decff..8764ef085 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -89,6 +89,12 @@ let mkBranches (eqonleft,mk,c1,c2,typ) =
clear_last;
intros]
+let inj_flags = Some {
+ Equality.keep_proof_equalities = true; (* necessary *)
+ Equality.injection_in_context = true; (* does not matter here *)
+ Equality.injection_pattern_l2r_order = true; (* does not matter here *)
+ }
+
let discrHyp id =
let c env sigma = (sigma, (mkVar id, NoBindings)) in
let tac c = Equality.discr_tac false (Some (None, ElimOnConstr c)) in
@@ -136,7 +142,7 @@ let eqCase tac =
let injHyp id =
let c env sigma = (sigma, (mkVar id, NoBindings)) in
- let tac c = Equality.injClause None false (Some (None, ElimOnConstr c)) in
+ let tac c = Equality.injClause inj_flags None false (Some (None, ElimOnConstr c)) in
Tacticals.New.tclDELAYEDWITHHOLES false c tac
let diseqCase hyps eqonleft =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index bb2de1904..7c03a3ba6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -48,6 +48,12 @@ module NamedDecl = Context.Named.Declaration
(* Options *)
+type inj_flags = {
+ keep_proof_equalities : bool;
+ injection_in_context : bool;
+ injection_pattern_l2r_order : bool;
+ }
+
let discriminate_introduction = ref true
let discr_do_intro () = !discriminate_introduction
@@ -63,7 +69,9 @@ let _ =
let injection_pattern_l2r_order = ref true
-let use_injection_pattern_l2r_order () = !injection_pattern_l2r_order
+let use_injection_pattern_l2r_order = function
+ | None -> !injection_pattern_l2r_order
+ | Some flags -> flags.injection_pattern_l2r_order
let _ =
declare_bool_option
@@ -75,9 +83,9 @@ let _ =
let injection_in_context = ref false
-let use_injection_in_context () =
- !injection_in_context
- && Flags.version_strictly_greater Flags.V8_5
+let use_injection_in_context = function
+ | None -> !injection_in_context && Flags.version_strictly_greater Flags.V8_5
+ | Some flags -> flags.injection_in_context
let _ =
declare_bool_option
@@ -721,7 +729,14 @@ let _ =
optread = (fun () -> !keep_proof_equalities_for_injection) ;
optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
-let find_positions env sigma ~no_discr t1 t2 =
+let keep_proof_equalities = function
+ | None -> !keep_proof_equalities_for_injection
+ | Some flags -> flags.keep_proof_equalities
+
+(* [keep_proofs] is relevant for types in Prop with elimination in Type *)
+(* In particular, it is relevant for injection but not for discriminate *)
+
+let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
let project env sorts posn t1 t2 =
let ty1 = get_type_of env sigma t1 in
let s = get_sort_family_of env sigma ty1 in
@@ -768,20 +783,22 @@ let find_positions env sigma ~no_discr t1 t2 =
project env sorts posn t1_0 t2_0
in
try
- let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp]
- else [InSet;InType]
- in
+ let sorts = if keep_proofs then [InSet;InType;InProp] else [InSet;InType] in
Inr (findrec sorts [] t1 t2)
with DiscrFound (path,c1,c2) ->
Inl (path,c1,c2)
+let use_keep_proofs = function
+ | None -> !keep_proof_equalities_for_injection
+ | Some b -> b
+
let discriminable env sigma t1 t2 =
- match find_positions env sigma ~no_discr:false t1 t2 with
+ match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with
| Inl _ -> true
| _ -> false
-let injectable env sigma t1 t2 =
- match find_positions env sigma ~no_discr:true t1 t2 with
+let injectable env sigma ~keep_proofs t1 t2 =
+ match find_positions env sigma ~keep_proofs:(use_keep_proofs keep_proofs) ~no_discr:true t1 t2 with
| Inl _ -> assert false
| Inr [] | Inr [([],_,_)] -> false
| Inr _ -> true
@@ -1024,7 +1041,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- match find_positions env sigma ~no_discr:false t1 t2 with
+ match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with
| Inr _ ->
tclZEROMSG (str"Not a discriminable equality.")
| Inl (cpath, (_,dirn), _) ->
@@ -1078,9 +1095,7 @@ let discrEverywhere with_evars =
(fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
else (* <= 8.2 compat *)
tryAllHypsAndConcl (discrSimpleClause with_evars))
-(* (fun gls ->
- user_err ~hdr:"DiscrEverywhere" (str"No discriminable equalities."))
-*)
+
let discr_tac with_evars = function
| None -> discrEverywhere with_evars
| Some c -> onInductionArg (fun clear_flag -> discr with_evars) c
@@ -1402,15 +1417,15 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
(if l2r then List.rev injectors else injectors)))
(tac (List.length injectors)))
-let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
+let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
let env = eq_clause.env in
- match find_positions env sigma ~no_discr:true t1 t2 with
+ match find_positions env sigma ~keep_proofs ~no_discr:true t1 t2 with
| Inl _ ->
assert false
| Inr [] ->
let suggestion =
- if !keep_proof_equalities_for_injection then
+ if keep_proofs then
"" else
" You can try to use option Set Keep Proof Equalities." in
tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
@@ -1429,13 +1444,13 @@ let get_previous_hyp_position id gl =
in
aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
-let injEq ?(old=false) with_evars clear_flag ipats =
+let injEq flags ?(old=false) with_evars clear_flag ipats =
(* Decide which compatibility mode to use *)
let ipats_style, l2r, dft_clear_flag, bounded_intro = match ipats with
- | None when not old && use_injection_in_context () ->
+ | None when not old && use_injection_in_context flags ->
Some [], true, true, true
| None -> None, false, false, false
- | _ -> let b = use_injection_pattern_l2r_order () in ipats, b, b, b in
+ | _ -> let b = use_injection_pattern_l2r_order flags in ipats, b, b, b in
(* Built the post tactic depending on compatibility mode *)
let post_tac c n =
match ipats_style with
@@ -1455,26 +1470,26 @@ let injEq ?(old=false) with_evars clear_flag ipats =
tclTHEN clear_tac intro_tac
end
| None -> tclIDTAC in
- injEqThen post_tac l2r
+ injEqThen (keep_proof_equalities flags) post_tac l2r
-let inj ipats with_evars clear_flag = onEquality with_evars (injEq with_evars clear_flag ipats)
+let inj flags ipats with_evars clear_flag = onEquality with_evars (injEq flags with_evars clear_flag ipats)
-let injClause ipats with_evars = function
- | None -> onNegatedEquality with_evars (injEq with_evars None ipats)
- | Some c -> onInductionArg (inj ipats with_evars) c
+let injClause flags ipats with_evars = function
+ | None -> onNegatedEquality with_evars (injEq flags with_evars None ipats)
+ | Some c -> onInductionArg (inj flags ipats with_evars) c
-let simpleInjClause with_evars = function
- | None -> onNegatedEquality with_evars (injEq ~old:true with_evars None None)
- | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq ~old:true with_evars clear_flag None)) c
+let simpleInjClause flags with_evars = function
+ | None -> onNegatedEquality with_evars (injEq flags ~old:true with_evars None None)
+ | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq flags ~old:true with_evars clear_flag None)) c
-let injConcl = injClause None false None
-let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.tag id)))
+let injConcl flags = injClause flags None false None
+let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent (Loc.tag id)))
-let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
+let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause =
Proofview.Goal.enter begin fun gl ->
let sigma = clause.evd in
let env = Proofview.Goal.env gl in
- match find_positions env sigma ~no_discr:false t1 t2 with
+ match find_positions env sigma ~keep_proofs ~no_discr:false t1 t2 with
| Inl (cpath, (_,dirn), _) ->
discr_positions env sigma u clause cpath dirn
| Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
@@ -1484,18 +1499,18 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
(ntac (clenv_value clause))
end
-let dEqThen with_evars ntac = function
- | None -> onNegatedEquality with_evars (decompEqThen (ntac None))
- | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (ntac clear_flag))) c
+let dEqThen ~keep_proofs with_evars ntac = function
+ | None -> onNegatedEquality with_evars (decompEqThen (use_keep_proofs keep_proofs) (ntac None))
+ | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (use_keep_proofs keep_proofs) (ntac clear_flag))) c
-let dEq with_evars =
- dEqThen with_evars (fun clear_flag c x ->
+let dEq ~keep_proofs with_evars =
+ dEqThen ~keep_proofs with_evars (fun clear_flag c x ->
(apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
let intro_decomp_eq tac data (c, t) =
Proofview.Goal.enter begin fun gl ->
let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in
- decompEqThen (fun _ -> tac) data cl
+ decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl
end
let _ = declare_intro_decomp_eq intro_decomp_eq
diff --git a/tactics/equality.mli b/tactics/equality.mli
index a4d1c0f9b..65da2e7dc 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -67,23 +67,31 @@ val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.ta
val replace : constr -> constr -> unit Proofview.tactic
val replace_by : constr -> constr -> unit Proofview.tactic -> unit Proofview.tactic
+type inj_flags = {
+ keep_proof_equalities : bool; (* One may want it or not *)
+ injection_in_context : bool; (* For regularity; one may want it from ML code but not interactively *)
+ injection_pattern_l2r_order : bool; (* Compatibility option: no reason not to want it *)
+ }
+
val discr : evars_flag -> constr with_bindings -> unit Proofview.tactic
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
-val inj : intro_patterns option -> evars_flag ->
+
+(* 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 : intro_patterns option -> evars_flag ->
+val injClause : inj_flags option -> intro_patterns option -> evars_flag ->
constr with_bindings destruction_arg option -> unit Proofview.tactic
-val injHyp : clear_flag -> Id.t -> unit Proofview.tactic
-val injConcl : unit Proofview.tactic
-val simpleInjClause : evars_flag ->
+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
-val dEq : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic
-val dEqThen : 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 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 make_iterated_tuple :
env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr)
@@ -100,7 +108,7 @@ val rewriteInConcl : bool -> constr -> unit Proofview.tactic
val discriminable : env -> evar_map -> constr -> constr -> bool
(* Tells if tactic "injection" is applicable *)
-val injectable : env -> evar_map -> constr -> constr -> bool
+val injectable : env -> evar_map -> keep_proofs:(bool option) -> constr -> constr -> bool
(* Subst *)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index f391382bf..c5aa74ba5 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -371,7 +371,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
(* If no immediate variable in the equation, try to decompose it *)
(* and apply a trailer which again try to substitute *)
(fun id ->
- dEqThen false (deq_trailer id)
+ dEqThen ~keep_proofs:None false (deq_trailer id)
(Some (None,ElimOnConstr (EConstr.mkVar id,NoBindings))))
id
diff --git a/test-suite/bugs/closed/5281.v b/test-suite/bugs/closed/5281.v
new file mode 100644
index 000000000..03bafdc9a
--- /dev/null
+++ b/test-suite/bugs/closed/5281.v
@@ -0,0 +1,6 @@
+Inductive A (T : Prop) := B (_ : T).
+Scheme Equality for A.
+
+Goal forall (T:Prop), (forall x y : T, {x=y}+{x<>y}) -> forall x y : A T, {x=y}+{x<>y}.
+decide equality.
+Qed.
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 503508fc0..7af391758 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -91,6 +91,15 @@ let destruct_on_using c id =
let destruct_on_as c l =
destruct false None c (Some (Loc.tag l)) None
+let inj_flags = Some {
+ Equality.keep_proof_equalities = true; (* necessary *)
+ injection_in_context = true; (* does not matter here *)
+ Equality.injection_pattern_l2r_order = true; (* does not matter here *)
+ }
+
+let my_discr_tac = Equality.discr_tac false None
+let my_inj_tac x = Equality.inj inj_flags None false None (EConstr.mkVar x,NoBindings)
+
(* reconstruct the inductive with the correct de Bruijn indexes *)
let mkFullInd (ind,u) n =
let mib = Global.lookup_mind (fst ind) in
@@ -595,7 +604,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
intro_using freshz;
intros;
Tacticals.New.tclTRY (
- Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None)
+ Tacticals.New.tclORELSE reflexivity my_discr_tac
);
simpl_in_hyp (freshz,Locus.InHyp);
(*
@@ -739,9 +748,9 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
intro_using freshz;
intros;
Tacticals.New.tclTRY (
- Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None)
+ Tacticals.New.tclORELSE reflexivity my_discr_tac
);
- Equality.inj None false None (EConstr.mkVar freshz,NoBindings);
+ my_inj_tac freshz;
intros; simpl_in_concl;
Auto.default_auto;
Tacticals.New.tclREPEAT (
@@ -936,7 +945,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
NoBindings
)
true;
- Equality.discr_tac false None
+ my_discr_tac
]
end
]
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 11:51:15 +0000