index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2019-11-19
G_constr: Renaming instance -> univ_instance (more specific name).
Hugo Herbelin
2019-11-19
G_constr: Uniformization of indentation.
Hugo Herbelin
2019-11-19
Separating constr grammar for fix and cofix, for the purpose of documentation.
Hugo Herbelin
2019-11-19
Grammar: slight simplification of treatment of annot/binder overlapping.
Hugo Herbelin
2019-11-19
Grammar: mini-factorization between fix/cofix and Fixpoint/CoFixpoint.
Hugo Herbelin
2019-11-19
Grammar of terms: mini-shortcut in the rules for fix and cofix.
Hugo Herbelin
2019-11-19
Fixing bugs in the computation of implicit arguments for fix with a let binder.
Hugo Herbelin
2019-11-19
coq_makefile: support COQBIN with no ending /
Gaëtan Gilbert
2019-11-19
Merge PR #11106: Printing name of change log file in changelog script
Gaëtan Gilbert
2019-11-19
added changelog entry
Cyril Cohen
2019-11-18
Adding `inj_compr` lemma in ssrfun.
Cyril Cohen
2019-11-18
Merge PR #11115: [dune] Update .gitignore after #11092
Emilio Jesus Gallego Arias
2019-11-16
Merge PR #10996: Refine Instance returns
Pierre-Marie Pédrot
2019-11-16
Merge PR #10998: Add missing zify class instances
Frédéric Besson
2019-11-16
Merge PR #11095: Do not export the internals of the prepare_hint function.
Gaëtan Gilbert
2019-11-15
Merge PR #11079: Rename non-unique local nonterminals
Hugo Herbelin
2019-11-15
Update doc/changelog/04-tactics/10998-zify-complements.rst
Kazuhiko Sakaguchi
2019-11-15
Add missing zify class instances
Kazuhiko Sakaguchi
2019-11-14
Rename non-unique local nonterminals
Jim Fehrle
2019-11-14
Merge PR #10979: Fix doc for universes(foo) attributes
Théo Zimmermann
2019-11-14
Fix doc for universes(foo) attributes
Gaëtan Gilbert
2019-11-14
Merge PR #11100: small documentation fixes
Théo Zimmermann
2019-11-14
doc fixes
Antonio Nikishaev
2019-11-14
Restore documentation of `Typeclasses Axioms Are Instances`
Maxime Dénès
2019-11-14
Document recommended syntax for `firstorder`
Maxime Dénès
2019-11-13
cleanup unused argument for Classes.do_instance_resolve_TC
Gaëtan Gilbert
2019-11-13
Return of Refine Instance as an attribute.
Gaëtan Gilbert
2019-11-13
don't double parse program attribute for vernacinstance
Gaëtan Gilbert
2019-11-13
Update .gitignore after #11092
Pierre Roux
2019-11-13
Merge PR #11094: Miscellaneous micro-improvements of the syntax of records
Pierre-Marie Pédrot
2019-11-13
Merge PR #11070: Do not rely on the user settings but on the actual window si...
Pierre-Marie Pédrot
2019-11-13
Register proof_irrelevance
Pierre Roux
2019-11-12
Printing name of change log file in changelog script.
Hugo Herbelin
2019-11-12
Merge PR #11067: Expand documentation about generating a Docker image.
Emilio Jesus Gallego Arias
2019-11-12
Expand documentation about generating a Docker image.
Pierre-Marie Pédrot
2019-11-12
Merge PR #11092: [dune] Have only one rule calling configure
Emilio Jesus Gallego Arias
2019-11-12
Merge PR #11045: Forbid Include inside sections
Pierre-Marie Pédrot
2019-11-11
Have only one dune rule calling configure
Pierre Roux
2019-11-11
Do not export the internals of the prepare_hint function.
Pierre-Marie Pédrot
2019-11-11
Merge PR #11032: Run update-compat script with --release option.
Pierre-Marie Pédrot
2019-11-11
Run update-compat script with --release option.
Théo Zimmermann
2019-11-11
Merge PR #11052: Fix #11048: uncaught destKO in inductive type
Pierre-Marie Pédrot
2019-11-11
Miscellaneous improvements of the syntax of records.
Hugo Herbelin
2019-11-10
Merge PR #10980: Fix #10903: type-in-type allows fixpoints on sprop inductives
Pierre-Marie Pédrot
2019-11-09
Merge PR #11017: Make [Proof_global.closed_proof_output] opaque
Pierre-Marie Pédrot
2019-11-08
Make [Proof_global.closed_proof_output] opaque
Gaëtan Gilbert
2019-11-08
Merge PR #11014: Fix #8459: anomaly not enough abstractions in fix body
Pierre-Marie Pédrot
2019-11-08
Merge PR #11069: Do not include final stops in queries. (Fixes #11058)
Pierre-Marie Pédrot
2019-11-08
coqdep: only output vos when passed -vos
Gaëtan Gilbert
2019-11-08
Merge PR #11050: Replace "option" in doc when it refers to a flag
Théo Zimmermann
[prev]
[next]