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
*
Fixing one part of #2830 (anomaly "defined twice" due to nested calls to
herbelin
2013-01-28
*
native_compute: Fixed dependencies compilation order.
mdenes
2013-01-28
*
Added backtrace information to anomalies
ppedrot
2013-01-28
*
Ordered evars by level of dependency in the merging phase of unification
herbelin
2013-01-27
*
Improving formatting of output of "Test table".
herbelin
2013-01-27
*
Fixed bug #2967 (some missing check on ill-formed recursive notation strings).
herbelin
2013-01-27
*
Slightly improving some debugging printing and error message for modules.
herbelin
2013-01-27
*
Avoid failure in debugger when printing Ltac names.
herbelin
2013-01-27
*
updating ide/coq documentation
ppedrot
2013-01-26
*
Monadification of coqtop queries in CoqIDE
ppedrot
2013-01-26
*
Uniformization of Coq tasks
ppedrot
2013-01-26
*
Better handling of escape find in CoqIDE
ppedrot
2013-01-25
*
Better Undo/Redo mechanism
ppedrot
2013-01-25
*
Trying to fix CoqIDE undo/redo mechanism
ppedrot
2013-01-25
*
Fixing autocompletion in CoqIDE
ppedrot
2013-01-25
*
Fixup last commit
ppedrot
2013-01-25
*
Hugo request: CoqIDE find on enter
ppedrot
2013-01-25
*
Reductionops: whd_state_gen can take and answers a cst_stack too
pboutill
2013-01-24
*
Fixed parsing of -no-native-compiler flag.
mdenes
2013-01-24
*
Native compiler: warnings were not turned off for OCaml 3.11
mdenes
2013-01-24
*
Coqide: limit read buffer size to 4096 (pipe size in win32)
letouzey
2013-01-23
*
Coqide: avoid potentially blocking read on coqtop channel
letouzey
2013-01-22
*
Added .native to .gitignore
ppedrot
2013-01-22
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Revert "remove -rectypes except for term.ml"
mdenes
2013-01-22
*
- Fix evarconv so that we have complete eta-conversion:
msozeau
2013-01-22
*
Fix bug 2958: Inductive deep in in clause are impossible
pboutill
2013-01-21
*
Last test-suite not in Symmetric Patterns syntax
pboutill
2013-01-21
*
I forget to use git log before git svn dcommit ...
pboutill
2013-01-18
*
Evarconv: Check stack before term in Canonical Structure approuval
pboutill
2013-01-18
*
Unset Asymmetric Patterns
pboutill
2013-01-18
*
Revert "coq_makefile: use coqdep instead of ocamldep on .ml4 files"
pboutill
2013-01-18
*
Envar: in w32, add .exe when searching for caml binaries
letouzey
2013-01-12
*
Coqmktop and camlp4 : sequel to commit 16113
letouzey
2013-01-12
*
Coq_makefile: quoting paths
pboutill
2013-01-07
*
Coq_makefile: -extra & -phony-extra for user defined makefile rule
pboutill
2013-01-07
*
Fixup notation printing in patterns
pboutill
2013-01-07
*
* Kernel/Terms:
regisgia
2013-01-06
*
Avoiding collision between Camlp4 Loc.Exc_located and Coq's Loc.Exc_located.
herbelin
2012-12-22
*
nat_iter n f x -> nat_rect _ x (fun _ => f) n
pboutill
2012-12-21
*
Yet a new reduction tactic in Coq : cbn
pboutill
2012-12-21
*
Awful heuristic to refold mutual fixpoint in reductionops
pboutill
2012-12-21
*
Fixup and comment reductionops
pboutill
2012-12-21
*
Reductionops reduction machine can refold constant
pboutill
2012-12-19
*
Evarconv.Pseudorigid erasure
pboutill
2012-12-19
*
Coqide: cleaner Coq.PrintOpt and session creation
letouzey
2012-12-19
*
Array.create is deprecated
pboutill
2012-12-19
*
GtkData.set_default_modifiers and no access to <primary> in lablgtk -> unsuab...
pboutill
2012-12-19
*
Fix coqtop -config when absolute path have been given for ocaml*
pboutill
2012-12-19
*
Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)
letouzey
2012-12-18
[next]