aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-09
|\
| * Fix strategy of Keyed UnificationGravatar Matthieu Sozeau2016-03-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\|
* | Slightly contracting code of evarconv.ml.Gravatar Hugo Herbelin2016-02-28
| * Fix part of bug #4533: respect declared global transparency ofGravatar Matthieu Sozeau2016-02-23
* | Adding location to universes generated by the pretyper.Gravatar Pierre-Marie Pédrot2016-02-19
* | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \
* | | Using monotonic types for conversion functions.Gravatar Pierre-Marie Pédrot2016-02-15
* | | 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
| | * CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ |/|
| * 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 02:05:47 +0000