| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-06-03 | Removing "rename" from the tactic AST. | Pierre-Marie Pédrot | |
| 2016-06-03 | Removing "exact" from the tactic AST. | Pierre-Marie Pédrot | |
| 2016-06-03 | Removing "intro" from the tactic AST. | Pierre-Marie Pédrot | |
| Note that this breaks the compatibility, in a beneficial way I believe. Tactics defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction on a local identifier anymore. They must use the "fresh" primitive instead. | |||
| 2016-06-03 | Removing "double induction" from the tactic AST. | Pierre-Marie Pédrot | |
| 2016-06-01 | g_tactics : remove opt_bindings (2-line dead code) | Pierre Letouzey | |
| 2016-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias | |
| This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work. | |||
| 2016-05-11 | The grammar_extend function now registers unsynchronized extensions. | Pierre-Marie Pédrot | |
| This made little sense, as all the uses of this function were actually called from toplevel ML modules. This was at best useless, and at worst a source of bugs when loading plugins and messing with backtracking. | |||
| 2016-05-11 | Making the grammar command extend API purely functional. | Pierre-Marie Pédrot | |
| Instead of leaving the responsibility of extending the grammar to the caller, we ask for a list of extensions in the return value of the function. | |||
| 2016-05-11 | Moving the constr empty entry registering to the state-based API. | Pierre-Marie Pédrot | |
| 2016-05-11 | Turning the grammar extend command API into a state-passing one. | Pierre-Marie Pédrot | |
| 2016-05-11 | Moving the grammar summary to Pcoq. | Pierre-Marie Pédrot | |
| 2016-05-10 | Delimiting the use of unsafe code in Pcoq. | Pierre-Marie Pédrot | |
| 2016-05-10 | Overlooked use of Gram instead of G module in Pcoq. | Pierre-Marie Pédrot | |
| This was probably wreaking havoc in tricky undo-redo scenarii. | |||
| 2016-05-10 | Further tidying of the constr extension code. | Pierre-Marie Pédrot | |
| 2016-05-10 | Type-safe constr notations. | Pierre-Marie Pédrot | |
| This removes the last call to unsafe_grammar_extend, so that all handwritten grammar extensions are now type-safe. Grammars defined by CAMLPX EXTEND are still using the unsafe interface, but as they insert explicit casts they are deemed safe. | |||
| 2016-05-10 | AlistNsep token now accepts an arbitrary separator. | Pierre-Marie Pédrot | |
| 2016-05-10 | Simpler data structure for Arules token. | Pierre-Marie Pédrot | |
| 2016-05-10 | Purer implementation of empty level registering in Pcoq. | Pierre-Marie Pédrot | |
| 2016-05-10 | Removing the Entry module now that rules need not be marshalled. | Pierre-Marie Pédrot | |
| 2016-05-10 | Hardening the obsolete unsafe_grammar_statement API. | Pierre-Marie Pédrot | |
| 2016-05-10 | Removing dead code in Compat. | Pierre-Marie Pédrot | |
| 2016-05-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-05-09 | Rename Lexer -> CLexer. | Pierre-Marie Pédrot | |
| 2016-05-08 | Removing dead code and unused opens. | Pierre-Marie Pédrot | |
| 2016-05-04 | Removing useless generic arguments. | Pierre-Marie Pédrot | |
| 2016-04-27 | Revert "In the short term, stronger invariant on the syntax of TacAssert, what" | Hugo Herbelin | |
| This reverts commit bde36d4b00185065628324d8ca71994f84eae244. | |||
| 2016-04-27 | Revert "Fixing a mispelling coma -> comma." | Hugo Herbelin | |
| This reverts commit 857dc0aaae30805725da213b6550dc1ff3a7adb2. | |||
| 2016-04-27 | Fixing a mispelling coma -> comma. | Hugo Herbelin | |
| 2016-04-27 | In the short term, stronger invariant on the syntax of TacAssert, what | Hugo Herbelin | |
| allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause. | |||
| 2016-04-25 | Removing dead code in Compat. | Pierre-Marie Pédrot | |
| 2016-04-24 | Remove dead registering code in Pcoq. | Pierre-Marie Pédrot | |
| 2016-04-24 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-04 | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵ | Matthieu Sozeau | |
| into JasonGross-trunk-function_scope | |||
| 2016-04-01 | Getting rid of the "_mods" parsing entry. | Pierre-Marie Pédrot | |
| It was only used by setoid_ring for the Add Ring command, and was easily replaced by a dedicated argument. Moreover, it was of no use to tactic notations. | |||
| 2016-03-31 | Moving the code handling tactic notations to Tacentries. | Pierre-Marie Pédrot | |
| 2016-03-31 | Abstracting away the Summary-synchronized grammar-modifying commands. | Pierre-Marie Pédrot | |
| We provide an API so that external code such as plugins can define grammar extensions synchronized with the summary. This API is not perfect yet and is a mere abstraction of the current behaviour. In particular, it expects the user to modify the parser in an imperative way. | |||
| 2016-03-31 | Moving the Tactic Notation entry parser from Pcoq to Tacentries. | Pierre-Marie Pédrot | |
| 2016-03-20 | Adding a new Ltac generic argument for forced tactics returing unit. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving the Ltac definition command to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Print Ltac to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tactic Notation to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tacinterp to Hightactics. | Pierre-Marie Pédrot | |
| 2016-03-19 | Fixing compilation with old versions of CAMLP5. | Pierre-Marie Pédrot | |
| 2016-03-19 | Further reducing the dependencies of the EXTEND macros. | Pierre-Marie Pédrot | |
| 2016-03-19 | Moving VernacSolve to an EXTEND-based definition. | Pierre-Marie Pédrot | |
| 2016-03-19 | Moving the parsing of the Ltac proof mode to G_ltac. | Pierre-Marie Pédrot | |
| 2016-03-19 | Moving the proof mode parsing management to Pcoq. | Pierre-Marie Pédrot | |
| 2016-03-19 | Allowing generalized rules in typed symbols. | Pierre-Marie Pédrot | |
| 2016-03-19 | Do not export entry_key from Pcoq anymore. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |