aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-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
2016-04-11Removing the ad-hoc tactic_expr type.Pierre-Marie Pédrot
2016-04-10Extruding the print_atom primitive.Pierre-Marie Pédrot
2016-04-10Expliciting the fact that the atomic tactic type is self-contained.Pierre-Marie Pédrot
2016-04-09A small test of Print Ltac.Hugo Herbelin
2016-04-09Removing extra spaces in printing arguments of VERNAC EXTEND.Hugo Herbelin
2016-04-09Removing automatic printing of leading space in auto_using andHugo Herbelin
2016-04-09Re-add printer for tacdef_body so that Ltac definitions are printed by pr_ver...Hugo Herbelin
2016-04-09Simplifying code for printing VERNAC EXTEND.Hugo Herbelin
2016-04-09Fixing extra space in printing inductive types with no explicit type given.Hugo Herbelin
2016-04-09In pr_clauses, do not print a leading space by default so that it canHugo Herbelin
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-09Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.vNickolai Zeldovich
2016-04-08Added compatibility coercions from Specif.v which were present in Coq 8.4.Hugo Herbelin
2016-04-08Fixing a source of inefficiency and an artificial dependency in theDaniel de Rauglaudre
2016-04-08Fixing printing of toplevel values.Pierre-Marie Pédrot
2016-04-08Fixing printing of Tactic Notations with tactic arguments.Pierre-Marie Pédrot
2016-04-07Allow to unset the refinement mode of Instance in MLMatthieu Sozeau
2016-04-07Fixing an incorrect use of prod_appvect on a term which was not aHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 05:05:40 +0000