diff options
| author | Pierre-Marie Pédrot | 2017-08-23 12:37:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-08 20:46:08 +0200 |
| commit | a9f8fa56e76aa557b1391cb9709cb893a4f602ce (patch) | |
| tree | 9ef357486083ebefa0a9b2ef328270b74f5dad93 /dev/doc/xml-protocol.md | |
| parent | b1fbec7e3945fe2965f4ba9f80c8c31b821dbce1 (diff) | |
Using EConstr equality check in unification.
The code from Universes what essentially a duplicate of the one from EConstr,
but they were copied for historical reasons. Now, this is not useful anymore,
so that we remove the implementation from Universes and rely on the one from
EConstr.
Diffstat (limited to 'dev/doc/xml-protocol.md')
0 files changed, 0 insertions, 0 deletions