index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2020-03-04
Merge PR #11715: Be robust in calculating visible ids for non-registered cons...
Hugo Herbelin
2020-03-04
[boot] Don't initialize coqlib when `-boot` is passed.
Emilio Jesus Gallego Arias
2020-03-04
Fix #11749: don't warn for hidden files.
Théo Zimmermann
2020-03-04
Merge PR #11429: [zify] several efficiency enhancements
Vincent Laporte
2020-03-04
Add overlay for equations.
Hugo Herbelin
2020-03-04
Experimenting using a record for decl_notation.
Hugo Herbelin
2020-03-04
Adding support for an "only parsing" modifier in "where"-based notations.
Hugo Herbelin
2020-03-04
Merge PR #11380: [exninfo] Deprecate aliases for exception re-raising.
Pierre-Marie Pédrot
2020-03-04
Merge PR #11618: [loadpath] Rework and simplify ML loadpath handling
Théo Zimmermann
2020-03-04
Merge PR #11709: Deprecate the "prolog" tactic.
Théo Zimmermann
2020-03-04
Add file to register names of reals library used by gappa
Michael Soegtrop
2020-03-03
[exn] Keep information from multiple extra exn handlers
Emilio Jesus Gallego Arias
2020-03-03
[vernac] Use a record for VernacAddLoadPath
Emilio Jesus Gallego Arias
2020-03-03
[stm] Port documentation of init options to ocamldoc
Emilio Jesus Gallego Arias
2020-03-03
[loadpath] Rework and simplify ML loadpath handling
Emilio Jesus Gallego Arias
2020-03-03
Remove invisible U+FE00 variation selector from CoqIDE bindings
Nickolai Zeldovich
2020-03-03
[dune] Fix bug in auto-configure deps.
Emilio Jesus Gallego Arias
2020-03-03
[exninfo] Deprecate aliases for exception re-raising.
Emilio Jesus Gallego Arias
2020-03-03
[zify] efficiency improvements
Frédéric Besson
2020-03-03
When parsing negative integer, ensure minus sign is contiguous to the number.
Hugo Herbelin
2020-03-03
Ltac2: Add notation for enough and eenough
Michael Soegtrop
2020-03-03
Update doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst
Hugo Herbelin
2020-03-03
Adding an alias "pose proof (x:=a)" for "pose proof a as x".
Hugo Herbelin
2020-03-03
Merge PR #11695: Refactor lookaheads
Pierre-Marie Pédrot
2020-03-03
Update the OCaml version in `default.nix` to 4.09.0
Maxime Dénès
2020-03-02
Merge PR #11634: Remove the dependency in float.cmo and uint63.cmo for buildi...
Pierre-Marie Pédrot
2020-03-02
Merge PR #11681: Fix backtraces in conversion anomalies caught by Reductionops.
Maxime Dénès
2020-03-02
Refine patch for clearer scoping of evar_map
Matthieu Sozeau
2020-03-02
Merge PR #11728: [dune] [doc] Be more explicit about coqtop dependencies
Théo Zimmermann
2020-03-01
Merge PR #11708: [ci] elpi 1.10.2
Emilio Jesus Gallego Arias
2020-03-01
[parser] lk_int -> lk_nat
Maxime Dénès
2020-03-01
Refactor lookaheads using DSL
Maxime Dénès
2020-03-01
Move lookahead combinators to Pcoq
Maxime Dénès
2020-03-01
[ci] [docker] overlay for elpi 1.10
Enrico Tassi
2020-03-01
[ci] [docker] bump elpi to 1.10.2
Enrico Tassi
2020-03-01
[ci] bump dune to 2.0.1 due to upstream problems
Enrico Tassi
2020-03-01
[dune] [doc] Be more explicit coqtop dependencies
Emilio Jesus Gallego Arias
2020-03-01
test-suite file for spurious universe generation
Matthieu Sozeau
2020-03-01
Fix mishandling of sigma in guess_elim (regression from 8.11)
Matthieu Sozeau
2020-02-29
[dune] [ocamldebug] Improve ocamldebug rules
Emilio Jesus Gallego Arias
2020-02-29
Merge PR #11701: Fix #11696: link from refman to stdlib doc is dead.
Clément Pit-Claudel
2020-02-29
Be robust in calculating visible ids for non-registered constants.
Pierre-Marie Pédrot
2020-02-28
Merge PR #10008: CoqIDE: Fix not escaping coqtop arguments when compiling
Hugo Herbelin
2020-02-28
[gramlib] Refactor gramlib interface.
Emilio Jesus Gallego Arias
2020-02-28
Merge PR #11423: Convert Vernacular section of gallina chapter to use prodn
Théo Zimmermann
2020-02-28
Convert Gallina Vernac to use prodn
Jim Fehrle
2020-02-28
Deprecate the "prolog" tactic.
Pierre-Marie Pédrot
2020-02-28
Merge PR #11609: [stm] Use Default Proof Using only with Proof
Enrico Tassi
2020-02-28
[stm] Use Default Proof Using only with Proof
Tej Chajed
2020-02-28
Deprecate the OCaml API to declare term Hints.
Pierre-Marie Pédrot
[prev]
[next]