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
...
*
lib/Xml_parser: Cosmetics.
Regis-Gianas
2014-11-04
*
lib/Xml_parser: Cosmetics.
Regis-Gianas
2014-11-04
*
Xml_lexer: Handle non-breakable spaces.
Regis-Gianas
2014-11-04
*
ide/{ide_slave.ml, interfaces}: Coerce input and output of requests between i...
Regis-Gianas
2014-11-04
*
ide/wg_ProofView: Do not refer to the {Proof} internal module, use {Interface...
Regis-Gianas
2014-11-04
*
ide/{Xmlprotocol,Interface,Ide_slave}: New command "annotate".
Regis-Gianas
2014-11-04
*
Ppvernac: Publish new rich pretty-printer.
Regis-Gianas
2014-11-04
*
Ppannotation.t: New constructor AVernac.
Regis-Gianas
2014-11-04
*
Ppvernacsig: New.
Regis-Gianas
2014-11-04
*
Ppvernac.Make: New
Regis-Gianas
2014-11-04
*
Ppvernac: Cosmetics.
Regis-Gianas
2014-11-04
*
Ppannotation: New.
Regis-Gianas
2014-11-04
*
RichPp: New module.
Regis-Gianas
2014-11-04
*
Xml_datatype.gxml: New type for semi-structured documents.
Regis-Gianas
2014-11-04
*
lib/Pp: Publish combinators for tags opening and closing.
Regis-Gianas
2014-11-04
*
printing/Ppconstr.Make:
Regis-Gianas
2014-11-04
*
lib/Pp.ppcmd_token:
Regis-Gianas
2014-11-04
*
lib/Pp: Cosmetics.
Regis-Gianas
2014-11-04
*
printing/Ppconstr.print_hunks:
Regis-Gianas
2014-11-04
*
printing/Ppconstr: Cosmetics.
Regis-Gianas
2014-11-04
*
Removing the old rename tactic.
Pierre-Marie Pédrot
2014-11-04
*
Fixing careless name confusion in CHANGES.
Pierre-Marie Pédrot
2014-11-04
*
Documenting the change of semantics of the replace tactic.
Pierre-Marie Pédrot
2014-11-04
*
Experimentally applying eager evar substitution at the same time as
Hugo Herbelin
2014-11-04
*
test suite: some reproduction cases for recently-reported bugs.
Xavier Clerc
2014-11-04
*
Test for bug #2149.
Pierre-Marie Pédrot
2014-11-04
*
Writing rename_hyps in the new monad.
Pierre-Marie Pédrot
2014-11-03
*
New bugs revealed fixed: #3408 by (probably) Maxime's commits
Hugo Herbelin
2014-11-03
*
Now that evars can be parsed, protect strongly Check from calling kernel with...
Hugo Herbelin
2014-11-03
*
Fixing confused code for interpretations of evar instances.
Hugo Herbelin
2014-11-03
*
vernac_classifier: VernacDeclareTacticDefinition does not alter the parser
Enrico Tassi
2014-11-03
*
Show: do print the goals
Enrico Tassi
2014-11-03
*
STM: code refactoring
Enrico Tassi
2014-11-03
*
Subtle swap of lines to preserve VarInstance src field before checking
Hugo Herbelin
2014-11-03
*
Fix to 844431761 on improving elimination with indices, getting rid of
Hugo Herbelin
2014-11-03
*
STM: fix printing of goals when on a tty interface
Enrico Tassi
2014-11-03
*
Fix error reporting id on VtUnknown commands
Enrico Tassi
2014-11-03
*
Fixing inefficiency in typeclass resolution.
Pierre-Marie Pédrot
2014-11-03
*
Saving some nf_evars in the code of destruct/induction.
Hugo Herbelin
2014-11-02
*
Improving elimination with indices, getting rid of intrusive residual
Hugo Herbelin
2014-11-02
*
Some reorganization of the code for destruct/induction:
Hugo Herbelin
2014-11-02
*
Fixing subterm matched for destruct when it is matched from prefix.
Hugo Herbelin
2014-11-02
*
Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".
Hugo Herbelin
2014-11-02
*
Plural and singular forms in error messages.
Hugo Herbelin
2014-11-02
*
Cosmetic changes.
Hugo Herbelin
2014-11-02
*
Fixing 1177da327 (reorganization of the test for generic selection of
Hugo Herbelin
2014-11-02
*
Fixing file destruct.v.
Hugo Herbelin
2014-11-02
*
Document [Info] command.
Arnaud Spiwack
2014-11-01
*
Info: the warning message of the defunct [info] tactic now points to the [Inf...
Arnaud Spiwack
2014-11-01
*
Info: do not record info trace unless needed.
Arnaud Spiwack
2014-11-01
[prev]
[next]