aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Collapse)Author
2016-05-11The 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-11Making 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-11Moving the constr empty entry registering to the state-based API.Pierre-Marie Pédrot
2016-05-11Turning the grammar extend command API into a state-passing one.Pierre-Marie Pédrot
2016-05-11Moving the grammar summary to Pcoq.Pierre-Marie Pédrot
2016-05-10Delimiting the use of unsafe code in Pcoq.Pierre-Marie Pédrot
2016-05-10Overlooked 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-10Further tidying of the constr extension code.Pierre-Marie Pédrot
2016-05-10Type-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-10AlistNsep token now accepts an arbitrary separator.Pierre-Marie Pédrot
2016-05-10Simpler data structure for Arules token.Pierre-Marie Pédrot
2016-05-10Purer implementation of empty level registering in Pcoq.Pierre-Marie Pédrot
2016-05-10Removing the Entry module now that rules need not be marshalled.Pierre-Marie Pédrot
2016-05-10Hardening the obsolete unsafe_grammar_statement API.Pierre-Marie Pédrot
2016-05-10Removing dead code in Compat.Pierre-Marie Pédrot
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-09Rename Lexer -> CLexer.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Removing useless generic arguments.Pierre-Marie Pédrot
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
2016-04-27Revert "Fixing a mispelling coma -> comma."Hugo Herbelin
This reverts commit 857dc0aaae30805725da213b6550dc1ff3a7adb2.
2016-04-27Fixing a mispelling coma -> comma.Hugo Herbelin
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
2016-04-25Removing dead code in Compat.Pierre-Marie Pédrot
2016-04-24Remove dead registering code in Pcoq.Pierre-Marie Pédrot
2016-04-24Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-12A fix to #4666 (Exc_located capsule added by camlp5 overwritingHugo 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-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Matthieu Sozeau
into JasonGross-trunk-function_scope
2016-04-01Getting 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-31Moving the code handling tactic notations to Tacentries.Pierre-Marie Pédrot
2016-03-31Abstracting 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-31Moving the Tactic Notation entry parser from Pcoq to Tacentries.Pierre-Marie Pédrot
2016-03-20Adding a new Ltac generic argument for forced tactics returing unit.Pierre-Marie Pédrot
2016-03-20Moving the Ltac definition command to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Print Ltac to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Tactic Notation to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Tacinterp to Hightactics.Pierre-Marie Pédrot
2016-03-19Fixing compilation with old versions of CAMLP5.Pierre-Marie Pédrot
2016-03-19Further reducing the dependencies of the EXTEND macros.Pierre-Marie Pédrot
2016-03-19Moving VernacSolve to an EXTEND-based definition.Pierre-Marie Pédrot
2016-03-19Moving the parsing of the Ltac proof mode to G_ltac.Pierre-Marie Pédrot
2016-03-19Moving the proof mode parsing management to Pcoq.Pierre-Marie Pédrot
2016-03-19Allowing generalized rules in typed symbols.Pierre-Marie Pédrot
2016-03-19Do not export entry_key from Pcoq anymore.Pierre-Marie Pédrot
2016-03-19Simplifying the code of Entry.Pierre-Marie Pédrot
2016-03-18Removing dead code in Pcoq.Pierre-Marie Pédrot
2016-03-18Making the EXTEND macros almost self-contained.Pierre-Marie Pédrot
2016-03-18ARGUMENT EXTEND made of only one entry share the same grammar.Pierre-Marie Pédrot
This fixes parsing conflicts with the [fix ... with] tactic.
2016-03-17Removing the special status of generic arguments defined by Coq itself.Pierre-Marie Pédrot
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.
2016-03-17Code factorization in Pcoq.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 06:18:06 +0000