diff options
| -rw-r--r-- | library/lib.ml | 4 | ||||
| -rw-r--r-- | test-suite/success/setoid_test.v | 14 |
2 files changed, 16 insertions, 2 deletions
diff --git a/library/lib.ml b/library/lib.ml index 7135a93cc..dfe00fae5 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -575,11 +575,11 @@ let close_section id = | oname,OpenedSection (_,fs) -> let id' = basename (fst oname) in if id <> id' then - errorlabstrm "close_section" (str "last opened section is " ++ pr_id id'); + errorlabstrm "close_section" (str "Last opened section is " ++ pr_id id' ++ str "."); (oname,fs) | _ -> assert false with Not_found -> - error "no opened section" + error "No opened section." in let (secdecls,secopening,before) = split_lib oname in lib_stk := before; diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index f49f58e5a..be5999df5 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -116,3 +116,17 @@ Add Morphism (@f A) : f_morph. Proof. unfold rel, f. trivial. Qed. + +(* Submitted by Nicolas Tabareau *) +(* Needs unification.ml to support environments with de Bruijn *) + +Goal forall + (f : Prop -> Prop) + (Q : (nat -> Prop) -> Prop) + (H : forall (h : nat -> Prop), Q (fun x : nat => f (h x)) <-> True) + (h:nat -> Prop), + Q (fun x : nat => f (Q (fun b : nat => f (h x)))) <-> True. +intros f0 Q H. +setoid_rewrite H. +tauto. +Qed. |