| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8964 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Also enclose traces with try with clauses to avoid detypinging anomalies.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8889 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
(previous and current version work).
Changed the type of typing constraints so as to have all the necessary information on abstract tycons.
Updates of subtac to use the new type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8693 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists.
Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop.
- Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
uses the original Coercion implementation.
Updated contributions that called pretyping to use the default impl.
Also update subtac using the functor, do some renamings and add interfaces for all files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
|
