aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
diff options
context:
space:
mode:
authorHugo Herbelin2017-05-24 21:55:21 +0200
committerHugo Herbelin2017-05-30 15:08:22 +0200
commitbbde815f8108f4641f5411d03f7a88096cc2221b (patch)
treebc46ccddc767bb65bf836fd978b5779d4b2e3d78 /test-suite/success
parent5a86aabf4375b5f6f205dd328454748d2bc1217f (diff)
Support for using type information to infer more precise evar sources.
This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted).
Diffstat (limited to 'test-suite/success')
-rw-r--r--test-suite/success/Abstract.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v
index ffd50f6efd..69dc9aca78 100644
--- a/test-suite/success/Abstract.v
+++ b/test-suite/success/Abstract.v
@@ -1,4 +1,3 @@
-
(* Cf coqbugs #546 *)
Require Import Omega.