aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
Commit message (Expand)AuthorAge
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* An old typo which was preventing example #3537 to work the same as itGravatar Hugo Herbelin2014-09-12
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Fix bug #3584, elaborating pattern-matching on primitive records to theGravatar Matthieu Sozeau2014-09-06
* Typing.sort_of does not leak evarmaps anymore.Gravatar Pierre-Marie Pédrot2014-09-04
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Change interface of refresh universes to get a pbty argument instead ofGravatar Matthieu Sozeau2014-06-26
* Fix program cases and inversion tactic to correctly record universe constraints.Gravatar Matthieu Sozeau2014-06-24
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* Refresh some universes in cases.ml as they might appear in the term.Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* TC: honor the use_typeclasses flag in pretypingGravatar Enrico Tassi2014-02-12
* Fix test-suite/success/evars.v.Gravatar Arnaud Spiwack2013-12-06
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Fix compilation of pattern matching wrt variables: alias.Gravatar aspiwack2013-11-02
* Fix the compilation of pattern matching wrt to variables.Gravatar aspiwack2013-11-02
* Abstracting evar filter away. The API is not perfect, but better than nothing.Gravatar ppedrot2013-10-27
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Fixing a source of evars leak, revealed by contrib QuicksortComplexityGravatar herbelin2013-05-11
* Uniformization: isevars -> evdref/sigma/evdGravatar herbelin2013-05-09
* Fix wrong computation of dependency signature in cases raising an uncaught ex...Gravatar msozeau2013-04-30
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
* invalid_arg instead of raise (Invalid_argement ...)Gravatar letouzey2013-03-12
* Removing Exc_located and using the new exception enrichementGravatar ppedrot2013-02-18
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
* Splitted Evarutil in two filesGravatar ppedrot2013-02-10
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Array.create is deprecatedGravatar pboutill2012-12-19
* Modulification of nameGravatar ppedrot2012-12-18
* Fixed a bug in the algorithm trying to elaborate a "match" return predicate.Gravatar herbelin2012-12-17
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 01:44:15 +0000