index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2014-11-04
lib/Xml_printer: Handle non-breakable spaces.
Regis-Gianas
2014-11-04
lib/Xml_parser.parse: Make canonicalization optional. (By default, it is appl...
Regis-Gianas
2014-11-04
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-03
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-02
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-01
Document [Info] command.
Arnaud Spiwack
[next]