aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/recordops.ml
Commit message (Expand)AuthorAge
* Remove spurious warnings about projections when requiring modules.Gravatar Pierre-Marie Pédrot2016-07-08
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Do not compose List.length with List.filter.Gravatar Guillaume Melquiond2015-12-31
|/
* Fix universe instantiation with canonical structures.Gravatar Maxime Dénès2015-07-16
* Update headers.Gravatar Maxime Dénès2015-01-12
* Documenting check_record + changing a possibly undefined int into int option.Gravatar Hugo Herbelin2014-12-15
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Fix canonical structure resolution which was launched on the results ofGravatar Matthieu Sozeau2014-09-26
* Fast path in Canonical structure detection. We do not always compute the normalGravatar Pierre-Marie Pédrot2014-06-27
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* - Fixes for canonical structure resolution (check that the initial term indee...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* Stack operations of Reductionops in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Unplugging Autoinstance. The code is still here if someone wishesGravatar ppedrot2013-09-12
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
* Removed many calls to OCaml generic equality. This was done byGravatar ppedrot2012-10-29
* 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
* Unification in Evar_conv uses an abstract machine stateGravatar pboutill2012-08-09
* Updating headers.Gravatar herbelin2012-08-08
* Replacing some str with strbrkGravatar ppedrot2012-06-04
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Improved check is_open_canonical_projectionGravatar gareuselesinge2011-11-08
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* Patch to simplify is_open_canonical_projectionGravatar herbelin2011-08-02
* Remove some occurrences of "open Termops"Gravatar glondu2010-09-28
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Applying François' patches about Canonical Projections (see #2302 and #2334).Gravatar herbelin2010-06-26
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Added a function in typing.ml to solve evars of a constr w/o going back down ...Gravatar herbelin2010-04-05
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17