aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Expand)AuthorAge
* 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
* Optmimize the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* Optimize the clear tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* Optimize the clear tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* Better algorithm for variable deambiguation in term printing.Gravatar Pierre-Marie Pédrot2016-06-23
* Document new Hint Mode option.Gravatar Matthieu Sozeau2016-06-16
* Proofview: extensions for backtracking eautoGravatar Matthieu Sozeau2016-06-16
* Implement limited proof search and iterative deepening.Gravatar Matthieu Sozeau2016-06-16
* Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\
* \ Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \
| | * Fix a typo in proofs/proofview.mli.Gravatar Cyprien Mangin2016-06-14
| | * Fix usage of Pervasives in goal selectors.Gravatar Cyprien Mangin2016-06-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 16:19:04 +0000