| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-02-24 | Removing the METAIDENT token, as it is not used anymore. | Pierre-Marie Pédrot | |
| 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. | |||
| 2016-02-24 | Removing the Q_coqast module. | Pierre-Marie Pédrot | |
| 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. | |||
| 2016-02-01 | Infering atomic ML entries from their grammar. | 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 | ML extensions use untyped representation of user entries. | Pierre-Marie Pédrot | |
| 2016-01-16 | Tactic notation printing accesses all the token data. | Pierre-Marie Pédrot | |
| 2016-01-14 | Removing constr generic argument. | Pierre-Marie Pédrot | |
| 2016-01-14 | Removing ident and var generic arguments. | Pierre-Marie Pédrot | |
| 2016-01-08 | Monotonizing Ftactic. | Pierre-Marie Pédrot | |
| 2016-01-06 | Merge remote-tracking branch 'origin/v8.5' into trunk | Guillaume Melquiond | |
| Conflicts: lib/cSig.mli | |||
| 2016-01-05 | Fix order of files in mllib. | Maxime Dénès | |
| 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. | |||
| 2016-01-02 | Simplification of grammar_prod_item type. | Pierre-Marie Pédrot | |
| Actually the identifier was never used and just carried along. | |||
| 2016-01-02 | Proper datatype for EXTEND syntax tokens. | Pierre-Marie Pédrot | |
| 2015-12-28 | Implementing non-focussed generic arguments. | Pierre-Marie Pédrot | |
| 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. | |||
| 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-25 | Fixing non exhaustive pattern-matching in 003fe3d5e60b. | Hugo Herbelin | |
| 2015-12-24 | Removing auto from the tactic AST. | Pierre-Marie Pédrot | |
| 2015-12-21 | ARGUMENT EXTEND shares the toplevel representation when possible. | 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-17 | Getting rid of some hardwired generic arguments. | Pierre-Marie Pédrot | |
| 2015-12-05 | Factorizing unsafe code by relying on the new Dyn module. | Pierre-Marie Pédrot | |
| 2015-10-28 | Type-safe Argextend. | Pierre-Marie Pédrot | |
| 2015-10-27 | Type-safe Egramml.grammar_prod_item. | Pierre-Marie Pédrot | |
| 2015-10-27 | Finer type for Pcoq.interp_entry_name. | Pierre-Marie Pédrot | |
| 2015-10-27 | Indexing existentially quantified entries returned by interp_entry_name. | Pierre-Marie Pédrot | |
| 2015-10-27 | Type-safe grammar extensions. | Pierre-Marie Pédrot | |
| 2015-10-26 | Pcoq entries are given a proper module. | Pierre-Marie Pédrot | |
| 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. | |||
| 2015-10-25 | Getting rid of the Atactic entry. | Pierre-Marie Pédrot | |
| 2015-10-25 | Getting rid of the Agram entry. | Pierre-Marie Pédrot | |
| 2015-10-21 | Pcoq.prod_entry_key now uses a GADT to statically enforce typedness. | Pierre-Marie Pédrot | |
| 2015-07-02 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-06-29 | Code documentation of the TACTIC/VERNAC EXTEND macros. | Pierre-Marie Pédrot | |
| 2015-06-25 | Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly. | Thomas Sibut-Pinote | |
| This allows fatal_error to be used for printing anomalies at loading time. | |||
| 2015-06-23 | Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly. | Thomas Sibut-Pinote | |
| This allows fatal_error to be used for printing anomalies at loading time. | |||
| 2015-05-15 | Merge v8.5 into trunk | Hugo Herbelin | |
| Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API) | |||
| 2015-05-08 | A more user-friendly naming of variables of ltac names defined by | Hugo Herbelin | |
| TACTIC EXTEND (based on user-given name). | |||
| 2015-02-23 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-19 | Adding a possible DEPRECATED flag to VERNAC EXTEND statements. | Pierre-Marie Pédrot | |
| 2015-02-19 | Record type for VERNAC EXTEND rules and a bit of documentation. | Pierre-Marie Pédrot | |
| 2015-01-27 | Tentative fix for bug #3957. | Pierre-Marie Pédrot | |
| Now that ML tactics are not dispatched according to the type of their arguments anymore, one has to take care of the way potentially atomic tactics are handled. This patch ensures that the atomic tactics generated by the TACTIC EXTEND macro have the right length and the right order. There may be very rare trouble if two ML tactics in the same entry are of the form "foo" x1 ... xn "foo" y1 ... ym where all xi and yi may be empty. I doubt that the legacy implementation behaved well in this case anyway. | |||
| 2015-01-23 | Splitting ML tactics in one function per grammar entry. | Pierre-Marie Pédrot | |
| Furthermore, ML tactic dispatch is not done according to the type of its argument anymore. | |||
| 2015-01-21 | Embedding the index of the ML tactic entry in the Tacexpr AST. | Pierre-Marie Pédrot | |
| This will allow to get rid of the fragile mechanism of discriminating which entry to call depending on the dynamic type of its arguments. | |||
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2014-12-23 | A global [gfail] tactic which works like [fail] except that it fails even if ↵ | Arnaud Spiwack | |
| there is no focused goal. The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not. | |||
| 2014-12-23 | Fix compilation error in some configurations. | Arnaud Spiwack | |
| This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select". Fixes #3877. | |||
| 2014-12-19 | Add a backtracking version of Ltac's [match]. | Arnaud Spiwack | |
| [multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well. | |||
| 2014-12-16 | Fixing CAMLP4 compilation. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |