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-06-04
test suite: make target to regenerate failing output tests
Gaëtan Gilbert
2018-06-04
Merge PR #7199: Fixes #7195: missing freshness condition in Ltac pattern-matc...
Matthieu Sozeau
2018-06-04
Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.
Matthieu Sozeau
2018-06-04
Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly
Matthieu Sozeau
2018-06-04
Merge PR #7189: Fix #5539: algebraic universe produced by cases.
Matthieu Sozeau
2018-06-04
Merge PR #7349: Fix an anomaly when calling Obligation 0 or Obligation -1.
Matthieu Sozeau
2018-06-04
Documenting the API change.
Pierre-Marie Pédrot
2018-06-04
Adding an overlay for the Equations plugin.
Pierre-Marie Pédrot
2018-06-04
Stronger invariants in unification signature.
Pierre-Marie Pédrot
2018-06-04
Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ta...
Matthieu Sozeau
2018-06-04
Merge PR #7216: Replace uses of Termops.dependent by more specific functions.
Matthieu Sozeau
2018-06-04
Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...
Matthieu Sozeau
2018-06-04
Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".
Matthieu Sozeau
2018-06-04
Documenting the deprecation.
Pierre-Marie Pédrot
2018-06-04
Deprecate implicit tactic solving.
Pierre-Marie Pédrot
2018-06-04
Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension ...
Pierre-Marie Pédrot
2018-06-04
Merge PR #7619: Mention test-suite in PR template
Maxime Dénès
2018-06-04
Merge PR #7648: Indicate in the doc that clearbody can take several idents
Maxime Dénès
2018-06-04
Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.
Maxime Dénès
2018-06-04
Merge PR #7657: Fix a couple typos in deprecation messages
Pierre-Marie Pédrot
2018-06-04
Merge PR #7640: Small refactoring to clarify make_local_hint_db.
Pierre-Marie Pédrot
2018-06-04
Merge PR #7649: Remove some dead code in class_tactics.ml
Pierre-Marie Pédrot
2018-06-03
Statment -> Statement
Hugo Herbelin
2018-06-03
Fixing typos in file Berardi.v
Hugo Herbelin
2018-06-03
Merge PR #7682: Fixes #7641: more detailed message about disjunctive patterns...
Emilio Jesus Gallego Arias
2018-06-03
Merge PR #7689: configure: fix warning printing
Emilio Jesus Gallego Arias
2018-06-03
Merge PR #7637: Fix an outdated comment refering to lib/dnet.mli
Pierre-Marie Pédrot
2018-06-03
configure: fix warning printing
Gaëtan Gilbert
2018-06-03
Further sharing in CList.
Hugo Herbelin
2018-06-03
Cleaning, documentation, uniformisation of the Coq extension of List.
Hugo Herbelin
2018-06-03
Merge PR #7683: [lib] Fix wrong deprecation annotations.
Pierre-Marie Pédrot
2018-06-03
Fixes #7641: more detailed message for disjunctive patterns with different vars.
Hugo Herbelin
2018-06-03
Merge PR #7656: CI for QuickChick and ext-lib
Emilio Jesus Gallego Arias
2018-06-02
Update .gitlab to use newer ocaml
Leonidas Lampropoulos
2018-06-03
[lib] Fix wrong deprecation annotations.
Emilio Jesus Gallego Arias
2018-06-03
Merge PR #7681: Fixes #7636: location missing on deprecated compatibility not...
Emilio Jesus Gallego Arias
2018-06-02
QuickChick CI
Leonidas Lampropoulos
2018-06-02
Merge PR #7680: [ci] Expose updated `OCAMLPATH` for CI users.
Gaëtan Gilbert
2018-06-02
Fixes #7636: location missing on deprecated compatibility notations.
Hugo Herbelin
2018-06-02
Refuse to parse empty [Context] command.
Gaëtan Gilbert
2018-06-02
[ci] Expose updated `OCAMLPATH` for CI users.
Emilio Jesus Gallego Arias
2018-06-02
[appveyor] Use OCaml version 4.06.1 in the Windows build.
Emilio Jesus Gallego Arias
2018-06-01
Merge PR #7234: Reduce circular dependency constants <-> projections
Maxime Dénès
2018-06-01
Merge PR #7570: [api] Move `Constrexpr` to the `interp` module.
Maxime Dénès
2018-06-01
Merge PR #7537: Improve the Gallina chapter of the reference manual.
Maxime Dénès
2018-06-01
Merge PR #7606: Allow more than one signature and name per Sphinx object
Maxime Dénès
2018-06-01
Merge PR #7660: Add codeowner for timing python scripts
Maxime Dénès
2018-06-01
Merge two clearbody docs
Théo Winterhalter
2018-05-31
Merge PR #7652: Explicitly require python2 in python scripts in tools/
Jason Gross
2018-05-31
Add codeowner for timing python scripts
Jason Gross
[prev]
[next]