coq/contrib/subtac/interp_fixpoint.ml, branch master The formal proof system Made pretyping a functor over a coercion implementation. Pretyping.Default uses the original Coercion implementation. 2006-03-22T15:36:58+00:00 msozeau 2006-03-22T15:36:58+00:00 10961655cb9c09da20cfe2ecc68def3d3b7d1bb5 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 
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
New files for subtac 2006-03-05T14:29:11+00:00 coq 2006-03-05T14:29:11+00:00 767cc0e73a7c394f77e3b9007a74dc5b4f2dd9ab git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8133 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8133 85f007b7-540e-0410-9357-904b9bb8a0f7