| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-04-27 | Optimization in building a return clause by pattern-matching: do not | Hugo Herbelin | |
| build a default case if the pattern is irrefutable. It did not matter in practice because we did not check for unused clauses in this case. | |||
| 2016-04-25 | Removing dead code in Compat. | Pierre-Marie Pédrot | |
| 2016-04-25 | Fixing bug #4684: Singleton list notation unusable in 8.5pl1. | Pierre-Marie Pédrot | |
| 2016-04-25 | Print magic numbers in bad magic error message | Tej Chajed | |
| 2016-04-25 | Simplifying and uniformizing the implementation of tactic notations. | Pierre-Marie Pédrot | |
| This branch mainly provides two features: 1. The resolution of tactic notation scopes is not tied to a hardwired Pcoq registration anymore. We expose instead an API to interpret names as a given generic argument, effectively reversing the logical dependency between parsing entries and generic arguments. 2. ML tactics do not declare their own notation system anymore. They rely instead on plain tactic notations, except for a little hack due to the way we currently interpret toplevel values. | |||
| 2016-04-25 | Removing dead code related to printing of ML tactics in Pptactic. | Pierre-Marie Pédrot | |
| 2016-04-25 | Merging the ML tactic notation and plain Tactic Notation mechanisms. | Pierre-Marie Pédrot | |
| 2016-04-25 | Factorizing code in tactic notations. | Pierre-Marie Pédrot | |
| 2016-04-25 | Documenting API. | Pierre-Marie Pédrot | |
| 2016-04-24 | avoid communicating to the serarch interface using raw strings. | Gregory Malecha | |
| - This patch changes the search interface to take [Str.regexp]s, [constr_pattern]s, and [DirPath.t] instead of [string]s and [string list]s. - Convenience functions are provided to do the translation. | |||
| 2016-04-24 | One more word about checking 4.01.0 with -debug and camlp4. | Hugo Herbelin | |
| 2016-04-24 | Remove dead registering code in Pcoq. | Pierre-Marie Pédrot | |
| 2016-04-24 | Disentangle tactic notation resolution from Pcoq. | Pierre-Marie Pédrot | |
| Instead of relying on entry names as given by a hardwired registering scheme in Pcoq, we recover them first through a user-defined map, and fallback on generic argument names. | |||
| 2016-04-24 | Higher-level API for tactic notations. | Pierre-Marie Pédrot | |
| 2016-04-24 | Factorizing the declaration of ML notation printing in Tacentries. | Pierre-Marie Pédrot | |
| 2016-04-24 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-04-22 | Fixing output test Notations2. | Hugo Herbelin | |
| 2016-04-22 | Mention problems with fix of #4582 in CHANGES. | Maxime Dénès | |
| 2016-04-22 | Mention #4548 (fixed) in CHANGES. | Maxime Dénès | |
| 2016-04-20 | Adding an OCaml printer for pre-initialization anomalies. | Pierre-Marie Pédrot | |
| 2016-04-19 | Do that "make" in test-suite writes failures as a default together | Hugo Herbelin | |
| with a more explicit message. | |||
| 2016-04-19 | Fixing #4677 (collision of a global variable and of a local variable | Hugo Herbelin | |
| while eta-expanding a notation) + a more serious variant of it (alpha-conversion incorrect wrt eta-expansion). | |||
| 2016-04-19 | Fixing 50266aab on incompatibility of OCaml 4.01.0 with option -debug. | Hugo Herbelin | |
| This was only when compiling with Camlp4 and it was producing an assertion failure in asmcomp/emitaux.ml at line 226, reported as OCaml's bug #6243. Note: The issue of a problematic compilation with 4.01.0 was raised at last WG. | |||
| 2016-04-19 | Revert "Fixing printing of surrounding parentheses in "ltac:"." | Hugo Herbelin | |
| I made a confusion between ltac: in constr and ltac: in tactics, the one needing parentheses in v8.5 but the latter needing parentheses only in trunk. This reverts commit f5dc54519f2a62bab2f7b9059e8c3c8dc53619be. | |||
| 2016-04-18 | Bugfix micromega: more careful syntaxification of terms of the form (Rinv t) | Frédéric Besson | |
| Bug uncovered by ekcburak@hotmail.com https://sympa.inria.fr/sympa/arc/coq-club/2016-04/msg00006.html Now, terms of the the form (Rinv t) are only syntaxified when t evaluates to a non-zero constant. | |||
| 2016-04-18 | [pp] Ensure Format is called with top level boxes. | Emilio Jesus Gallego Arias | |
| The documentation of Ocaml's `Format` module specifies: > The behaviour of pretty-printing commands is unspecified if there is > no opened pretty-printing box. Each box opened via one of the open_ > functions below must be closed using close_box for proper > formatting. Otherwise, some of the material printed in the boxes may > not be output, or may be formatted incorrectly. (http://caml.inria.fr/pub/docs/manual-ocaml/libref/Format.html) However, [lib/pp.ml] seems not to take lots of precautions to ensure that format is always called with an enclosing box. If `log_via_feedback` is set, [lib/pp.ml:string_of_ppcmds] will call `msg_with` without a top-level enclosing box, resulting in poor display results like mismatched width. Note that there are more functions affected, but these codepaths don't seem to matter when `log_via_feedback` is set. A small cleanup of pp.ml may be in order. | |||
| 2016-04-17 | Building lazily a few debugging messages involving expressions of commands | Hugo Herbelin | |
| so that they are not silently computed when not in debugging mode. | |||
| 2016-04-17 | Updating configure.ml wrt Coq not compilable with OCaml 4.01.0 in debug mode. | Hugo Herbelin | |
| 2016-04-17 | Fixing printing of surrounding parentheses in "ltac:". | Hugo Herbelin | |
| 2016-04-17 | Updating OCaml version number needed for 8.6. | Hugo Herbelin | |
| 2016-04-17 | Add changelog for 8.5pl1 after the fact. | Maxime Dénès | |
| Will be displayed on the website, but not part of the package. | |||
| 2016-04-15 | Build stm debugging messages lazily so that they are not silently | Hugo Herbelin | |
| computed when not in debugging mode (especially those printing a command). | |||
| 2016-04-15 | Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh | Pierre Courtieu | |
| 2016-04-15 | Cleaning unpolished commit 0dfd0fb7d7 on basic functions about union type. | Hugo Herbelin | |
| 2016-04-14 | This is an attempt to clarify terminology in choosing variable names | Hugo Herbelin | |
| in file indtypes.ml so that it is easier to follow what the code is doing. This is a purely alpha-renaming commit (if no mistakes). Note: was submitted as pull request #116. | |||
| 2016-04-14 | Moving and enhancing the grammar_tactic_prod_item_expr type. | Pierre-Marie Pédrot | |
| 2016-04-13 | Uniformizing the semantics of ARGUMENT EXTEND macros. | Pierre-Marie Pédrot | |
| Most notably, we bring the single argument and three argument variants closer, so that the various TYPED AS clauses may be optional. Compile-time warnings have been added for redundant clauses. | |||
| 2016-04-12 | Adding toplevel representation sharing for some generic arguments. | Pierre-Marie Pédrot | |
| 2016-04-12 | Removing redundant *_TYPED AS clauses in EXTEND statements. | Pierre-Marie Pédrot | |
| 2016-04-12 | Adding warnings for inferrable *_TYPED AS clauses. | Pierre-Marie Pédrot | |
| 2016-04-12 | Allowing optional RAW_TYPED and GLOB_TYPED clauses in ARGUMENT EXTEND. | Pierre-Marie Pédrot | |
| 2016-04-12 | Warning for redundant TYPED AS clauses. | Pierre-Marie Pédrot | |
| 2016-04-12 | Allowing simple ARGUMENT EXTEND not to mention their self type. | Pierre-Marie Pédrot | |
| The TYPED AS clause was useless when defining a fresh generic argument. Instead of having to write it mandatorily, we simply make it optional. | |||
| 2016-04-12 | Allowing the presence of TYPED AS in specialized ARGUMENT EXTEND. | Pierre-Marie Pédrot | |
| This allows to use the ARGUMENT EXTEND macro while sharing the same toplevel dynamic representation as another argument. | |||
| 2016-04-12 | A fix to #4666 (Exc_located capsule added by camlp5 overwriting | Hugo Herbelin | |
| location set by lexer). This improves on abb4e7b0c by recovering the lexer location. AFAICS, it has an effect on lexer's errors Unterminated_comment and Unterminated_string. The other errors were not wrongly located, presumably because the Exc_located location added by camlp5 coincided with the location given by the lexer. | |||
| 2016-04-12 | Quick fix for #4603 (part 2): Anomaly: Universe undefined | Maxime Dénès | |
| This is a follow-up on Matthieu's 7e7b5684 The Definition command was classified incorrectly when a body was provided. This fix is a bit ad-hoc. A better one would require more expressiveness in side effect classification, but I'll do it in trunk only since it could impact plugins. Thanks a lot to Enrico for his help! | |||
| 2016-04-12 | FIX: HTML version of Chapter 4 of the Reference Manual | Matej Kosik | |
| 2016-04-12 | Fixing printing of "destruct in" after ce71ac17268f. | Hugo Herbelin | |
| 2016-04-12 | TYPOGRAPHY: adding missing \noindent macros | Matej Kosik | |
| 2016-04-11 | Removing the typed-level tactic_expr type. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |