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