| Age | Commit message (Collapse) | Author |
|---|
|
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Makefile: Option (environment variable NO_RECOMPILE_LIB) to not
recompile the whole standard library just because the coq binaries
got rebuilt.
- Infrastructure to change the object pretty-printers at runtime.
- Use that infrastructure to make coqtop-protocol with Pcoq trees and
Pcoq-protocol with pretty-printed terms possible in coq-interface.
- Make "Back(track)" into closed sections, modules and module types
"Just Work™".
- Modernise/generalise Pcoq protocol a bit, make some of its warts
optional.
- Implement "Show." in Pcoq mode.
- Add Rpow_def.vo to REALSBASEVO so that its dependencies are
computed (and used).
- "make revision" now handles GNU Arch / tla in addition to svn.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9476 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Modifies the behavior of Recursive definition to produce goals instead of
established theorems
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7843 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
et d'"externalisation"; standardisation du nom des fonctions d'affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
in theorems were renamed to avoid the names present in the current goal's
context. This version corrects this problem.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2425 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dependence files are updated accordingly.
Modifications in other files to cope with a few errors in the translation for
the parser (mostly around records, coercions, and the search-pattern command).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1599 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1531 85f007b7-540e-0410-9357-904b9bb8a0f7
|
