index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
romega: if it bugs again, at least do it with a short and quick error
Pierre Letouzey
2017-05-22
*
refl_omega: comment the lack of lifts when dealing with arrows
Pierre Letouzey
2017-05-22
*
romega: discard constructor D_mono (shorter trace + fix a bug)
Pierre Letouzey
2017-05-22
*
refl_omega: more refactoring (e.g. IntSets instead of sorted lists)
Pierre Letouzey
2017-05-22
*
refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp)
Pierre Letouzey
2017-05-22
*
ReflOmegaCore: discard useless cosntructor P_NOP
Pierre Letouzey
2017-05-22
*
ReflOmegaCore: revised proofs (mostly bullets instead of ;[|||])
Pierre Letouzey
2017-05-22
*
Merge PR#276: Stopping injection not to work on discriminable atoms (see #4890).
Maxime Dénès
2017-05-20
|
\
*
\
Merge PR#654: Travis: do not cache opam logs (+prettier spacing)
Maxime Dénès
2017-05-20
|
\
\
*
\
\
Merge PR#643: [ide] Disable `print_ast` call.
Maxime Dénès
2017-05-20
|
\
\
\
*
\
\
\
Merge PR#474: A fix for #5390 (a useful error on used introduction names was ...
Maxime Dénès
2017-05-20
|
\
\
\
\
*
\
\
\
\
Merge PR#627: Obligations shrinking: shrink abstraction too
Maxime Dénès
2017-05-20
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR#644: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)
Maxime Dénès
2017-05-20
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR#648: Allow interactive editing of `plugins/` by adding .dir-locals.el
Maxime Dénès
2017-05-20
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR#649: Fix a typo
Maxime Dénès
2017-05-20
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR#651: Re-adding explicit dependency of misc universe test into all_st...
Maxime Dénès
2017-05-20
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR#640: [toplevel] Restore 8.6 goal printing behavior.
Maxime Dénès
2017-05-20
|
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
|
|
*
|
Travis: do not cache opam logs (+prettier spacing)
Gaetan Gilbert
2017-05-19
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
Re-adding explicit dependency of misc universe test into all_stdlib.v.
Hugo Herbelin
2017-05-19
|
|
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
Fix a typo
Jason Gross
2017-05-18
|
|
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
Add .dir-locals.el to plugins
Jason Gross
2017-05-18
|
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
[toplevel] [stm] Avoid edit_at in batch mode (bug #5520)
Emilio Jesus Gallego Arias
2017-05-18
|
|
|
|
|
*
|
[ide] Disable `print_ast` call.
Emilio Jesus Gallego Arias
2017-05-18
|
|
|
|
_
|
/
/
|
|
|
/
|
|
|
|
|
|
|
*
|
A fix for #5390 (a useful error on used introduction names was masked).
Hugo Herbelin
2017-05-17
|
|
|
|
/
/
|
|
|
/
|
|
*
|
|
|
|
Merge PR#633: An extension of EXTEND and notations to make standard parsing t...
Maxime Dénès
2017-05-17
|
\
\
\
\
\
|
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
*
Documenting relaxing of constraints on injection.
Hugo Herbelin
2017-05-17
|
|
|
|
*
Stopping injection not to work on discriminable atoms (see #4890).
Hugo Herbelin
2017-05-17
|
|
_
|
_
|
/
|
/
|
|
|
*
|
|
|
Merge PR#457: Adding an even more compact goal hyps mode.
Maxime Dénès
2017-05-17
|
\
\
\
\
*
\
\
\
\
Merge PR#607: Make congruence reuse discriminate instead of rolling its own.
Maxime Dénès
2017-05-17
|
\
\
\
\
\
|
|
|
|
*
|
[toplevel] Restore 8.6 goal printing behavior.
Emilio Jesus Gallego Arias
2017-05-17
*
|
|
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-05-17
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR#620: Reorganization of the layout for miscellaneous tests
Maxime Dénès
2017-05-17
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR#614: Improve Travis
Maxime Dénès
2017-05-17
|
\
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
|
Travis: add -warn-error targets (standard and 4.04.1 ocaml)
Gaetan Gilbert
2017-05-17
*
|
|
|
|
|
|
|
|
Merge PR#630: [interp] [ast] Make raw_cases_pattern_expr private + small cleanup
Maxime Dénès
2017-05-17
|
\
\
\
\
\
\
\
\
\
|
|
*
|
|
|
|
|
|
|
Travis: deduplicate package list for coqide+documentation targets
Gaetan Gilbert
2017-05-17
|
|
*
|
|
|
|
|
|
|
Travis: do not run the tests if building Coq fails
Gaetan Gilbert
2017-05-17
|
|
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
Merge PR#635: Fixing #5522 (anomaly with free vars of pat)
Maxime Dénès
2017-05-17
|
|
|
|
\
\
\
\
\
\
*
|
|
|
\
\
\
\
\
\
Merge PR#636: Miscellaneous typos, dead code, etc.
Maxime Dénès
2017-05-17
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR#639: Stop using auto with * in two proofs.
Maxime Dénès
2017-05-17
|
\
\
\
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
Stop using auto with * in two proofs.
Théo Zimmermann
2017-05-16
|
/
/
/
/
/
/
/
/
/
/
|
|
|
|
|
|
|
|
*
|
Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.
Hugo Herbelin
2017-05-16
|
|
|
|
|
|
|
|
*
|
Adding support for using grammar entries returning no value in EXTEND.
Hugo Herbelin
2017-05-16
|
|
_
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
Simplified compaction criterion + tests.
Pierre Courtieu
2017-05-16
|
|
|
|
|
*
|
|
|
Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).
Hugo Herbelin
2017-05-16
|
|
|
|
|
*
|
|
|
Fixing a bug with nested "as" clauses in "match".
Hugo Herbelin
2017-05-16
|
|
|
|
*
|
|
|
|
Merge PR#624: Switch bedrock to mit-plv base
Maxime Dénès
2017-05-16
|
|
|
|
|
\
\
\
\
\
|
|
|
|
|
|
/
/
/
/
|
|
|
|
|
/
|
|
|
|
*
|
|
|
|
|
|
|
|
Merge PR#626: Add documentation for Set Ltac Batch Debug
Maxime Dénès
2017-05-16
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR#629: A couple of simple updates for Travis
Maxime Dénès
2017-05-16
|
\
\
\
\
\
\
\
\
\
\
|
|
|
*
|
|
|
|
|
|
|
Dead code in coqdep.
Hugo Herbelin
2017-05-15
[next]
Pierre Letouzey
Maxime Dénès
Gaetan Gilbert
Hugo Herbelin
Jason Gross
Jason Gross
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Théo Zimmermann
Pierre Courtieu