aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
AgeCommit message (Expand)Author
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-03-02Noise for nothingpboutill
2011-05-05Definitions of positive, N, Z moved in Numbers/BinNums.vletouzey
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-11-02Move stuff about positive into a distinct PArith subdirletouzey
2010-10-14Reparation du parseur/printer de nombres BigNletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-11-12Repair interpretation of numeral for BigQ, add a printer (close #2160)letouzey
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-28Fix static compilation of numeral syntax (typo in _mod files, sorry ...)letouzey
2009-03-27Parsing files for numerals (+ ascii/string) moved into pluginsletouzey