aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/record.ml
Commit message (Expand)AuthorAge
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (toplevel)Gravatar ppedrot2012-11-26
* Taking into account the type of a definition (if it exists), and theGravatar herbelin2012-11-17
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* 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
* Separated notice vs info messages, and cleaned up the interface a bit.Gravatar ppedrot2012-06-04
* Cleaning Pp.ppnl useGravatar ppedrot2012-06-01
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Basic stuff about constr_expr migrated from topconstr to constrexpr_opsGravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlGravatar letouzey2012-05-29
* Better error message when defining recursive records with Record orGravatar aspiwack2012-04-13
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Noise for nothingGravatar pboutill2012-03-02
* Check for unresolved evars in textual order of the params and fields declarat...Gravatar msozeau2012-01-25
* Proof using ...Gravatar gareuselesinge2011-12-12
* Restore backward compatibility. ":>" declares subinstances in Class declarati...Gravatar msozeau2011-11-18
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* Fixing bug #2181 (Class mechanism can create dependencies over unnamedGravatar herbelin2011-06-14
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Keep information on which fields are subclasses in class declarations,Gravatar msozeau2011-03-11
* Interp a definition with the implicit arguments of its local contextGravatar pboutill2011-02-10
* Data structure telling implicits of local variables is a map in theGravatar pboutill2011-02-10
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Do not throw an error for anonymous generalized binders as they will beGravatar msozeau2010-11-18
* Minor fixes from Gregory Malecha. A typo fixed and a better (located) Gravatar msozeau2010-11-15
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
* Fix bug #2321, allowing "_" named projections in classes. Not realizingGravatar msozeau2010-09-28
* Remove some occurrences of "open Termops"Gravatar glondu2010-09-28
* Fix function applications without labels (OCaml warning 6)Gravatar glondu2010-09-28
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* * removed declare_constant and declare_internal_constant Gravatar vsiles2010-09-02
* v13392 port from v8.3 to trunk : correct message when defining inductive schemesGravatar vsiles2010-09-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Simplified the way internalization_data (i.e. bindings of bound varsGravatar herbelin2010-07-22
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
* change the flag "internal" in declare/ind_tables from bool toGravatar vsiles2010-06-29
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Fix treatment of remaining unification constraints: raise a moreGravatar msozeau2010-03-07