aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/reserve.ml
Commit message (Expand)AuthorAge
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Better behaviour for sets of reserved names.Gravatar Pierre-Marie Pédrot2014-03-01
* Never suppress the typing constraint of bound variables whose name wasGravatar Pierre-Marie Pédrot2014-03-01
* Notations can now accept dummy arguments. If ever a bound variable is notGravatar Pierre-Marie Pédrot2013-12-22
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Replacing uses of association lists by maps in notations.Gravatar ppedrot2013-08-03
* Getting rid of module Gmapl.Gravatar ppedrot2013-05-09
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (interp)Gravatar ppedrot2012-11-25
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Stuff about notation_constr (ex-aconstr) now in notation_ops.mlGravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* Fixing failing printer when the type of a binder name with implicitGravatar herbelin2011-10-24
* Rather quick hack to avoid using notations involving "Type" whenGravatar herbelin2011-06-12
* Added a table for using reserved names for binding names to typesGravatar herbelin2011-03-05
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Add information of localisation when an error involving an "implicitGravatar herbelin2010-11-07
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Pas d'escamotage des noms réservés si Set Printing All actibvéGravatar herbelin2006-12-08