aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.ml
Commit message (Expand)AuthorAge
* merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\
* \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \
| * | Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
| | * CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ |/|
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\|
| * Add an option to deactivate compatibility printing of primitiveGravatar Matthieu Sozeau2015-12-02
* | Experimenting printing the type of the defined term of a LetIn whenGravatar Hugo Herbelin2015-11-07
|/
* Using "__" rather than this unelegant arbitrary "A" for the name of variables...Gravatar Hugo Herbelin2015-10-18
* Using appropriate lambda decomposition function counting let-ins whenGravatar Hugo Herbelin2015-10-18
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Do not compress match constructs when the inner match contains no branch. (Fi...Gravatar Guillaume Melquiond2015-09-18
* Continuing experimentation on what part of the instance of an evarGravatar Hugo Herbelin2015-02-21
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Fix issue in printing due to de Bruijn bug when constructing compatibilityGravatar Matthieu Sozeau2015-01-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Reactivating option "Set Printing Existential Instances" for asking printing ...Gravatar Hugo Herbelin2014-12-04
* Printing function for [uconstr].Gravatar Arnaud Spiwack2014-11-19
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* New experimental heuristic printing strategy for evar instances: WeGravatar Hugo Herbelin2014-10-17
* Re-displaying evar instances in debugger.Gravatar Hugo Herbelin2014-10-17
* Add an option to not print primitive projection parameters, which canGravatar Matthieu Sozeau2014-10-15
* Make constrMatching and detyping more robust with respect toGravatar Matthieu Sozeau2014-10-10
* Avoid a warning with Meta's names in debugger.Gravatar Hugo Herbelin2014-10-07
* 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
* Fix incorrect assert false in detyping.Gravatar Matthieu Sozeau2014-09-25
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Checking typability of evar instances. Using ";" to separate bindingsGravatar Hugo Herbelin2014-09-13
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Fixing the essence of naming bug #3204: use same strategy for namingGravatar Hugo Herbelin2014-08-25
* 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
* Compute the trace of a universe inconsistency only when explicitly requiredGravatar Pierre-Marie Pédrot2014-06-10
* 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
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing #3293 (eta-expansion at "match" printing time was failingGravatar Hugo Herbelin2014-04-28
* Goptions do not rely anymore on generic equality.Gravatar Pierre-Marie Pédrot2014-03-03
* Fixing bad comparison in Detyping.Gravatar Pierre-Marie Pédrot2014-03-01
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Typo resulting in bad eta-expansion of destructing let's body.Gravatar Hugo Herbelin2013-11-25
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 18:32:17 +0000