| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2006-03-22 | Made pretyping a functor over a coercion implementation. Pretyping.Default ↵ | msozeau | |
| 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 | |||
| 2006-03-05 | New files for subtac | coq | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8133 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |