aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Renaming functions in Typing to stick to the standard e_* scheme.Gravatar Pierre-Marie Pédrot2016-02-15
* Monotonizing the Evarutil module.Gravatar Pierre-Marie Pédrot2016-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
| * Optimizing the computation of frozen evars.Gravatar Pierre-Marie Pédrot2016-02-03
| * Opacifying the type of evar naming structure in Evd.Gravatar Pierre-Marie Pédrot2016-02-03
| * More compact representation for evar resolvability flag.Gravatar Pierre-Marie Pédrot2016-02-03
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\|
| * Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Gravatar Pierre-Marie Pédrot2016-01-27
| * Fix bug #4519: oops, global shadowed local universe level bindings.Gravatar Matthieu Sozeau2016-01-23
| * Fix bug #4506. Using betadeltaiota_nolet might produce terms of the formGravatar Matthieu Sozeau2016-01-23
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\|
| * Fixing #4256 and #4484 (changes in evar-evar resolution made that newGravatar Hugo Herbelin2016-01-12
| * Extend last commit: keyed unification uses full conversions on the applied co...Gravatar Matthieu Sozeau2016-01-12
| * Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | | Remove duplicate declarations.Gravatar Guillaume Melquiond2016-01-02
* | | Reduce dependencies of interface files.Gravatar Guillaume Melquiond2016-01-02
* | | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|\ \ \ | | |/ | |/|
* | | Do not compose List.length with List.filter.Gravatar Guillaume Melquiond2015-12-31
| * | Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.Gravatar Pierre-Marie Pédrot2015-12-29
* | | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
| |/ |/|
| * (Partial) fix for bug #4453: raise an error instead of an anomaly.Gravatar Matthieu Sozeau2015-12-17
* | CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
* | CLEANUP: in the Reductionops moduleGravatar Matej Kosik2015-12-17
* | CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
* | Fixing unexpected length of context in a typing function, detected byGravatar Hugo Herbelin2015-12-15
* | Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite.Gravatar Hugo Herbelin2015-12-15
* | API: documenting context_chop and removing a duplicate.Gravatar Hugo Herbelin2015-12-15
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-15
|\|
| * Optimize occur_evar_upto_types, avoiding repeateadly looking into theGravatar Matthieu Sozeau2015-12-11
* | Unifying betazeta_applist and prod_applist into a clearer interface.Gravatar Hugo Herbelin2015-12-05
* | Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
* | Simplifying an instantiation function using subst_of_rel_context_instance.Gravatar Hugo Herbelin2015-12-05
* | About building of substitutions from instances.Gravatar Hugo Herbelin2015-12-05
* | An example in centralizing similar functions to a common place so thatGravatar Hugo Herbelin2015-12-05
* | Removing dynamic inclusion of constrs in tactic AST.Gravatar Pierre-Marie Pédrot2015-12-04
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\|
| * Add an option to deactivate compatibility printing of primitiveGravatar Matthieu Sozeau2015-12-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\|
| * Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* | More efficient implementation of equality-up-to-universes in Universes.Gravatar Pierre-Marie Pédrot2015-11-26
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-26
|\|
| * Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej).Gravatar Hugo Herbelin2015-11-25
| * Fixing an old typo in Retyping, found by Matej.Gravatar Hugo Herbelin2015-11-24
| * Fixing a vm_compute bug in the presence of let-ins among theGravatar Hugo Herbelin2015-11-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 22:25:37 +0000