diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-10 18:05:09 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-10 18:05:09 +0000 |
| commit | 2d8c70b3380d899c2717d00f2f27b4c6aefa2322 (patch) | |
| tree | 9efb666763308bb6c72c831490331b3cec380e9e /toplevel | |
| parent | 461a5a2093f8e46708e01a27993f80919e20d4aa (diff) | |
Remove obsolete TheoryList
This library is no longer used anywhere, and its contents is
very... let's say historical... More seriously, many (and presumably
the most useful) stuff that used to be there are in List, now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13828 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/indschemes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index f7ff2013b..52c9be675 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -167,7 +167,7 @@ let declare_beq_scheme_with l kn = try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn let try_declare_beq_scheme kn = - (* TODO: handle Fix, see e.g. TheoryList.In_spec, eventually handle + (* TODO: handle Fix, eventually handle proof-irrelevance; improve decidability by depending on decidability for the parameters rather than on the bl and lb properties *) try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelVerbose [] kn |