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
...
*
|
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
*
|
Moving Tactic_debug to tactics/ folder.
Pierre-Marie Pédrot
2016-03-06
*
|
Moving Ltac traces to Tacexpr and Tacinterp.
Pierre-Marie Pédrot
2016-03-06
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
|
|
*
Rename Ephemeron -> CEphemeron.
Maxime Dénès
2016-03-04
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-21
|
\
|
|
*
Fixing the Proofview.Goal.goal function.
Pierre-Marie Pédrot
2016-02-17
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-17
|
\
\
*
|
|
CLEANUP: Renaming "Util.compose" function to "%"
Matej Kosik
2016-02-17
|
*
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
/
|
|
[prev]
[next]