diff options
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | test-suite/success/apply.v | 28 |
2 files changed, 26 insertions, 6 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5123aed9ca..43093ba12f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1109,8 +1109,10 @@ let make_projection env sigma params cstr sign elim i n c u = if (* excludes dependent projection types *) noccur_between 1 (n-i-1) t - (* excludes flexible projection types *) + (* to avoid surprising unifications, excludes flexible + projection types or lambda which will be instantiated by Meta/Evar *) && not (isEvar (fst (whd_betaiota_stack sigma t))) + && not (isRel t && destRel t > n-i) then let t = lift (i+1-n) t in let abselim = beta_applist (elim,params@[t;branch]) in diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 25367a10fe..29c9ab95ff 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -336,25 +336,43 @@ Qed. (* From 12612, descent in conjunctions is more powerful *) (* The following, which was failing badly in bug 1980, is now properly rejected, as descend in conjunctions builds an - ill-formed elimination from Prop to Type. *) + ill-formed elimination from Prop to Type. + + Added Aug 2014: why it fails is now that trivial unification ?x = goal is + rejected by the descent in conjunctions to avoid surprising results. *) Goal True. Fail eapply ex_intro. exact I. Qed. -(* The following, which were not accepted, are now accepted as - expected by descent in conjunctions *) +Goal True. +Fail eapply (ex_intro _). +exact I. +Qed. + +(* Note: the following succeed directly (i.e. w/o "exact I") since + Aug 2014 since the descent in conjunction does not use a "cut" + anymore: the iota-redex is contracted and we get rid of the + uninstantiated evars + + Is it good or not? Maybe it does not matter so much. Goal True. eapply (ex_intro (fun _ => True) I). -exact I. +exact I. (* Not needed since Aug 2014 *) +Qed. + +Goal True. +eapply (ex_intro (fun _ => True) I _). +exact I. (* Not needed since Aug 2014 *) Qed. Goal True. eapply (fun (A:Prop) (x:A) => conj I x). -exact I. +exact I. (* Not needed since Aug 2014 *) Qed. +*) (* The following was not accepted from r12612 to r12657 *) |