aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/record.ml
Commit message (Expand)AuthorAge
* Fixing bug #2951.Gravatar Pierre-Marie Pédrot2015-03-08
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Give the same argument name for the record binder of type classGravatar Matthieu Sozeau2014-10-10
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Rework typeclass resolution and control of backtracking.Gravatar Matthieu Sozeau2014-09-15
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Add a flag for restricting resolution of typeclasses toGravatar Matthieu Sozeau2014-09-11
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* Types declared as Variants really do not accept recursive definitions.Gravatar Arnaud Spiwack2014-09-04
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Fix bug when defining primitive projections mixing defined and abstracts fields.Gravatar Matthieu Sozeau2014-08-29
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* - Do module substitution inside mind_record.Gravatar Matthieu Sozeau2014-07-25
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Complying an ocaml warning.Gravatar Hugo Herbelin2014-06-17
* Safer entry point of primitive projections in the kernel, now it does recognizeGravatar Matthieu Sozeau2014-06-17
* Allow records whose sort is defined by a constant.Gravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* cList: a few alternative to hashtbl-based uniquize, distinct, subsetGravatar letouzey2013-10-23
* Removing almost all new_untyped_evar, and a bunch of Evd.add.Gravatar ppedrot2013-09-18
* Unplugging Autoinstance. The code is still here if someone wishesGravatar ppedrot2013-09-12
* State Transaction MachineGravatar gareuselesinge2013-08-08
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* 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