aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/modules
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-31 18:58:15 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-31 18:58:15 +0000
commit3aad12391a9566af41395c674614e56383dff8c2 (patch)
treeeaf8d45f840bda673030e93946cf41487e357c2b /test-suite/modules
parent6d10a4751154cfb8149398d37c8dbde775adbf1c (diff)
As remarked by Enrico, we'd better use eq_constr than structural equality
(it is a priori optimized but also able to reason modulo equality of names and modulo alpha-conversion). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13945 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/modules')
0 files changed, 0 insertions, 0 deletions