aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_natsyntax.mli
AgeCommit message (Collapse)Author
2011-12-08Makefile: force the installation of all .cmi (and remove some obsolete .mli)letouzey
The previous code wasn't detecting and installing .cmi coming from .mli without corresponding .ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14783 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-10Fix the number parsing/printing for BigN/BigZ/BigQletouzey
* 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
2004-07-16Nouvelle en-tĂȘteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-03compilation nativefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@201 85f007b7-540e-0410-9357-904b9bb8a0f7