index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
Commit message (
Expand
)
Author
Age
*
Moving "move" in the new proof engine.
Hugo Herbelin
2016-09-24
*
Adding variants enter_one and refine_one which assume that exactly one
Hugo Herbelin
2016-09-16
*
Merge remote-tracking branch 'github-coq/pr/249' into v8.6
Matthieu Sozeau
2016-09-12
|
\
|
*
no-refold patch
Paul Steckler
2016-09-09
*
|
Fast path in Clenvtac.clenv_refine typeclass resolution.
Pierre-Marie Pédrot
2016-09-09
|
/
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-09-02
|
\
|
*
Fixing name of internal refine ("simple refine").
Hugo Herbelin
2016-09-01
*
|
[pp] Fix newline issues.
Emilio Jesus Gallego Arias
2016-08-19
|
*
infoH: output via msg_* to make the XML protocol happy
Enrico Tassi
2016-08-17
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-07-13
|
\
|
|
*
Fixing printing of evar name in an error message of instantiate.
Hugo Herbelin
2016-07-13
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2016-07-04
|
\
|
*
|
closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)
Pierre Letouzey
2016-07-03
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
Add and document match, fix and cofix reduction flags.
Maxime Dénès
2016-07-01
*
|
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
|
*
Fixing #4881 (synchronizing "Declare Implicit Tactic" with backtrack).
Hugo Herbelin
2016-07-01
|
*
Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars).
Hugo Herbelin
2016-07-01
*
|
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
*
|
Optim in Clenv: use noccurn instead of depends.
Pierre-Marie Pédrot
2016-06-24
*
|
Prevent a useless evar normalization in Clenvtac.unify.
Pierre-Marie Pédrot
2016-06-20
*
|
Add documentation for goal selectors.
Cyprien Mangin
2016-06-14
*
|
Add goal range selectors.
Cyprien Mangin
2016-06-14
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-13
|
\
|
|
*
Another fix to #4782 (a typing error not captured when dealing with bindings).
Hugo Herbelin
2016-06-12
|
*
Fixing #4782 (a typing error not captured when dealing with bindings).
Hugo Herbelin
2016-06-11
*
|
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-06-09
*
|
proofs/proofs.mllib: no more proof_errors !
Pierre Letouzey
2016-06-08
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-01
|
\
|
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
*
Pfedit.get_current_context refinement (fix #4523)
Matthieu Sozeau
2016-05-26
*
|
Removing some compatibility layers in Tactics.
Pierre-Marie Pédrot
2016-05-17
*
|
Put the "cofix" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
|
Put the "fix" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
|
Put the "clear" tactic into the monad.
Pierre-Marie Pédrot
2016-05-16
|
*
Fix bug #4737: cycle tactic doesn't like zero goals.
Pierre-Marie Pédrot
2016-05-16
*
|
Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"
Enrico Tassi
2016-05-10
*
|
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-30
|
\
|
|
*
Univs: fix get_current_context (bug #4603, part I)
Matthieu Sozeau
2016-03-25
|
*
Revert "refine: do check all unif problems are solved (Close: #4415, #4532)"
Enrico Tassi
2016-03-23
|
*
refine: do check all unif problems are solved (Close: #4415, #4532)
Enrico Tassi
2016-03-23
*
|
Moving Proofview to pretyping/.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving Refine to its proper module.
Pierre-Marie Pédrot
2016-03-20
*
|
Making Proofview independent of Logic.
Pierre-Marie Pédrot
2016-03-20
*
|
Making Proofview independent from Goal.
Pierre-Marie Pédrot
2016-03-20
*
|
Extruding the code for the Existential command from Proofview.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving VernacSolve to an EXTEND-based definition.
Pierre-Marie Pédrot
2016-03-19
*
|
Removing the dependency in VernacSolve in the STM.
Pierre-Marie Pédrot
2016-03-19
*
|
Fix the comment of Refine.refine
Matthieu Sozeau
2016-03-14
[next]