aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.mli
Commit message (Collapse)AuthorAge
* Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
| | | | | simplifying and generalizing the grammar entries for injection, discriminate and simplify_eq.
* The grammar_extend function now registers unsynchronized extensions.Gravatar Pierre-Marie Pédrot2016-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.Gravatar Pierre-Marie Pédrot2016-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.Gravatar Pierre-Marie Pédrot2016-05-11
|
* Turning the grammar extend command API into a state-passing one.Gravatar Pierre-Marie Pédrot2016-05-11
|
* Moving the grammar summary to Pcoq.Gravatar Pierre-Marie Pédrot2016-05-11
|
* Delimiting the use of unsafe code in Pcoq.Gravatar Pierre-Marie Pédrot2016-05-10
|
* Type-safe constr notations.Gravatar Pierre-Marie Pédrot2016-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.Gravatar Pierre-Marie Pédrot2016-05-10
|
* Removing the Entry module now that rules need not be marshalled.Gravatar Pierre-Marie Pédrot2016-05-10
|
* Hardening the obsolete unsafe_grammar_statement API.Gravatar Pierre-Marie Pédrot2016-05-10
|
* Removing dead code in Compat.Gravatar Pierre-Marie Pédrot2016-05-10
|
* Remove dead registering code in Pcoq.Gravatar Pierre-Marie Pédrot2016-04-24
|
* Moving the Tactic Notation entry parser from Pcoq to Tacentries.Gravatar Pierre-Marie Pédrot2016-03-31
|
* Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
|
* Moving the proof mode parsing management to Pcoq.Gravatar Pierre-Marie Pédrot2016-03-19
|
* Do not export entry_key from Pcoq anymore.Gravatar Pierre-Marie Pédrot2016-03-19
|
* Simplifying the code of Entry.Gravatar Pierre-Marie Pédrot2016-03-19
|
* Removing dead code in Pcoq.Gravatar Pierre-Marie Pédrot2016-03-18
|
* ARGUMENT EXTEND made of only one entry share the same grammar.Gravatar Pierre-Marie Pédrot2016-03-18
| | | | This fixes parsing conflicts with the [fix ... with] tactic.
* Removing the special status of generic arguments defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-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.Gravatar Pierre-Marie Pédrot2016-03-17
|
* Relying on parsing rules rather than genarg to check if an argument is empty.Gravatar Pierre-Marie Pédrot2016-03-17
|
* Removing a source of type-unsafeness in Pcoq.Gravatar Pierre-Marie Pédrot2016-02-02
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\
| * Implement support for universe binder lists in Instance and Program ↵Gravatar Matthieu Sozeau2016-01-23
| | | | | | | | Fixpoint/Definition.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Removing dynamic entries from Pcoq.Gravatar Pierre-Marie Pédrot2016-01-17
| |
* | ML extensions use untyped representation of user entries.Gravatar Pierre-Marie Pédrot2016-01-17
| |
* | Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
| | | | | | | | | | We also intepret it at toplevel as a true constr and push the resulting evarmap in the current state.
* | CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionGravatar Matej Kosik2015-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.).Gravatar Hugo Herbelin2015-12-15
| |
* | Fixing the return type of the Atoken symbol.Gravatar Pierre-Marie Pédrot2015-10-28
| |
* | Removing unused code in Pcoq.Gravatar Pierre-Marie Pédrot2015-10-27
| |
* | Finer type for Pcoq.interp_entry_name.Gravatar Pierre-Marie Pédrot2015-10-27
| |
* | Indexing existentially quantified entries returned by interp_entry_name.Gravatar Pierre-Marie Pédrot2015-10-27
| |
* | Type-safe grammar extensions.Gravatar Pierre-Marie Pédrot2015-10-27
| |
* | Pcoq entries are given a proper module.Gravatar Pierre-Marie Pédrot2015-10-26
| | | | | | | | | | | | | | | | | | | | | | Entries defined in the Pcoq AST of symbols must be marshallable, because they are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as they contain functional values. This is why the Pcoq module used a pair [string * string] to describe entries. It is obviously type-unsafe, so we define a new abstract type in its own module. There is a little issue though, which is that our entries and CAMLP4/5 entries must be kept synchronized through an association table. The Pcoq module tries to maintain this invariant.
* | Getting rid of the Atactic entry.Gravatar Pierre-Marie Pédrot2015-10-25
| |
* | Getting rid of the Agram entry.Gravatar Pierre-Marie Pédrot2015-10-25
| |
* | Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.Gravatar Pierre-Marie Pédrot2015-10-21
| |
* | Expliciting some uses of Compat module.Gravatar Pierre-Marie Pédrot2015-10-21
|/
* grammar: export constr_evalGravatar Enrico Tassi2015-03-30
|
* grammar: export hypidentGravatar Enrico Tassi2015-03-30
| | | | This is necessary to make ssr compile with both camlp4/5
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)Gravatar Hugo Herbelin2014-11-06
| | | | | by hopefully computing the right position where to reinit an empty level. Also removing obsolete comment.
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
| | | | "pat/term" for "apply term on current_hyp as pat".
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
| | | | | Also taking advantage of the change to rename it into TacML. Ultimately should allow ML tactic to return values.
* Properly declare uconstr as an argument for TACTIC EXTEND.Gravatar Arnaud Spiwack2014-08-05
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 21:23:52 +0000