| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-01 | [flags] Remove XML output flag. | Emilio Jesus Gallego Arias | |
| This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied. | |||
| 2015-10-13 | Fix some typos. | Guillaume Melquiond | |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross | |
| It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar). | |||
| 2006-02-23 | Nettoyage de l'archive doc et restructuration avant intégration à l'archive | herbelin | |
| principale de Coq et publication des sources (HH) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8606 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |