Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | [location] Use located in misctypes. | 2017-04-24 | |
| | |||
* | [camlpX] Remove camlp4 compat layer. | 2017-04-07 | |
| | | | | | | | | We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes. | ||
* | Renaming local_binder into local_binder_expr. | 2017-03-24 | |
| | | | | This is a bit long, but it is to keep a symmetry with constr_expr. | ||
* | Merge branch 'v8.6' | 2017-03-22 | |
|\ | |||
| * | don't require printing-only notation to be productive | 2017-02-16 | |
| | | |||
* | | Merge branch 'v8.6' | 2016-11-30 | |
|\| | |||
| * | Fix some documentation typos. | 2016-11-24 | |
| | | |||
* | | Merge branch 'v8.6' | 2016-11-18 | |
|\| | |||
| * | Lets Hints/Instances take an optional pattern | 2016-11-03 | |
| | | | | | | | | | | | | | | | | | | In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well. | ||
| * | Fix bug #5098: Symmetry broken in HoTT. | 2016-10-08 | |
| | | | | | | | | | | | | | | We defactorize the in_clause grammar entry to allow parsing of the "symmetry" tactic when it has no arguments. Beforehand, the clause_dft_concl entry accepted the empty stream, preventing the definition of symmetry as a mere identifier. | ||
* | | Merge branch 'v8.6' | 2016-10-02 | |
|\| | |||
| * | Fix bug #4869, allow Prop, Set, and level names in constraints. | 2016-09-29 | |
| | | |||
* | | Moving Ltac-specific parsing API to ltac/ folder. | 2016-09-14 | |
|/ | |||
* | Remove lexing of ordinal notations. | 2016-07-03 | |
| | | | | | This was implemented in anticipation of a part of PR#164 that we decided not to merge. | ||
* | Exporting a generic argument induction_arg. As a consequence, | 2016-06-18 | |
| | | | | | simplifying and generalizing the grammar entries for injection, discriminate and simplify_eq. | ||
* | The grammar_extend function now registers unsynchronized extensions. | 2016-05-11 | |
| | | | | | | 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. | ||
* | Making the grammar command extend API purely functional. | 2016-05-11 | |
| | | | | | 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. | ||
* | Moving the constr empty entry registering to the state-based API. | 2016-05-11 | |
| | |||
* | Turning the grammar extend command API into a state-passing one. | 2016-05-11 | |
| | |||
* | Moving the grammar summary to Pcoq. | 2016-05-11 | |
| | |||
* | Delimiting the use of unsafe code in Pcoq. | 2016-05-10 | |
| | |||
* | Type-safe constr notations. | 2016-05-10 | |
| | | | | | | | 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. | ||
* | Purer implementation of empty level registering in Pcoq. | 2016-05-10 | |
| | |||
* | Removing the Entry module now that rules need not be marshalled. | 2016-05-10 | |
| | |||
* | Hardening the obsolete unsafe_grammar_statement API. | 2016-05-10 | |
| | |||
* | Removing dead code in Compat. | 2016-05-10 | |
| | |||
* | Remove dead registering code in Pcoq. | 2016-04-24 | |
| | |||
* | Moving the Tactic Notation entry parser from Pcoq to Tacentries. | 2016-03-31 | |
| | |||
* | Moving the Ltac definition command to an EXTEND based command. | 2016-03-20 | |
| | |||
* | Moving the proof mode parsing management to Pcoq. | 2016-03-19 | |
| | |||
* | Do not export entry_key from Pcoq anymore. | 2016-03-19 | |
| | |||
* | Simplifying the code of Entry. | 2016-03-19 | |
| | |||
* | Removing dead code in Pcoq. | 2016-03-18 | |
| | |||
* | ARGUMENT EXTEND made of only one entry share the same grammar. | 2016-03-18 | |
| | | | | This fixes parsing conflicts with the [fix ... with] tactic. | ||
* | Removing the special status of generic arguments defined by Coq itself. | 2016-03-17 | |
| | | | | | | | | This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They now have to be reachable in the ML code. Note that this has some consequences, as the previous macro was potentially mixing grammar entries and arguments as long as their name was the same. Now, each genarg comes with its grammar instead, so there is no way to abuse the macro. | ||
* | Adding a universe argument to Pcoq.create_generic_entry. | 2016-03-17 | |
| | |||
* | Relying on parsing rules rather than genarg to check if an argument is empty. | 2016-03-17 | |
| | |||
* | Removing a source of type-unsafeness in Pcoq. | 2016-02-02 | |
| | |||
* | Merge branch 'v8.5' | 2016-01-29 | |
|\ | |||
| * | Implement support for universe binder lists in Instance and Program ↵ | 2016-01-23 | |
| | | | | | | | | Fixpoint/Definition. | ||
* | | Merge branch 'v8.5' | 2016-01-21 | |
|\| | |||
| * | Update copyright headers. | 2016-01-20 | |
| | | |||
* | | Removing dynamic entries from Pcoq. | 2016-01-17 | |
| | | |||
* | | ML extensions use untyped representation of user entries. | 2016-01-17 | |
| | | |||
* | | Removing the special status of open_constr generic argument. | 2015-12-28 | |
| | | | | | | | | | | We also intepret it at toplevel as a true constr and push the resulting evarmap in the current state. | ||
* | | CLEANUP: Vernacexpr.VernacDeclareTacticDefinition | 2015-12-18 | |
| | | | | | | | | | | | | | | | | | | | | The definition of Vernacexpr.VernacDeclareTacticDefinition was changed. The original definition allowed us to represent non-sensical value such as: VernacDeclareTacticDefinition(Qualid ..., false, ...) The new definition prevents that. | ||
* | | Adding a token "index" representing positions (1st, 2nd, etc.). | 2015-12-15 | |
| | | |||
* | | Fixing the return type of the Atoken symbol. | 2015-10-28 | |
| | | |||
* | | Removing unused code in Pcoq. | 2015-10-27 | |
| | | |||
* | | Finer type for Pcoq.interp_entry_name. | 2015-10-27 | |
| | |