aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
Commit message (Expand)AuthorAge
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Better structure for Ltac pretyping environments.Gravatar Pierre-Marie Pédrot2014-08-07
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Quickly fixing bug #2996: typing functions now check when referring toGravatar Hugo Herbelin2014-06-28
* Change interface of refresh universes to get a pbty argument instead ofGravatar Matthieu Sozeau2014-06-26
* Fix for bug 1951, allowing at least fully-applied inductives types to be usedGravatar Matthieu Sozeau2014-06-23
* Fixed some HoTT bugs, provide a proper error message when giving an ill-formedGravatar Matthieu Sozeau2014-06-20
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Fixing #3282 (two bugs in the presence of let-in's in "fix").Gravatar Hugo Herbelin2014-06-17
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Fix type inference of the record argument of a projection to catch ill-typedGravatar Matthieu Sozeau2014-06-17
* In generalized rewrite, avoid retyping completely and constantly the conclusi...Gravatar Matthieu Sozeau2014-06-11
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* Find a more efficient fix for dealing with template universes:Gravatar Matthieu Sozeau2014-05-06
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
* - Add back some compatibility functions to avoid rewriting plugins.Gravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Fix interface for template polymorphism, cleaning up code in all typing algor...Gravatar Matthieu Sozeau2014-05-06
* Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing bug #3228 (fixing precedence of ltac variables over variables in env).Gravatar Hugo Herbelin2014-04-05
* TC: honor the use_typeclasses flag in pretypingGravatar Enrico Tassi2014-02-12
* Support for evars and metas in native compiler.Gravatar Maxime Dénès2013-12-30
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Removing useless casts between arrays and lists.Gravatar ppedrot2013-08-04
* Using the whole tactic environment while Pretyping.Gravatar ppedrot2013-06-24
* Generalizing the use of maps instead of lists in the interpretationGravatar ppedrot2013-06-22
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Avoid a few overzealous "when Errors.noncritical"Gravatar letouzey2013-03-17
* Retyping.get_type_of: a lax version raising no anomaliesGravatar letouzey2013-03-17
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
* Actually adding backtrace handling.Gravatar ppedrot2013-01-28
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Added backtrace information to anomaliesGravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 02:55:58 +0000