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
...
*
Dedicated type for on-demand objects in Library.
Pierre-Marie Pédrot
2015-03-23
*
coqchk: more prints when -debug
Enrico Tassi
2015-03-23
*
Load: don't give anomaly on aborted proofs (Close: #3882)
Enrico Tassi
2015-03-23
*
Announcing * and ** which were not official yet in 8.4.
Hugo Herbelin
2015-03-22
*
Qed export -> Qed exporting
Enrico Tassi
2015-03-22
*
Aliasing give_up with admit
Enrico Tassi
2015-03-22
*
STM: if Set Universe Polymorphism then synchronous (#4119)
Enrico Tassi
2015-03-22
*
STM: do not delegate proofs containing Print
Enrico Tassi
2015-03-22
*
STM: after every command restore the expected proof mode
Enrico Tassi
2015-03-22
*
typo
Enrico Tassi
2015-03-22
*
Index MMaps files, otherwise documentation cannot be built. (Fix for bug #4107)
Guillaume Melquiond
2015-03-21
*
Avoid segfault from code extracted to ghc. (Fix for bug #1257)
Guillaume Melquiond
2015-03-21
*
Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)
Guillaume Melquiond
2015-03-21
*
Do not revert parameter lists when extracting singleton types to Haskell. (Fi...
Guillaume Melquiond
2015-03-21
*
Fixed #4138. In emacs mode Set/Unset does not print the goal anymore.
Pierre Courtieu
2015-03-20
*
More sharing in module substitution.
Pierre-Marie Pédrot
2015-03-18
*
add -type-in-type to the usage message
Daniel R. Grayson
2015-03-18
*
Fixing internal representation of Dyn.t in votour.
Pierre-Marie Pédrot
2015-03-18
*
Add function to fix the non-substituted universe variables of an evar_map.
Matthieu Sozeau
2015-03-17
*
Removing the whole library content from the summary.
Pierre-Marie Pédrot
2015-03-16
*
More invariants in Library.
Pierre-Marie Pédrot
2015-03-16
*
gitattributes: add `.mailmap` file to the list of files excluded from the `.t...
Arnaud Spiwack
2015-03-16
*
Gitattributes file added to generate archive.
Guillaume Claret
2015-03-16
*
Adding a primitive to dump the current association table of dynamic types.
Pierre-Marie Pédrot
2015-03-16
*
STM: -debug: better explanation of why not async (#4125)
Enrico Tassi
2015-03-15
*
STM: -quick: async no Proof using but no Section (#4124)
Enrico Tassi
2015-03-15
*
End of Bug 3986 - make cleanall removes .*.aux files
Pierre Boutillier
2015-03-14
*
Bug 3981 ends to convice me that subdirs in coq_makefile deverse a warning
Pierre Boutillier
2015-03-14
*
Fix Bug 3548 - Makefile should fallback gracefully in the absence of codesign
Pierre Boutillier
2015-03-14
*
Fix compilation with forthcoming Ocaml version 4.03.
Arnaud Spiwack
2015-03-13
*
Declarative mode: make it so that unfocussing can only be done for closed sub...
Arnaud Spiwack
2015-03-13
*
Declarative mode: remove dead code.
Arnaud Spiwack
2015-03-13
*
Declarative mode: remove a superfluous [set_proof_mode].
Arnaud Spiwack
2015-03-13
*
Declarative mode: fix the focus behaviour.
Arnaud Spiwack
2015-03-13
*
rewiring Czar printers that were disabled
Pierre Corbineau
2015-03-13
*
CHANGES: more correct equivalent to "constructor tac" syntax.
Arnaud Spiwack
2015-03-13
*
Add some tests for tryif
Jason Gross
2015-03-13
*
Fixing #4127 (command for locating exists notation in refman changed).
Hugo Herbelin
2015-03-13
*
Fixing bug #4055.
Pierre-Marie Pédrot
2015-03-12
*
Fix double print in decl_mode.
Enrico Tassi
2015-03-11
*
Fix regression in HoTT_coq_014.v
Enrico Tassi
2015-03-11
*
CoqIDE: load first _CoqProject file found and notify the user
Enrico Tassi
2015-03-11
*
CoqIDE: fix tag colors to support superposing unsafe and partial
Enrico Tassi
2015-03-11
*
CoqIDE: restore module/proof name in info bar
Enrico Tassi
2015-03-11
*
CoqIDE: do not lose tag on Qed ending focused proof
Enrico Tassi
2015-03-11
*
STM: ease re-editing of Admitted proofs
Enrico Tassi
2015-03-11
*
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
Enrico Tassi
2015-03-11
*
Do not display the status of monomorphic constants unless in universe-polymor...
Guillaume Melquiond
2015-03-09
*
Test for bug #2951.
Pierre-Marie Pédrot
2015-03-08
*
Fixing bug #2951.
Pierre-Marie Pédrot
2015-03-08
[prev]
[next]