index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2017-04-12
Merge PR#441: Port Toplevel to the Stm API
Maxime Dénès
2017-04-12
[toplevel] [stm] cleanup in module open
Emilio Jesus Gallego Arias
2017-04-12
[stm] [nit] Centralize compile-time debug flag.
Emilio Jesus Gallego Arias
2017-04-12
[stm] Improve error messages on add/parse.
Emilio Jesus Gallego Arias
2017-04-12
[flags] Documentation and a minor tweak.
Emilio Jesus Gallego Arias
2017-04-12
[vernac] vernacentries.mli cleanup
Emilio Jesus Gallego Arias
2017-04-12
[stm] Port the toplevel to the STM.
Emilio Jesus Gallego Arias
2017-04-12
[stm] Move main parsing entry point to the STM.
Emilio Jesus Gallego Arias
2017-04-12
[stm] Remove edit_id.
Emilio Jesus Gallego Arias
2017-04-12
Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...
Maxime Dénès
2017-04-11
Merge PR#549: Fast path in weak head reduction of applied atoms.
Maxime Dénès
2017-04-11
Merge PR#543: Sanitize instance interpretation
Maxime Dénès
2017-04-11
Merge PR#532: Clean Nsatz implementation.
Maxime Dénès
2017-04-11
Merge PR#537: Efficient side-effect abstraction
Maxime Dénès
2017-04-11
Merge PR#379: Introducing evar-insensitive constrs
Maxime Dénès
2017-04-10
Adding a test for 'rewrite in *' when an evar is solved by side-effect.
Pierre-Marie Pédrot
2017-04-10
Adding a test for the correctness of normalization in legacy typeclasses.
Pierre-Marie Pédrot
2017-04-10
Documenting the changes introduced by the EConstr branch.
Pierre-Marie Pédrot
2017-04-10
Revert "refactoring: Reductionops.contextual_reduction_function type"
Matej Košík
2017-04-10
Revert "comment: typo"
Matej Košík
2017-04-10
Revert "refactoring: Names.DirPath.equal"
Matej Košík
2017-04-10
Revert "refactoring: Names.DirPath.compare"
Matej Košík
2017-04-10
Revert "refactoring: Names.DirPath.is_empty"
Matej Košík
2017-04-10
Revert "simplify: Environ.push_named"
Matej Košík
2017-04-10
Revert "trivial"
Matej Košík
2017-04-10
Revert "trivial"
Matej Košík
2017-04-10
Revert "comments: corrected in the Context module"
Matej Košík
2017-04-10
comments: corrected in the Context module
Matej Kosik
2017-04-10
trivial
Matej Kosik
2017-04-10
trivial
Matej Kosik
2017-04-10
simplify: Environ.push_named
Matej Kosik
2017-04-10
refactoring: Names.DirPath.is_empty
Matej Kosik
2017-04-10
refactoring: Names.DirPath.compare
Matej Kosik
2017-04-10
refactoring: Names.DirPath.equal
Matej Kosik
2017-04-10
comment: typo
Matej Kosik
2017-04-10
refactoring: Reductionops.contextual_reduction_function type
Matej Kosik
2017-04-10
Merge PR#547: [toplevel] Remove the feedback printer only on exit.
Maxime Dénès
2017-04-10
Merge PR#548: [ide] Correctly place warning tags.
Maxime Dénès
2017-04-09
Merge PR#460: Turning the printing primitive projection compatibility flag of...
Maxime Dénès
2017-04-09
Fix an algorithmic issue in Nsatz.
Pierre-Marie Pédrot
2017-04-09
Academic prescriptivism strikes back: down with baroque programming in Nsatz.
Pierre-Marie Pédrot
2017-04-08
Fast path in weak head reduction of applied atoms.
Pierre-Marie Pédrot
2017-04-08
[ide] Correctly place warning tags.
Emilio Jesus Gallego Arias
2017-04-08
Update the .mailmap file.
Guillaume Melquiond
2017-04-08
Fix a heuristic used by legacy typeclass resolution.
Pierre-Marie Pédrot
2017-04-07
[stm] remove process_error_hook
Emilio Jesus Gallego Arias
2017-04-07
[stm] remove tactic_being_run hook
Emilio Jesus Gallego Arias
2017-04-07
Merge PR#461: [camlpX] Remove camlp4 compat layer.
Maxime Dénès
2017-04-07
[toplevel] Remove the feedback feeder printing only on exit.
Emilio Jesus Gallego Arias
2017-04-07
Fix an unhandled exception in Omega.
Pierre-Marie Pédrot
[next]