aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--tactics/tactics.ml30
-rw-r--r--test-suite/bugs/closed/7779.v15
2 files changed, 32 insertions, 13 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b571b347d..fc73e4d40 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2645,6 +2645,15 @@ let insert_before decls lasthyp env =
push_named d env)
~init:(reset_context env) env
+let mk_eq_name env id {CAst.loc;v=ido} =
+ match ido with
+ | IntroAnonymous -> fresh_id_in_env (Id.Set.singleton id) (add_prefix "Heq" id) env
+ | IntroFresh heq_base -> fresh_id_in_env (Id.Set.singleton id) heq_base env
+ | IntroIdentifier id ->
+ if List.mem id (ids_of_named_context (named_context env)) then
+ user_err ?loc (Id.print id ++ str" is already used.");
+ id
+
(* unsafe *)
let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
@@ -2654,14 +2663,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
else LocalAssum (id,t)
in
match with_eq with
- | Some (lr,{CAst.loc;v=ido}) ->
- let heq = match ido with
- | IntroAnonymous -> fresh_id_in_env (Id.Set.singleton id) (add_prefix "Heq" id) env
- | IntroFresh heq_base -> fresh_id_in_env (Id.Set.singleton id) heq_base env
- | IntroIdentifier id ->
- if List.mem id (ids_of_named_context (named_context env)) then
- user_err ?loc (Id.print id ++ str" is already used.");
- id in
+ | Some (lr,heq) ->
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
@@ -4396,7 +4398,8 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
match res with
| None ->
(* pattern not found *)
- let with_eq = Option.map (fun eq -> (false,eq)) eqname in
+ let with_eq = Option.map (fun eq -> (false,mk_eq_name env id eq)) eqname in
+ let inhyps = if List.is_empty inhyps then inhyps else Option.fold_left (fun inhyps (_,heq) -> heq::inhyps) inhyps with_eq in
(* we restart using bindings after having tried type-class
resolution etc. on the term given by the user *)
let flags = tactic_infer_flags (with_evars && (* do not give a success semantics to edestruct on an open term yet *) false) in
@@ -4421,21 +4424,22 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
else Proofview.tclUNIT ();
if isrec then Proofview.cycle (-1) else Proofview.tclUNIT ()
])
- tac
+ (tac inhyps)
in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac
| Some (sigma', c) ->
(* pattern found *)
- let with_eq = Option.map (fun eq -> (false,eq)) eqname in
(* TODO: if ind has predicate parameters, use JMeq instead of eq *)
let env = reset_with_named_context sign env in
+ let with_eq = Option.map (fun eq -> (false,mk_eq_name env id eq)) eqname in
+ let inhyps = if List.is_empty inhyps then inhyps else Option.fold_left (fun inhyps (_,heq) -> heq::inhyps) inhyps with_eq in
let tac =
Tacticals.New.tclTHENLIST [
Refine.refine ~typecheck:false begin fun sigma ->
mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None
end;
- tac
+ (tac inhyps)
]
in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma') tac
@@ -4485,7 +4489,7 @@ let induction_gen clear_flag isrec with_evars elim
pose_induction_arg_then
isrec with_evars info_arg elim id arg t inhyps cls
(induction_with_atomization_of_ind_arg
- isrec with_evars elim names id inhyps)
+ isrec with_evars elim names id)
end
(* Induction on a list of arguments. First make induction arguments
diff --git a/test-suite/bugs/closed/7779.v b/test-suite/bugs/closed/7779.v
new file mode 100644
index 000000000..78936b595
--- /dev/null
+++ b/test-suite/bugs/closed/7779.v
@@ -0,0 +1,15 @@
+(* Checking that the "in" clause takes the "eqn" clause into account *)
+
+Definition test (x: nat): {y: nat | False }. Admitted.
+
+Parameter x: nat.
+Parameter z: nat.
+
+Goal
+ proj1_sig (test x) = z ->
+ False.
+Proof.
+ intro H.
+ destruct (test x) eqn:Heqs in H.
+ change (test x = exist (fun _ : nat => False) x0 f) in Heqs. (* Check it has the expected statement *)
+Abort.