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
*
Renaming functions in Typing to stick to the standard e_* scheme.
Pierre-Marie Pédrot
2016-02-15
*
Monotonizing the Evarutil module.
Pierre-Marie Pédrot
2016-02-15
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-13
|
\
|
*
Do not give a name to anonymous evars anymore. See bug #4547.
Pierre-Marie Pédrot
2016-02-13
|
*
STM: always stock in vio files the first node (state) of a proof
Enrico Tassi
2016-02-10
|
*
STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530
Enrico Tassi
2016-02-10
|
*
Don't fail fatally if PATH is not set.
Emilio Jesus Gallego Arias
2016-02-10
|
*
Improving error message with missing patterns in the presence of
Hugo Herbelin
2016-02-08
|
*
Optimizing the universes_of_constr_function.
Pierre-Marie Pédrot
2016-02-03
|
*
Optimizing the computation of frozen evars.
Pierre-Marie Pédrot
2016-02-03
*
|
Adding a "get" primitive to map signature.
Pierre-Marie Pédrot
2016-02-03
|
*
Opacifying the type of evar naming structure in Evd.
Pierre-Marie Pédrot
2016-02-03
|
*
More compact representation for evar resolvability flag.
Pierre-Marie Pédrot
2016-02-03
*
|
Removing a source of type-unsafeness in Pcoq.
Pierre-Marie Pédrot
2016-02-02
*
|
Infering atomic ML entries from their grammar.
Pierre-Marie Pédrot
2016-02-01
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
|
\
|
|
*
Fix bug #4537: Coq 8.5 is slower in typeclass resolution.
Pierre-Marie Pédrot
2016-01-27
|
*
Fixing bde12b70 about reporting ill-formed constructor.
Hugo Herbelin
2016-01-26
|
*
Tentative fix for bug #4522: Incorrect "Warning..." on windows.
Pierre-Marie Pédrot
2016-01-24
|
*
Fixing bug #4373: coqdep does not know about .vio files.
Pierre-Marie Pédrot
2016-01-24
|
*
Fixing bug #3826: "Incompatible module types" is uninformative.
Pierre-Marie Pédrot
2016-01-24
|
*
Adding a test for bug #4378.
Pierre-Marie Pédrot
2016-01-24
|
*
Fixing bug #4495: Failed assertion in metasyntax.ml.
Pierre-Marie Pédrot
2016-01-24
|
*
Fixing bug #4511: evar tactic can create non-typed evars.
Pierre-Marie Pédrot
2016-01-24
|
*
Fix bug #4503: mixing universe polymorphic and monomorphic
Matthieu Sozeau
2016-01-23
|
*
Fix bug #4519: oops, global shadowed local universe level bindings.
Matthieu Sozeau
2016-01-23
|
*
Implement support for universe binder lists in Instance and Program Fixpoint/...
Matthieu Sozeau
2016-01-23
|
*
Fix bug #4506. Using betadeltaiota_nolet might produce terms of the form
Matthieu Sozeau
2016-01-23
*
|
Fixing a use of "clear" on an non-existing hypothesis in intro-patterns.
Hugo Herbelin
2016-01-22
|
*
Restore warnings produced by the interpretation of the command line
Hugo Herbelin
2016-01-22
*
|
New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).
Hugo Herbelin
2016-01-21
|
*
Compile OS X binaries without native_compute support.
Maxime Dénès
2016-01-21
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
|
Stronger invariants on the use of the introduction pattern (pat1,...,patn).
Hugo Herbelin
2016-01-21
*
|
Fixing some problems with double induction.
Hugo Herbelin
2016-01-21
*
|
Code simplification in elim.ml.
Hugo Herbelin
2016-01-20
*
|
Fixing a bug with introduction patterns over inductive types containing let-ins.
Hugo Herbelin
2016-02-18
|
*
Update cic.mli MD5 after header update.
Maxime Dénès
2016-01-20
|
*
Update version number in configure.
Maxime Dénès
2016-01-20
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
|
*
Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.
Maxime Dénès
2016-01-20
|
*
Documenting Set Bullet Behavior.
Hugo Herbelin
2016-01-20
|
*
Clarifying the documentation of tactics "cbv" and "lazy".
Hugo Herbelin
2016-01-20
|
*
Fixing Not_found on unknown bullet behavior.
Hugo Herbelin
2016-01-20
|
*
Fix bug #4420: check_types was losing universe constraints.
Matthieu Sozeau
2016-01-19
*
|
Universes algorithm : clarified comments
Jacques-Henri Jourdan
2016-01-17
*
|
Moving val_cast to Tacinterp.
Pierre-Marie Pédrot
2016-01-17
*
|
Getting rid of the awkward unpack mechanism from Genarg.
Pierre-Marie Pédrot
2016-01-17
*
|
Simplification and type-safety of Pcoq thanks to GADTs in Genarg.
Pierre-Marie Pédrot
2016-01-17
*
|
Exporting Genarg implementation in the API.
Pierre-Marie Pédrot
2016-01-17
[next]