aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/recordops.ml
Commit message (Expand)AuthorAge
* Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
* Moving Option.smart_map to Option.Smart.map.Gravatar Hugo Herbelin2018-05-23
* Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* More detailed error messages for Canonical Structure, #6398Gravatar Paul Steckler2018-02-06
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* unification: fix BZ#5692, recognize prim projs as CS projectionsGravatar Matthieu Sozeau2017-10-17
* Properly handling projection parameters in canonical structures.Gravatar Pierre-Marie Pédrot2017-10-17
* Handling primitive projections in canonical structures.Gravatar Pierre-Marie Pédrot2017-10-17
* Getting rid of AUContext abstraction breakers in Recordops.Gravatar Pierre-Marie Pédrot2017-07-13
* Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: KernelGravatar Maxime Dénès2017-07-13
|\
| * Safe API for accessing universe constraints of global references.Gravatar Pierre-Marie Pédrot2017-07-11
* | Merge PR #863: Fixing environment in warning "Projection value has no head co...Gravatar Maxime Dénès2017-07-07
|\ \ | |/ |/|
| * Fixing environment in warning "Projection value has no head constant".Gravatar Hugo Herbelin2017-07-07
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|/
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Inv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Recordops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 17:05:31 +0000