| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-10-27 | Rename misc nonterminals | Jim Fehrle | |
| 2020-10-27 | Rename tactic_expr -> ltac_expr | Jim Fehrle | |
| 2020-03-18 | Update headers in the whole code base. | Théo Zimmermann | |
| Add headers to a few files which were missing them. | |||
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann | |
| 2018-09-10 | [dune] Add apidoc target using `odoc` | Emilio Jesus Gallego Arias | |
| We build the `@doc` target in the `dune` job: - The documentation can be found in `_build/default/_doc/` - We had to fix a couple of quoting problems. | |||
| 2018-03-08 | Make most of TACTIC EXTEND macros runtime calls. | Maxime Dénès | |
| 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. | |||
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann | |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2016-06-09 | Adding a bit of documentation in the mli. | Pierre-Marie Pédrot | |
| 2016-05-04 | Moving the Val module to Geninterp. | Pierre-Marie Pédrot | |
| 2016-05-04 | Switching to an untyped toplevel representation for Ltac values. | Pierre-Marie Pédrot | |
| 2016-04-08 | Fixing printing of toplevel values. | Pierre-Marie Pédrot | |
| 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. | |||
| 2016-03-30 | Ensuring that the type of base generic arguments contain triples. | Pierre-Marie Pédrot | |
| 2016-03-19 | Removing dead code in Genarg. | Pierre-Marie Pédrot | |
| 2016-03-19 | Removing the untyped representation of genargs. | Pierre-Marie Pédrot | |
| 2016-03-17 | Removing the registering of default values for generic arguments. | Pierre-Marie Pédrot | |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-20 | Update copyright headers. | Maxime Dénès | |
| 2016-01-17 | Moving val_cast to Tacinterp. | Pierre-Marie Pédrot | |
| 2016-01-17 | Getting rid of the awkward unpack mechanism from Genarg. | Pierre-Marie Pédrot | |
| 2016-01-17 | Simplification and type-safety of Pcoq thanks to GADTs in Genarg. | Pierre-Marie Pédrot | |
| 2016-01-17 | Exporting Genarg implementation in the API. | Pierre-Marie Pédrot | |
| We can now use the expressivity of GADT to work around historical kludges of generic arguments. | |||
| 2016-01-17 | Temporary commit getting rid of Obj.magic unsafety for Genarg. | Pierre-Marie Pédrot | |
| This will allow an easier landing of the rewriting of Genarg. | |||
| 2016-01-14 | Removing constr generic argument. | Pierre-Marie Pédrot | |
| 2016-01-14 | Removing ident and var generic arguments. | Pierre-Marie Pédrot | |
| 2015-12-28 | Removing the special status of open_constr generic argument. | Pierre-Marie Pédrot | |
| We also intepret it at toplevel as a true constr and push the resulting evarmap in the current state. | |||
| 2015-12-21 | Finer-grained types for toplevel values. | Pierre-Marie Pédrot | |
| 2015-12-21 | Removing ad-hoc interpretation rules for tactic notations and their genarg. | Pierre-Marie Pédrot | |
| 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. | |||
| 2015-12-21 | Removing the now useless genarg generic argument. | Pierre-Marie Pédrot | |
| 2015-12-21 | Using dynamic values in tactic evaluation. | Pierre-Marie Pédrot | |
| 2015-12-21 | Attaching a dynamic argument to the toplevel type of generic arguments. | Pierre-Marie Pédrot | |
| 2015-12-17 | Getting rid of some hardwired generic arguments. | Pierre-Marie Pédrot | |
| 2015-12-12 | Removing dead unsafe code in Genarg. | Pierre-Marie Pédrot | |
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2014-08-29 | Type-safe version of genarg list / pair / opt functions. | Pierre-Marie Pédrot | |
| 2014-08-29 | Simplification of Genarg unpackers. | Pierre-Marie Pédrot | |
| Instead of having a version of unpackers for each level, we use a dummy argument to force unification of types. | |||
| 2014-02-27 | Remove unsafe code (Obj.magic) in Tacinterp. | Arnaud Spiwack | |
| This commit also introduces a module Monad to generate monadic combinators (currently, only List.map). | |||
| 2014-01-19 | Adding a default object to generic argument registering mechanism. | Pierre-Marie Pédrot | |
| 2013-12-19 | Removing the useless pattern ident genarg. | Pierre-Marie Pédrot | |
| 2013-12-01 | Removing RefArgType generic argument. | Pierre-Marie Pédrot | |
| 2013-11-30 | Getting rid of casted_open_constr. It was only used by the | Pierre-Marie Pédrot | |
| 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. | |||
| 2013-08-04 | Small cleaning of printing coercion failures in Ltac interpretation. | ppedrot | |
| 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 | |||
| 2013-07-05 | Removing SortArgType. | ppedrot | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16618 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2013-07-05 | Expurgating the useless difference between List0 and List1 at the | ppedrot | |
| 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 | |||
| 2013-06-30 | Using functors to reduce the boilerplate used in registering | ppedrot | |
| 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 | |||
| 2013-06-27 | Getting rid of IntroPatternArgType. | ppedrot | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16610 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2013-06-21 | Splitted up Genarg in four different levels: | ppedrot | |
| 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 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |