aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-04-27Optimization in building a return clause by pattern-matching: do notHugo Herbelin
2016-04-25Removing dead code in Compat.Pierre-Marie Pédrot
2016-04-25Fixing bug #4684: Singleton list notation unusable in 8.5pl1.Pierre-Marie Pédrot
2016-04-25Print magic numbers in bad magic error messageTej Chajed
2016-04-25Simplifying and uniformizing the implementation of tactic notations.Pierre-Marie Pédrot
2016-04-25Removing dead code related to printing of ML tactics in Pptactic.Pierre-Marie Pédrot
2016-04-25Merging the ML tactic notation and plain Tactic Notation mechanisms.Pierre-Marie Pédrot
2016-04-25Factorizing code in tactic notations.Pierre-Marie Pédrot
2016-04-25Documenting API.Pierre-Marie Pédrot
2016-04-24avoid communicating to the serarch interface using raw strings.Gregory Malecha
2016-04-24One more word about checking 4.01.0 with -debug and camlp4.Hugo Herbelin
2016-04-24Remove dead registering code in Pcoq.Pierre-Marie Pédrot
2016-04-24Disentangle tactic notation resolution from Pcoq.Pierre-Marie Pédrot
2016-04-24Higher-level API for tactic notations.Pierre-Marie Pédrot
2016-04-24Factorizing the declaration of ML notation printing in Tacentries.Pierre-Marie Pédrot
2016-04-24Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-22Fixing output test Notations2.Hugo Herbelin
2016-04-22Mention problems with fix of #4582 in CHANGES.Maxime Dénès
2016-04-22Mention #4548 (fixed) in CHANGES.Maxime Dénès
2016-04-20Adding an OCaml printer for pre-initialization anomalies.Pierre-Marie Pédrot
2016-04-19Do that "make" in test-suite writes failures as a default togetherHugo Herbelin
2016-04-19Fixing #4677 (collision of a global variable and of a local variableHugo Herbelin
2016-04-19Fixing 50266aab on incompatibility of OCaml 4.01.0 with option -debug.Hugo Herbelin
2016-04-19Revert "Fixing printing of surrounding parentheses in "ltac:"."Hugo Herbelin
2016-04-18Bugfix micromega: more careful syntaxification of terms of the form (Rinv t)Frédéric Besson
2016-04-18[pp] Ensure Format is called with top level boxes.Emilio Jesus Gallego Arias
2016-04-17Building lazily a few debugging messages involving expressions of commandsHugo Herbelin
2016-04-17Updating configure.ml wrt Coq not compilable with OCaml 4.01.0 in debug mode.Hugo Herbelin
2016-04-17Fixing printing of surrounding parentheses in "ltac:".Hugo Herbelin
2016-04-17Updating OCaml version number needed for 8.6.Hugo Herbelin
2016-04-17Add changelog for 8.5pl1 after the fact.Maxime Dénès
2016-04-15Build stm debugging messages lazily so that they are not silentlyHugo Herbelin
2016-04-15Merge remote-tracking branch 'OFFICIAL/trunk' into morefreshPierre Courtieu
2016-04-15Cleaning unpolished commit 0dfd0fb7d7 on basic functions about union type.Hugo Herbelin
2016-04-14This is an attempt to clarify terminology in choosing variable namesHugo Herbelin
2016-04-14Moving and enhancing the grammar_tactic_prod_item_expr type.Pierre-Marie Pédrot
2016-04-13Uniformizing the semantics of ARGUMENT EXTEND macros.Pierre-Marie Pédrot
2016-04-12Adding toplevel representation sharing for some generic arguments.Pierre-Marie Pédrot
2016-04-12Removing redundant *_TYPED AS clauses in EXTEND statements.Pierre-Marie Pédrot
2016-04-12Adding warnings for inferrable *_TYPED AS clauses.Pierre-Marie Pédrot
2016-04-12Allowing optional RAW_TYPED and GLOB_TYPED clauses in ARGUMENT EXTEND.Pierre-Marie Pédrot
2016-04-12Warning for redundant TYPED AS clauses.Pierre-Marie Pédrot
2016-04-12Allowing simple ARGUMENT EXTEND not to mention their self type.Pierre-Marie Pédrot
2016-04-12Allowing the presence of TYPED AS in specialized ARGUMENT EXTEND.Pierre-Marie Pédrot
2016-04-12A fix to #4666 (Exc_located capsule added by camlp5 overwritingHugo Herbelin
2016-04-12Quick fix for #4603 (part 2): Anomaly: Universe undefinedMaxime Dénès
2016-04-12FIX: HTML version of Chapter 4 of the Reference ManualMatej Kosik
2016-04-12Fixing printing of "destruct in" after ce71ac17268f.Hugo Herbelin
2016-04-12TYPOGRAPHY: adding missing \noindent macrosMatej Kosik
2016-04-11Removing the typed-level tactic_expr type.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 10:38:25 +0000