index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2017-09-27
Avoid looping when searching for CoqProject.
Maxime Dénès
2017-09-26
Merge PR #688: Binding universe constraints in Definition/Inductive/etc...
Maxime Dénès
2017-09-25
Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...
Maxime Dénès
2017-09-25
Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ...
Maxime Dénès
2017-09-25
Merge PR #1079: Avoid generated names for html pages of the reference manual ...
Maxime Dénès
2017-09-25
Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4...
Maxime Dénès
2017-09-25
Merge PR #1057: Reporting locations in error messages about notation formats.
Maxime Dénès
2017-09-25
Merge PR #1060: An optimization of tactic constructor
Maxime Dénès
2017-09-25
Merge PR #1075: Re-enable checker error messages
Maxime Dénès
2017-09-23
Discharge.ml: cosmetic renaming of some variables.
Hugo Herbelin
2017-09-23
Fixing #5755 (discharging of inductive types not correct with let-ins).
Hugo Herbelin
2017-09-23
Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).
Hugo Herbelin
2017-09-23
Fixing _rect bug for inductive types with let-ins and non-rec uniform params.
Hugo Herbelin
2017-09-22
Avoid generated names for html pages of the reference manual (bug #4742).
Guillaume Melquiond
2017-09-22
Merge PR #1055: Remove STM vernaculars
Maxime Dénès
2017-09-22
Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as exp...
Maxime Dénès
2017-09-22
Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a contex...
Maxime Dénès
2017-09-22
Merge PR #1071: Mark "Set Tactic Compat Context" as deprecated.
Maxime Dénès
2017-09-22
Merge PR #1070: Remove remaining occurrences of -just-parsing.
Maxime Dénès
2017-09-22
Merge PR #1064: coq_makefile: dont show errors from failed (ignored) rmdir
Maxime Dénès
2017-09-22
Merge PR #1063: [flags] Flag `open Flags`
Maxime Dénès
2017-09-22
Merge PR #1061: Fix appveyor build
Maxime Dénès
2017-09-21
Fix -silent flag of coqchk after ff918e4.
Maxime Dénès
2017-09-21
Adapt checker to change in locations.
Maxime Dénès
2017-09-21
Proposing meta names more distinguishable from evar names than ?M42.
Hugo Herbelin
2017-09-21
A possible fix to BZ#5750 (ability to print context of ltac subterm match).
Hugo Herbelin
2017-09-21
[checker] Add missing Feedback printer (BZ#5587)
Emilio Jesus Gallego Arias
2017-09-21
Do not reinstall preinstalled packages under AppVeyor.
Maxime Dénès
2017-09-21
Print Cygwin setup output rather than logging in to a file.
Maxime Dénès
2017-09-21
Mark "Set Tactic Compat Context" as deprecated.
Guillaume Melquiond
2017-09-21
Remove remaining occurrences of -just-parsing.
Guillaume Melquiond
2017-09-20
In gitlab set TRAVIS_BRANCH so user overlays will work as expected.
Gaëtan Gilbert
2017-09-20
coq_makefile: dont show errors from failed (ignored) rmdir
Ralf Jung
2017-09-20
[flags] Flag `open Flags`
Emilio Jesus Gallego Arias
2017-09-19
An optimization of tactic constructor.
Hugo Herbelin
2017-09-19
Merge PR #1036: Unify EConstr.t equality
Maxime Dénès
2017-09-19
Improve documentation of Status message.
Maxime Dénès
2017-09-19
Remove STM vernaculars.
Maxime Dénès
2017-09-19
Add XML protocol support for Wait.
Maxime Dénès
2017-09-19
Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).
Maxime Dénès
2017-09-19
Merge PR #1043: Disable OSX signing for temporary artifacts.
Maxime Dénès
2017-09-19
Document UState.universe_context.
Gaëtan Gilbert
2017-09-19
Don't lose names in UState.universe_context.
Gaëtan Gilbert
2017-09-19
test-suite: polymorphism
Matthieu Sozeau
2017-09-19
proof_global: cleanup and comment close_proof
Matthieu Sozeau
2017-09-19
Allow declaring universe binders with no constraints with @{|}
Gaëtan Gilbert
2017-09-19
Allow declaring universe constraints at definition level.
Matthieu Sozeau
2017-09-19
Allow empty instance parsing @{}
Matthieu Sozeau
2017-09-19
Merge PR #1024: Switch Travis to OSX 10.12 and Xcode 8.3.3.
Maxime Dénès
2017-09-19
Merge PR #920: kernel: bugfix in filter_stack_domain.
Maxime Dénès
[next]