diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-01 18:59:04 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-01 18:59:04 +0000 |
| commit | 15cb1aace0460e614e8af1269d874dfc296687b0 (patch) | |
| tree | 87f3c4237d3ef3dd9b34af8a4c8f2772f470243d /toplevel/libtypes.mli | |
| parent | 70d8c1e7a24b542c8e3f1788fd18226e2469801b (diff) | |
Univ: a univ_depends function to avoid a hack in Inductiveops
univ_depends checks whether a universe variable appears or
is equal to a universe. In comparison with the previous hack
in inductiveops based on try...catching UniverseInconsistency,
this should be semantically equivalent, simplier, and more
robust in case we allow someday an unsafe mode where
merge_constraints would be a no-op.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15013 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/libtypes.mli')
0 files changed, 0 insertions, 0 deletions