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
*
configure.ml: our configure script is now written in ML :-)
Pierre Letouzey
2013-12-20
*
Makefile.build: avoid a -pp
Pierre Letouzey
2013-12-20
*
coqc: execvp is now available even on win32
Pierre Letouzey
2013-12-20
*
coqmktop without Unix (simpler all_subdirs)
Pierre Letouzey
2013-12-20
*
Remove unused Makefile lines about .elc compilation
Pierre Letouzey
2013-12-20
*
Warning removal
Pierre Boutillier
2013-12-20
*
List: Bug 3039 weaker requirement for fold symmetric
Pierre Boutillier
2013-12-20
*
Coqdep always uses / as dir_sep
Pierre Boutillier
2013-12-20
*
micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...
Frédéric Besson
2013-12-20
*
Removing the useless pattern ident genarg.
Pierre-Marie Pédrot
2013-12-19
*
Using interp_genarg in tactic notations where possible, instead of an ad-hoc
Pierre-Marie Pédrot
2013-12-19
*
test-suite/output/Notations : evar number change
Pierre Boutillier
2013-12-19
*
Bad use of Obj.magic in interpretation of TacAlias arguments.
Pierre Boutillier
2013-12-19
*
Printing function for Stdargs in debugger
Pierre Boutillier
2013-12-19
*
Missing Fail in r16792
Pierre Boutillier
2013-12-19
*
test guard condition against feature incompatible with prop-ext
Bruno Barras
2013-12-17
*
Fix make install after 3e972b3ff8e532be233f70567c87512324c99b4e
Pierre Boutillier
2013-12-17
*
Merge branch 'trunk' of github.com:coq/coq into trunk
Matthieu Sozeau
2013-12-17
|
\
*
|
Tentative fix of the guardedness checker by Christine and me. All stdlib and ...
Matthieu Sozeau
2013-12-17
|
*
Removing the need of evarmaps in constr internalization.
Pierre-Marie Pédrot
2013-12-17
|
/
*
Get rid of messages "emitting ..." when compiling .v files
Pierre Letouzey
2013-12-16
*
A few fixes to the build system (mostly for ocamlbuild)
Pierre Letouzey
2013-12-16
*
Added test-suite for bug #2990.
Pierre-Marie Pédrot
2013-12-16
*
Dedicated inductive for return values of rewrite strategies.
Pierre-Marie Pédrot
2013-12-16
*
Do not overallocate closures' named environments in infos. Modifying the access
Pierre-Marie Pédrot
2013-12-15
*
Do not compile coqide with -thread
Pierre Boutillier
2013-12-12
*
Patch for supporting [From Xxx Require Yyy Zzz.]
Gregory Malecha
2013-12-12
*
Better unification for [projT1] and [proj1_sig].
Jason Gross
2013-12-12
*
Generalize eq_proofs_unicity
Jason Gross
2013-12-12
*
Documenting the tactic-in-term construction.
Pierre-Marie Pédrot
2013-12-11
*
Fix CoqIDE compilation under standard version of lablgtk2
Enrico Tassi
2013-12-11
*
Fixing backtrace registering of various tactic-related try-with blocks.
Pierre-Marie Pédrot
2013-12-11
*
Fix CoqIDE on windows
Enrico Tassi
2013-12-10
*
Renaming elisp files to avoid conflict with pg in distribs.
Pierre Courtieu
2013-12-10
*
Fix printing of Ltac's backtrace.
Arnaud Spiwack
2013-12-09
*
Stylistic change.
Arnaud Spiwack
2013-12-09
*
Fix test-suite/success/evars.v.
Arnaud Spiwack
2013-12-06
*
Remove duplicate test-suite file.
Arnaud Spiwack
2013-12-06
*
Fix the refine related test-suite files to account for the new refine.
Arnaud Spiwack
2013-12-06
*
Missing file in commit 1fb883.
Arnaud Spiwack
2013-12-06
*
Fix g_derive.ml4.
Arnaud Spiwack
2013-12-04
*
Documentation of the Derive plugin.
Arnaud Spiwack
2013-12-04
*
Stm: remove an assertion.
Arnaud Spiwack
2013-12-04
*
Derive plugin.
Arnaud Spiwack
2013-12-04
*
Fix Admitted.
Arnaud Spiwack
2013-12-04
*
Proof_global: fix start_proof comment after the preceding commits.
Arnaud Spiwack
2013-12-04
*
Factoring(continued).
Arnaud Spiwack
2013-12-04
*
Refactoring: storing more information in the terminator closure.
Arnaud Spiwack
2013-12-04
*
The commands that initiate proofs are now in charge of what happens when proo...
Arnaud Spiwack
2013-12-04
*
Vernac classification: allow for commands which start proofs but must be sync...
Arnaud Spiwack
2013-12-04
[next]