diff options
| author | letouzey | 2013-03-12 23:59:20 +0000 |
|---|---|---|
| committer | letouzey | 2013-03-12 23:59:20 +0000 |
| commit | 7be6f0291c7d1a60bcd33e1086ed45414b7e9568 (patch) | |
| tree | 782e252d64b26420b0dec60e66e9402ca97a653a /kernel | |
| parent | 0e7855095be6f06d1dcf563a9036b79e20172d28 (diff) | |
Equality: avoid an anomaly about inj_pair2_eq_dec
In coming commits, we'll restrict (try ... with ...), in particular
to avoid catching anomalies. Currently, an anomaly about inj_pair2_eq_dec
is raised and catched, let's avoid that by ensuring that Eqdep_dec is
loaded before entering the critical code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16273 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions