diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-29 19:59:11 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-29 19:59:11 +0000 |
| commit | af354d63a814b0855eefda81852029d72b3544db (patch) | |
| tree | ef2fdf48eaea7e0690ac69cf9bc9b988c30bf11d /library/library.ml | |
| parent | ba0bfcafe850586d72ad0b06db19d8de429d1caf (diff) | |
The "clean integration of subtac" patch.
Adds a new kind of casts (CastCoerce) for coercing an object to its base type (e.g. inductive).
The new cast_type type subsumes usual casts ConvCasts. Much of the patch is just adding ConvCasts where needed.
The Pretyping module has been adapted to this change, although it doesn't change anything yet, but this construct could have
a use with current coercions also. Pretyping is also cleaned from the "Use type constraints under lambdas" patch which is not yet ready
for wide use. It has been transferred to a copy of the Pretyping Functor in subtac_pretyping_F.ml.
Subtac is now working as well as I demonstrated at TYPES.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8875 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/library.ml')
0 files changed, 0 insertions, 0 deletions