coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Parsing files for numerals (+ ascii/string) moved into plugins	letouzey	2009-03-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Idea: make coqtop more independant of the standard library. In the future, we can imagine loading the syntax for numerals right after their definition. For the moment, it is easier to stay lazy and load the syntax plugins slightly before the definitions. After this commit, the main (sole ?) references to theories/ from the core ml files are in Coqlib (but many parts of coqlib are only used by plugins), and it mainly concerns Init (+ Logic/JMeq and maybe a few others). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12024 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
\| \| \| \| \| \| \| \| \| \|	majuscule - si pas un ident ou un terme - et se terminent par un point). Restent quelques utilisations de "error" qui sont liées à des usages internes, ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix the number parsing/printing for BigN/BigZ/BigQ	letouzey	2008-06-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* In order to get via a "SearchAbout bigZ" all the generic lemmas that are now available, I moved bigZ to a notation for BigZ.t instead of a definition. But this notation was interacting badly with the number parsing. * Moreover, I also discovered that printing was broken as well, due to a reference to obsolete name Basic_type (now DoubleType) that I forgot to adapt in g_intsyntax. * Last but not least, there was also a bug not due to myself that was probably preventing parsing/printing _very_ big numbers (the ones for which generic constructor BigN.Nn is used): this Nn is the 7-th constructor, not the 13-th. In addition, the first argument to Nn was supposed to be automatically inferred, this was not working, so we build it now explicitely (very easy). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11087 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Integration of theories/Ints into theories/Numbers, part 1: moving files	letouzey	2008-05-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	For the moment, the Ints files are simply moved into directories in theories/Numbers with meaningful names. No filenames changed, apart from: Zaux.v -> theories/Numbers/BigNumPrelude.v MemoFn.v -> theories/Lists/StreamMemo.v More to come... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10899 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
\| \| \| \| \| \| \| \|	pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding BigQ and proofs	thery	2007-10-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10265 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrected the treatment of negative numbers for the bigZ parser. And	aspiwack	2007-05-29
\| \| \| \| \| \| \| \|	corrected a small typo in an error message (bogN instead of bigN). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9870 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added Z and Q implementations with int31.	aspiwack	2007-05-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9846 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du pretty-printing des big-int (la sous-fonction get_height	aspiwack	2007-05-15
\| \| \| \| \| \| \| \| \|	faisait n'importe quoi). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9825 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
	details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7