aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_xml.ml4
AgeCommit message (Expand)Author
2015-07-22Removing the G_xml module again.Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-08-01Continuing (incomplete) cleaning of Inductiveops.Hugo Herbelin
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-01-30G_xml: remove some duplication in error fonctionsPierre Letouzey
2014-01-30G_xml: protect against some possible Not_foundPierre Letouzey
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 9)letouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (parsing)ppedrot
2012-11-13More monomorphizationsppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-02Glob_term.predicate_pattern: No number of parameters with letins.pboutill
2012-03-02Noise for nothingpboutill
2012-01-16Inductiveops.nb_*{,_env} cleaningpboutill
2011-11-07Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsletouzey
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19static (and shared) camlp4use instead of per-file declarationletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-08Some dead code removal + cleanupsletouzey
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-07-16Generalized CAMLP4USE for pp dependenciescorbinea
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2006-10-03le parsing du LETIN ne suivait pas la DTD (bug #1237)herbelin
2006-07-05Nettoyage code mortherbelin
2006-06-22Added {measure x f} as a valid recursion order.msozeau
2006-05-29The "clean integration of subtac" patch.msozeau