aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/genarg.mli
Commit message (Collapse)AuthorAge
* Make most of TACTIC EXTEND macros runtime calls.Gravatar Maxime Dénès2018-03-08
| | | | | | | | | Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic and its parsing rule. Instead, we make it generate a typed AST that is passed to the parser and a generic tactic execution routine. PMP has written a small parser that can generate the same typed ASTs without relying on camlp5, which is overkill for such simple macros.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
|
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Switching to an untyped toplevel representation for Ltac values.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Fixing printing of toplevel values.Gravatar Pierre-Marie Pédrot2016-04-08
| | | | | | | This is not perfect yet, in particular the whole precedence system is a real mess, as there is a real need for tidying up the Pptactic implementation. Nonetheless, printing toplevel values is only used for debugging purposes, where an ugly display is better than none at all.
* Ensuring that the type of base generic arguments contain triples.Gravatar Pierre-Marie Pédrot2016-03-30
|
* Removing dead code in Genarg.Gravatar Pierre-Marie Pédrot2016-03-19
|
* Removing the untyped representation of genargs.Gravatar Pierre-Marie Pédrot2016-03-19
|
* Removing the registering of default values for generic arguments.Gravatar Pierre-Marie Pédrot2016-03-17
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Moving val_cast to Tacinterp.Gravatar Pierre-Marie Pédrot2016-01-17
| |
* | Getting rid of the awkward unpack mechanism from Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
| |
* | Simplification and type-safety of Pcoq thanks to GADTs in Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
| |
* | Exporting Genarg implementation in the API.Gravatar Pierre-Marie Pédrot2016-01-17
| | | | | | | | | | We can now use the expressivity of GADT to work around historical kludges of generic arguments.
* | Temporary commit getting rid of Obj.magic unsafety for Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
| | | | | | | | This will allow an easier landing of the rewriting of Genarg.
* | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
| |
* | Removing ident and var generic arguments.Gravatar Pierre-Marie Pédrot2016-01-14
| |
* | 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.
* | Finer-grained types for toplevel values.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
| |
* | Attaching a dynamic argument to the toplevel type of generic arguments.Gravatar Pierre-Marie Pédrot2015-12-21
| |
* | Getting rid of some hardwired generic arguments.Gravatar Pierre-Marie Pédrot2015-12-17
| |
* | Removing dead unsafe code in Genarg.Gravatar Pierre-Marie Pédrot2015-12-12
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Type-safe version of genarg list / pair / opt functions.Gravatar Pierre-Marie Pédrot2014-08-29
|
* Simplification of Genarg unpackers.Gravatar Pierre-Marie Pédrot2014-08-29
| | | | | Instead of having a version of unpackers for each level, we use a dummy argument to force unification of types.
* Remove unsafe code (Obj.magic) in Tacinterp.Gravatar Arnaud Spiwack2014-02-27
| | | This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
* Adding a default object to generic argument registering mechanism.Gravatar Pierre-Marie Pédrot2014-01-19
|
* Removing the useless pattern ident genarg.Gravatar Pierre-Marie Pédrot2013-12-19
|
* Removing RefArgType generic argument.Gravatar Pierre-Marie Pédrot2013-12-01
|
* Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
| | | | | | | | | | | | | | | | | refine tactic, which now uses plain glob_constr's. Now there is no real need to depend on goal when interpreting genargs. Possible minor incompatibilities: 1. The interpretation of glob_constr to constr is now done by Goal.constr_of_raw, which may be slightly dumbier than the dedicated Tacinterp.interp_open_constr which tries harder. Stdlib and test-suite do go through, though. 2. I had to change the parsing level of wit_glob in Extraargs from lconstr to constr. It may break ML notations using glob, but as they are only used inside Coq code and all well-parenthezised, it should be OK.
* Small cleaning of printing coercion failures in Ltac interpretation.Gravatar ppedrot2013-08-04
| | | | | | Now we at least print the type of the offending object. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16657 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing SortArgType.Gravatar ppedrot2013-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16618 85f007b7-540e-0410-9357-904b9bb8a0f7
* Expurgating the useless difference between List0 and List1 at theGravatar ppedrot2013-07-05
| | | | | | | | | | level of generic arguments. This only matters at parsing time. TODO: the current status is not satisfactory enough, as rule emptyness is still decided w.r.t. generic arguments. This should be done on a grammar entry basis instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16617 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using functors to reduce the boilerplate used in registeringGravatar ppedrot2013-06-30
| | | | | | generic argument stuff, including the unsafe Obj.magic-like casts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of IntroPatternArgType.Gravatar ppedrot2013-06-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16610 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-22 06:32:08 +0000