aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Expand)AuthorAge
* CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\
| * Fix bug #5145: Anomaly: index to an anonymous variable.Gravatar Pierre-Marie Pédrot2016-10-15
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\|
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
| * Merge remote-tracking branch 'github/pr/263' into v8.6Gravatar Maxime Dénès2016-10-03
| |\
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\| |
| * | Adding variants enter_one and refine_one which assume that exactly oneGravatar Hugo Herbelin2016-09-16
| | * Tracking careless uses of slow name lookup.Gravatar Pierre-Marie Pédrot2016-09-09
| |/
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-07
|\ \ \ | | |/ | |/|
| * | Fast path in push_rel_context_to_named_context.Gravatar Pierre-Marie Pédrot2016-09-05
| * | Fast path in whd_evar.Gravatar Pierre-Marie Pédrot2016-09-02
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\| |
| * | Short documentation, filling TODO's in evd.mli.Gravatar Hugo Herbelin2016-09-01
* | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
* | | Removing calls of "Context.Rel.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-26
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-26
* | | CLEANUP: removing "Termops.compact_named_context_reverse" functionGravatar Matej Kosik2016-08-26
* | | CLEANUP: rename "Context.Named.{to,of}_rel" functions to "Context.Named.{to,o...Gravatar Matej Kosik2016-08-26
* | | CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Gravatar Matej Kosik2016-08-26
* | | Merge remote-tracking branch 'v8.6' into trunkGravatar Matej Kosik2016-08-25
|\| |
* | | CLEANUP: changing the definition of the "Context.NamedList.Declaration" typeGravatar Matej Kosik2016-08-25
* | | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Gravatar Matej Kosik2016-08-25
| * | Do not export an internal function in Namegen.Gravatar Pierre-Marie Pédrot2016-08-25
* | | CLEANUP: removing calls of the "Context.Named.Declaration.get_value" functionGravatar Matej Kosik2016-08-25
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* | | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
| | * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| | * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
| |/ |/|
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-08-17
|\|
| * Two protections against failures when printing evar_map.Gravatar Hugo Herbelin2016-08-17
| * Fixing printing in debugger (no global env in debugger).Gravatar Hugo Herbelin2016-08-17
| * Efficiently generate the pretyping contexts.Gravatar Pierre-Marie Pédrot2016-08-16
| |\
* | | CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-11
* | | CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-11
| * | Remove unused optional "predicative" argument.Gravatar Guillaume Melquiond2016-08-10
|/ /
| * Using a dedicated kind of substitutions in evar name generation.Gravatar Pierre-Marie Pédrot2016-08-06
| * Using the extended contexts in pretyping.Gravatar Pierre-Marie Pédrot2016-08-05
| * Use sets instead of lists for names to avoid in evar generation.Gravatar Pierre-Marie Pédrot2016-08-04
| * Simplifying code in evar generation.Gravatar Pierre-Marie Pédrot2016-08-04
| * Exporting the renaming API for evar declaration.Gravatar Pierre-Marie Pédrot2016-08-04
|/
* Fixing #4906 (regression in printing an error message).Gravatar Hugo Herbelin2016-07-08
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Univ: Use loc even if there are more unbound levelsGravatar Matthieu Sozeau2016-06-29
* Univs: add source locations of levelsGravatar Matthieu Sozeau2016-06-29