index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
...
|
|
|
|
*
|
|
|
|
STM: proof block detection made optional + simple test
Enrico Tassi
2016-06-06
|
|
_
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
Fixing problems introduced in 8.5 with Ltac trace report. E.g.
Hugo Herbelin
2016-06-06
|
|
|
*
|
|
|
|
-profileltac -> -profile-ltac, as per @herbelin
Jason Gross
2016-06-05
|
|
|
*
|
|
|
|
LtacProf for Coq trunk
Jason Gross
2016-06-05
|
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
*
|
|
|
|
|
|
coqtop: Add ltac/ to search path.
Matthieu Sozeau
2016-06-02
|
|
|
*
|
|
|
STM delegation policy can be customized
Enrico Tassi
2016-05-31
|
|
*
|
|
|
|
Revert "Rename Lexer -> CLexer."
Pierre-Marie Pédrot
2016-05-31
*
|
|
|
|
|
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
Univs/Program/Function: Fix bug #4725
Matthieu Sozeau
2016-05-26
|
|
|
|
|
*
Program: remove debug tracing
Matthieu Sozeau
2016-05-26
|
|
|
|
_
|
/
|
|
|
/
|
|
|
|
|
*
|
fix blanks in usage message
Enrico Tassi
2016-05-19
|
|
|
*
|
coqc: support -o option to specify output file name
Enrico Tassi
2016-05-19
|
|
_
|
/
/
|
/
|
|
|
*
|
|
|
Put the "exact_constr" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
|
|
|
Put the "clear" tactic into the monad.
Pierre-Marie Pédrot
2016-05-16
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-09
|
\
\
\
\
|
|
|
/
/
|
|
/
|
|
|
*
|
|
Fix bug #3887: Better error message for "More than one program with unsolved ...
Pierre-Marie Pédrot
2016-05-09
|
*
|
|
Rename Lexer -> CLexer.
Pierre-Marie Pédrot
2016-05-09
*
|
|
|
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
|
\
|
|
|
|
*
|
|
Fix bug #4705: coqtop accepts both -emacs and -ideslave.
Pierre-Marie Pédrot
2016-05-03
|
*
|
|
Call hooks when terminating a definition proof (bug #4663).
Guillaume Melquiond
2016-05-03
|
*
|
|
Properly handle notations containing spaces (bug #4538).
Guillaume Melquiond
2016-05-02
*
|
|
|
Revert "A heuristic to add parentheses in the presence of rules such as"
Hugo Herbelin
2016-04-27
*
|
|
|
Revert "Protect the beautifier from change in the lexer state (typically by"
Hugo Herbelin
2016-04-27
*
|
|
|
Protect the beautifier from change in the lexer state (typically by
Hugo Herbelin
2016-04-27
*
|
|
|
A heuristic to add parentheses in the presence of rules such as
Hugo Herbelin
2016-04-27
|
|
*
|
avoid communicating to the serarch interface using raw strings.
Gregory Malecha
2016-04-24
|
|
/
/
|
/
|
|
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-24
|
\
|
|
|
*
|
Building lazily a few debugging messages involving expressions of commands
Hugo Herbelin
2016-04-17
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-09
|
\
|
|
|
*
|
Allow to unset the refinement mode of Instance in ML
Matthieu Sozeau
2016-04-07
*
|
|
Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr/gitroot/coq/coq into trunk
Matej Kosik
2016-04-04
|
\
\
\
*
\
\
\
Merging "https://github.com/coq/coq/pull/94", i.e. "Traversal of inductive de...
Matej Kosik
2016-04-04
|
\
\
\
\
|
|
*
|
|
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...
Matthieu Sozeau
2016-04-04
|
|
/
|
|
|
|
/
|
|
|
|
*
|
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-30
|
\
\
\
\
\
|
|
|
_
|
/
/
|
|
/
|
|
|
*
|
|
|
|
Was too restrictive in syntactic definitions, not imagining that they
Hugo Herbelin
2016-03-28
|
*
|
|
|
Fix handling of arity of definitional classes.
Matthieu Sozeau
2016-03-24
*
|
|
|
|
Moving Tactic_debug to Hightactic.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
|
Making Evarutil independent from Reductionops.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
|
Splitting Evarutil in two distinct files.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
|
Moving Refine to its proper module.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-20
|
\
|
|
|
|
*
|
|
|
|
Moving Tacintern to Hightactics.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
|
Moving the Ltac definition command to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
|
Moving the tactic related code from Metasyntax to a new file.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
|
Moving Print Ltac to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
|
Moving Tactic Notation to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
|
Moving Tacinterp to Hightactics.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
|
Moving the use of Tactic_option from Obligations to G_obligations.
Pierre-Marie Pédrot
2016-03-19
*
|
|
|
|
Moving VernacSolve to an EXTEND-based definition.
Pierre-Marie Pédrot
2016-03-19
[prev]
[next]