aboutsummaryrefslogtreecommitdiff
path: root/engine
AgeCommit message (Expand)Author
2016-08-26CLEANUP: minor readability improvementsMatej Kosik
2016-08-26CLEANUP: removing "Termops.compact_named_context_reverse" functionMatej Kosik
2016-08-26CLEANUP: rename "Context.Named.{to,of}_rel" functions to "Context.Named.{to,o...Matej Kosik
2016-08-26CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Matej Kosik
2016-08-25Merge remote-tracking branch 'v8.6' into trunkMatej Kosik
2016-08-25CLEANUP: changing the definition of the "Context.NamedList.Declaration" typeMatej Kosik
2016-08-25CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Matej Kosik
2016-08-25Do not export an internal function in Namegen.Pierre-Marie Pédrot
2016-08-25CLEANUP: removing calls of the "Context.Named.Declaration.get_value" functionMatej Kosik
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-08-24CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionMatej Kosik
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-08-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-08-17Two protections against failures when printing evar_map.Hugo Herbelin
2016-08-17Fixing printing in debugger (no global env in debugger).Hugo Herbelin
2016-08-16Efficiently generate the pretyping contexts.Pierre-Marie Pédrot
2016-08-11CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" functionMatej Kosik
2016-08-11CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" functionMatej Kosik
2016-08-10Remove unused optional "predicative" argument.Guillaume Melquiond
2016-08-06Using a dedicated kind of substitutions in evar name generation.Pierre-Marie Pédrot
2016-08-05Using the extended contexts in pretyping.Pierre-Marie Pédrot
2016-08-04Use sets instead of lists for names to avoid in evar generation.Pierre-Marie Pédrot
2016-08-04Simplifying code in evar generation.Pierre-Marie Pédrot
2016-08-04Exporting the renaming API for evar declaration.Pierre-Marie Pédrot
2016-07-08Fixing #4906 (regression in printing an error message).Hugo Herbelin
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29Univ: Use loc even if there are more unbound levelsMatthieu Sozeau
2016-06-29Univs: add source locations of levelsMatthieu Sozeau
2016-06-24Optmimize the subst tactic.Pierre-Marie Pédrot
2016-06-24Optimize the clear tactic.Pierre-Marie Pédrot
2016-06-24Optimize the clear tactic.Pierre-Marie Pédrot
2016-06-23Better algorithm for variable deambiguation in term printing.Pierre-Marie Pédrot
2016-06-16Document new Hint Mode option.Matthieu Sozeau
2016-06-16Proofview: extensions for backtracking eautoMatthieu Sozeau
2016-06-16Implement limited proof search and iterative deepening.Matthieu Sozeau
2016-06-16Merge 'pr/191' into trunkEnrico Tassi
2016-06-14Merge remote-tracking branch 'origin/pr/173' into trunkEnrico Tassi
2016-06-14Fix a typo in proofs/proofview.mli.Cyprien Mangin
2016-06-14Fix usage of Pervasives in goal selectors.Cyprien Mangin
2016-06-14Add a comment about the use of a zipper, for clarity.Cyprien Mangin
2016-06-14Add a [CList.partitioni] function.Cyprien Mangin
2016-06-14Add goal range selectors.Cyprien Mangin
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-06-06STM: proof block detection for bullets and { block }Enrico Tassi
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-20Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Normalizing the names of dynamic types to follow a typ_* scheme.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 07:29:17 +0000