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
*
MMapAVL: implementing MMapInterface via AVL trees
Pierre Letouzey
2015-04-02
*
ZArith/Int.v: some modernizations
Pierre Letouzey
2015-04-02
*
MMapPositive: some improvements
Pierre Letouzey
2015-04-02
*
Accomodating #4166 (providing "Require Import OmegaTactic" as a
Hugo Herbelin
2015-04-01
*
Fixing a few typos + some uniformization of writing in doc.
Hugo Herbelin
2015-04-01
*
More clarifications on loadpaths.
Pierre-Marie Pédrot
2015-04-01
*
Documenting "From * Require *" and clearing a bit the loadpath chapter.
Pierre-Marie Pédrot
2015-04-01
*
From X Require Y looks for X with absolute path, disregarding -R.
Pierre-Marie Pédrot
2015-04-01
*
Fixing inclusion of user contrib directory in the loadpath.
Pierre-Marie Pédrot
2015-04-01
*
Fixing test-suite.
Pierre-Marie Pédrot
2015-04-01
*
Removing a probably incorrect on-the-fly require in a tactic.
Pierre-Marie Pédrot
2015-04-01
*
Removing references to deprecated syntax -I/-R -as.
Pierre-Marie Pédrot
2015-03-31
*
Removing the unused root flag from loadpaths.
Pierre-Marie Pédrot
2015-03-31
*
Fixing test-suite.
Pierre-Marie Pédrot
2015-03-31
*
A more reasonable implementation of Loadpath.
Pierre-Marie Pédrot
2015-03-31
*
Declarative mode: fix proof modes.
Arnaud Spiwack
2015-03-31
*
Declarative mode: fix vernac classification.
Arnaud Spiwack
2015-03-31
*
Declarative mode: plug the specialised printers back.
Arnaud Spiwack
2015-03-31
*
Better formatting of messages in proofs.
Arnaud Spiwack
2015-03-31
*
Generalisation of the "end command" argument of the goal printer.
Arnaud Spiwack
2015-03-31
*
Fix various typos in documentation
Matěj Grabovský
2015-03-31
*
Do not escape "'" when outputting to html, especially not using "´".
Guillaume Melquiond
2015-03-31
*
grammar: export constr_eval
Enrico Tassi
2015-03-30
*
grammar: export hypident
Enrico Tassi
2015-03-30
*
camlp4: grep away warnings in output/* tests
Enrico Tassi
2015-03-30
*
coq_makefile: fix compilation with camlp4
Enrico Tassi
2015-03-30
*
fix code and bound for SWITCH instruction.
Benjamin Gregoire
2015-03-30
*
Ensuring more invariants in Constr_matching.
Pierre-Marie Pédrot
2015-03-29
*
Adding test for bug #4165.
Pierre-Marie Pédrot
2015-03-29
*
Fixing bug #4165.
Pierre-Marie Pédrot
2015-03-29
*
Normalize scope names before storing them in vo files. (Fix for bug #4162)
Guillaume Melquiond
2015-03-27
*
Putting the From parameter of the Require command into the AST.
Pierre-Marie Pédrot
2015-03-27
*
STM: refine the notion of "simply a tactic"
Enrico Tassi
2015-03-27
*
Properly handle extra "clean" targets with coq_makefile.
Guillaume Melquiond
2015-03-27
*
use a more compact representation of non-constant constructors
Benjamin Gregoire
2015-03-27
*
allows the vm to deal with inductive type with 8388607 constant constructors ...
Benjamin Gregoire
2015-03-26
*
fix compilation
Benjamin Gregoire
2015-03-26
*
Fix bug 4157,
Benjamin Gregoire
2015-03-26
*
add coqdep in distributed_exec, else make does not work.
Benjamin Gregoire
2015-03-26
*
STM: change how proof mode switching commands are handled (decl_mode)
Enrico Tassi
2015-03-26
*
Fix vm compiler to refuse to compile code making use of inductives with
Matthieu Sozeau
2015-03-25
*
More clever representation of substituted Cemitcode.
Pierre-Marie Pédrot
2015-03-25
*
Summary: fix code to detect functional values in summary
Enrico Tassi
2015-03-25
*
STM: avoid processing asynchronously empty proofs (Close: #4134)
Enrico Tassi
2015-03-25
*
Exporting memory representation of STM tasks for votour.
Pierre-Marie Pédrot
2015-03-25
*
Fully fixing bug #3491 (anomaly when building _rect scheme in the
Hugo Herbelin
2015-03-25
*
Another example about the consequence of a wrong computation of the
Hugo Herbelin
2015-03-25
*
Use kernel names instead of user names when looking for coercions. (Fix for b...
Guillaume Melquiond
2015-03-25
*
coqc: fix --help
Enrico Tassi
2015-03-25
*
Correcting a bug introduced by universes polymorphism
jforest
2015-03-25
[next]