index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2018-10-23
Merge PR #8799: Fix formatting. Use standard if..then grammar.
Théo Zimmermann
2018-10-23
Fixing #8794 (anomaly with abbreviation involving both term and binders).
Hugo Herbelin
2018-10-23
Merge PR #8802: [dune] Install man pages + remove two obsolete ones.
Théo Zimmermann
2018-10-23
Fix issue #8801.
Guillaume Melquiond
2018-10-23
Fix issue #8800.
Guillaume Melquiond
2018-10-23
Merge PR #8786: Adding a regression test for bug #8785: universe constraints ...
Pierre-Marie Pédrot
2018-10-23
Compat 8.8: For String/Ascii, hides "Declare ML Module" behind an "Export".
Hugo Herbelin
2018-10-23
Encapsulating declarations of primitive string syntax in a module.
Hugo Herbelin
2018-10-23
Merge PR #8797: [doc] [api] Update `odoc` to new release 1.3.0
Gaëtan Gilbert
2018-10-23
Merge remote-tracking branch 'origin/pr/70'
Pierre-Marie Pédrot
2018-10-23
Merge remote-tracking branch 'origin/pr/71'
Pierre-Marie Pédrot
2018-10-23
[dune] Install man pages + remove two obsolete ones.
Emilio Jesus Gallego Arias
2018-10-23
Fix formatting. Use standard if..then grammar.
Sam Pablo Kuper
2018-10-23
Order Greek letters consistently w/rest of document
Sam Pablo Kuper
2018-10-23
[dune] Compile debug and checker printers.
Emilio Jesus Gallego Arias
2018-10-23
[build] Refactoring to config lib and ocamldebug tweaks.
Emilio Jesus Gallego Arias
2018-10-22
[doc] [api] Update `odoc` to new release 1.3.0
Emilio Jesus Gallego Arias
2018-10-22
Merge PR #8708: Stupid but critical unfolding heuristic.
Maxime Dénès
2018-10-22
Merge PR #8784: [dune] Remove rule for cLexer.ml4 -> cLexer.ml
Théo Zimmermann
2018-10-22
Merge pull request #11 from ejgallego/vernac+monify_hook
Yves Bertot
2018-10-21
Adding a regression test for bug #8785 (missing univ constraints registration).
Hugo Herbelin
2018-10-20
Cleanup comparing projections through their constants.
Gaëtan Gilbert
2018-10-20
Merge PR #8769: [library] Remove redundant re-addition of universe constraints.
Gaëtan Gilbert
2018-10-20
[dune] Remove rule for cLexer.ml4 -> cLexer.ml
Emilio Jesus Gallego Arias
2018-10-20
Merge PR #8782: gitignore test-suite/.nia.cache
Théo Zimmermann
2018-10-19
Merge PR #8758: [api] Qualify access to `Nametab`
Hugo Herbelin
2018-10-19
gitignore test-suite/.nia.cache
Gaëtan Gilbert
2018-10-19
Deprecating unused Engine.type_of_global.
Hugo Herbelin
2018-10-19
Deprecating Global.type_of_global_in_context.
Hugo Herbelin
2018-10-19
Deprecating Global.constr_of_global_in_context.
Hugo Herbelin
2018-10-19
Moving Global.constr_of_global_in_context to Typeops.
Hugo Herbelin
2018-10-19
Moving Global.type_of_global_in_context to Typeops.
Hugo Herbelin
2018-10-19
Cleaning layout typeops.mli.
Hugo Herbelin
2018-10-19
Porting the test-suite to coqpp.
Pierre-Marie Pédrot
2018-10-19
Adapt coq_makefile to handle coqpp-based macro files.
Pierre-Marie Pédrot
2018-10-19
Merge PR #8724: [universes] deprecate constr_of_global
Pierre-Marie Pédrot
2018-10-19
Explicitly merge contexts in side-effect universe handling.
Pierre-Marie Pédrot
2018-10-19
Move side-effect typing into Safe_env.
Pierre-Marie Pédrot
2018-10-19
Merge PR #8740: Removing the Camlp5 macros from CLexer.
Emilio Jesus Gallego Arias
2018-10-19
Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoerceTo.
Pierre-Marie Pédrot
2018-10-19
Replace non-idiomatic "dead-alleys" with idiomatic "dead-ends"
Sam Pablo Kuper
2018-10-18
[library] Remove redundant re-addition of universe constraints.
Emilio Jesus Gallego Arias
2018-10-18
[nametab] [api] Provide basic support for efficient completion.
Emilio Jesus Gallego Arias
2018-10-18
[clib] Provide `filter_range` function.
Emilio Jesus Gallego Arias
2018-10-18
Merge PR #8719: [ci] [appveyor] Disable validate target.
Maxime Dénès
2018-10-18
Give code ownership of merging doc to pushers team to notify members when it ...
Théo Zimmermann
2018-10-18
Merge PR #8670: Document the issue with positive coinductive types.
Théo Zimmermann
2018-10-18
Adding a rule to generate grammar.cma.
Pierre-Marie Pédrot
2018-10-18
Removing the Camlp5 macros from CLexer.
Pierre-Marie Pédrot
2018-10-18
[universes] deprecate constr_of_global
Matthieu Sozeau
[prev]
[next]