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
*
Adding a monotonic variant of Goal.enter and Goal.nf_enter.
Pierre-Marie Pédrot
2015-10-19
*
Making Evarutil.new_evar monotonous.
Pierre-Marie Pédrot
2015-10-18
*
Constraining refine to monotonic functions.
Pierre-Marie Pédrot
2015-10-18
*
Clarifying and documenting the UState API.
Pierre-Marie Pédrot
2015-10-17
*
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-10-16
|
\
|
*
Fix #4346 1/2: native casts were not inferring universe constraints.
Maxime Dénès
2015-10-15
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
*
Fix LemmaOverloading
Matthieu Sozeau
2015-10-14
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
*
Remove misleading warning (Close #4365)
Enrico Tassi
2015-10-09
|
*
Proof using: let-in policy, optional auto-clear, forward closure*
Enrico Tassi
2015-10-08
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-06
|
\
|
|
*
Fixing emacs output in debugging mode.
Pierre Courtieu
2015-10-06
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
|
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
\
|
|
*
Univs: fix handling of evd's universes and side effects in build_by_tactic
Matthieu Sozeau
2015-10-02
|
|
*
Univs: fix handling of side effects/delayed proofs
Matthieu Sozeau
2015-10-02
|
|
/
|
*
Changed status of Info messages from notice to info.
Pierre Courtieu
2015-10-02
*
|
Removing meta_with_name from Evd.
Pierre-Marie Pédrot
2015-09-27
*
|
Removing uselessly duplicated function in Evd.
Pierre-Marie Pédrot
2015-09-27
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-25
|
\
|
|
*
Removing the generalization of the body of inductive schemes from
Hugo Herbelin
2015-09-23
|
*
Proof: suggest Admitted->Qed only if the proof is really complete (#4349)
Enrico Tassi
2015-09-20
*
|
Fix previous merge.
Maxime Dénès
2015-09-17
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-09-17
|
\
|
|
*
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
|
Opacifying the proof_terminator type.
Pierre-Marie Pédrot
2015-09-08
|
*
Reverting 16 last commits, committed mistakenly using the wrong push command.
Hugo Herbelin
2015-08-02
|
*
Removing the generalization of the body of inductive schemes from
Hugo Herbelin
2015-08-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-07-29
|
\
|
|
*
Fixing what seems to be a typo.
Hugo Herbelin
2015-07-29
|
*
Slightly improving line break formatting in Info command.
Hugo Herbelin
2015-07-27
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-06-24
|
\
|
|
*
Fix `Pp` function used by the `Info` command.
Arnaud Spiwack
2015-06-23
*
|
Merge remote-tracking branch 'forge/v8.5'
Pierre Boutillier
2015-06-22
|
\
|
|
*
STM: states coming from workers have no proof terminators (Close #4246)
Enrico Tassi
2015-06-09
|
*
Admitted does not drop poly-univ constraints (Fix #4244)
Enrico Tassi
2015-06-03
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-06-01
|
\
|
|
*
STM/Univ: save initial univs (the ones in the statement) in Proof.proof
Enrico Tassi
2015-05-29
|
*
Fix bug #4159
Matthieu Sozeau
2015-05-27
|
*
Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...
Pierre-Marie Pédrot
2015-05-18
*
|
Merge v8.5 into trunk
Hugo Herbelin
2015-05-15
|
\
|
|
*
Disable precompilation for native_compute by default.
Guillaume Melquiond
2015-05-14
|
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
|
Exposing the minimal amount of internal of the Logic monad in order to
Pierre-Marie Pédrot
2015-05-06
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-05-05
|
\
|
|
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
|
*
Tactical `progress` compares term up to potentially equalisable universes.
Arnaud Spiwack
2015-04-22
|
*
Slightly more efficient implementation of the logic monad.
Pierre-Marie Pédrot
2015-04-19
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-03-23
|
\
|
[next]