aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
Commit message (Collapse)AuthorAge
...
* | Adding a universe argument to Pcoq.create_generic_entry.Gravatar Pierre-Marie Pédrot2016-03-17
| |
* | Removing the registering of default values for generic arguments.Gravatar Pierre-Marie Pédrot2016-03-17
| |
* | Removing dead code in Q_util.Gravatar Pierre-Marie Pédrot2016-03-17
| |
* | Reducing the number of modules linked in grammar.cma.Gravatar Pierre-Marie Pédrot2016-03-17
| |
* | Expurging grammar.mllib from uselessly linked modules.Gravatar Pierre-Marie Pédrot2016-03-06
| |
* | Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.Gravatar Pierre-Marie Pédrot2016-03-06
| | | | | | | | | | | | | | | | We just reuse the same one weird old trick in CAMLP4 to compare keywords and identifiers as tokens. Note though that the commit 982460743 does not fix the keyword vs. identifier issue in CAMLP4, so that the corresponding test fails. This means that since that commit, some code compiling with CAMLP5 does not when using CAMLP4, making it a second-class citizen.
| * Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)".Gravatar Pierre-Marie Pédrot2016-03-05
| | | | | | | | | | | | | | The ARGUMENT EXTEND statement was wrongly using a CompatLoc instead of a Loc, and this was not detected by typing "thanks" to the Gram.action magic. When using CAMLP4, this was wreaking havoc at runtime, but not when using CAMLP5, as the locations where sharing the same representation.
* | All arguments defined through ARGUMENT EXTEND declare a tactic scope.Gravatar Pierre-Marie Pédrot2016-03-04
| | | | | | | | | | Amongs other things, it kind of fixes bug #4492, even though you cannot really take advantage of the parsed data for now.
* | Removing the METAIDENT token, as it is not used anymore.Gravatar Pierre-Marie Pédrot2016-02-24
| | | | | | | | | | | | METAIDENT were idents of the form $foobar, only used in quotations. Note that it removes two dollars in the Coq codebase! Guess I'm absolved for the $(...) syntax.
* | Removing the Q_coqast module.Gravatar Pierre-Marie Pédrot2016-02-24
| | | | | | | | | | | | It implemented the quotation logic of terms and tactics, although it was mostly obsolete. With quotations gone, it is now useless and thus removed. I fundamentally doubt that anyone hardly depends on this out there.
* | Infering atomic ML entries from their grammar.Gravatar Pierre-Marie Pédrot2016-02-01
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | ML extensions use untyped representation of user entries.Gravatar Pierre-Marie Pédrot2016-01-17
| |
* | Tactic notation printing accesses all the token data.Gravatar Pierre-Marie Pédrot2016-01-16
| |
* | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
| |
* | Removing ident and var generic arguments.Gravatar Pierre-Marie Pédrot2016-01-14
| |
* | Monotonizing Ftactic.Gravatar Pierre-Marie Pédrot2016-01-08
| |
* | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-06
|\| | | | | | | | | Conflicts: lib/cSig.mli
| * Fix order of files in mllib.Gravatar Maxime Dénès2016-01-05
| | | | | | | | | | | | | | | | CString was linked after Serialize, although the later was using CString.equal. This had not been noticed so far because OCaml was ignoring functions marked as external in interfaces (which is the case of CString.equal) when considering link dependencies. This was changed on the OCaml side as part of the fix of PR#6956, so linking was now failing in several places.
* | Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
| | | | | | | | Actually the identifier was never used and just carried along.
* | Proper datatype for EXTEND syntax tokens.Gravatar Pierre-Marie Pédrot2016-01-02
| |
* | Implementing non-focussed generic arguments.Gravatar Pierre-Marie Pédrot2015-12-28
| | | | | | | | | | | | | | Kind of enhances the situation of bug #4409. Now arguments can be interpreted globally or focussedly in a dynamic fashion because the interpretation function returns a Ftactic.t. The bug is not fixed yet because we should tweak the interpretation of tactic arguments.
* | 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.
* | Fixing non exhaustive pattern-matching in 003fe3d5e60b.Gravatar Hugo Herbelin2015-12-25
| |
* | Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
| |
* | ARGUMENT EXTEND shares the toplevel representation when possible.Gravatar Pierre-Marie Pédrot2015-12-21
| |
* | Removing ad-hoc interpretation rules for tactic notations and their genarg.Gravatar Pierre-Marie Pédrot2015-12-21
| | | | | | | | | | | | Now that types can share the same dynamic representation, we do not have to transtype the topelvel values dynamically and just take advantage of the standard interpretation function.
* | Removing the now useless genarg generic argument.Gravatar Pierre-Marie Pédrot2015-12-21
| |
* | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
| |
* | Getting rid of some hardwired generic arguments.Gravatar Pierre-Marie Pédrot2015-12-17
| |
* | Factorizing unsafe code by relying on the new Dyn module.Gravatar Pierre-Marie Pédrot2015-12-05
| |
* | Type-safe Argextend.Gravatar Pierre-Marie Pédrot2015-10-28
| |
* | Type-safe Egramml.grammar_prod_item.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
| |
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-07-02
|\|
| * Code documentation of the TACTIC/VERNAC EXTEND macros.Gravatar Pierre-Marie Pédrot2015-06-29
| |
| * Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25
| | | | | | | | This allows fatal_error to be used for printing anomalies at loading time.
* | Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-23
| | | | | | | | This allows fatal_error to be used for printing anomalies at loading time.
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
|\| | | | | | | | | | | | | Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
| * A more user-friendly naming of variables of ltac names defined byGravatar Hugo Herbelin2015-05-08
| | | | | | | | TACTIC EXTEND (based on user-given name).
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-23
|\|
| * Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Gravatar Pierre-Marie Pédrot2015-02-19
| |
| * Record type for VERNAC EXTEND rules and a bit of documentation.Gravatar Pierre-Marie Pédrot2015-02-19
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 07:54:11 +0000