From 10a6452c6bbf618428591d9c40aed945f7fe92b3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 26 Apr 2018 14:45:45 +0200 Subject: Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars. --- test-suite/success/evars.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'test-suite/success') diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 5b13f35d5..253b48e4d 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -421,3 +421,8 @@ Goal exists n : nat, n = n -> True. eexists. set (H := _ = _). Abort. + +(* Check interpretation of default evar instance in pretyping *) +(* (reported as bug #7356) *) + +Check fun (P : nat -> Prop) (x:nat) (h:P x) => exist _ ?[z] (h : P ?z). -- cgit v1.2.3