| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-03-04 | Uniformizing the parsing of argument scopes in Ltac. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "move" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "exists" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "symmetry" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "generalize dependent" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "clearbody" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "clear" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "cofix" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 2016-02-29 | Moving the "fix" tactic to TACTIC EXTEND. | Pierre-Marie Pédrot | |
| 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 MetaIdArg entry of tactic expressions. | Pierre-Marie Pédrot | |
| This was historically used together with the <:tactic< ... >> quotation to insert foreign code as $foo, but it actually only survived in the implementation of Tauto. With the removal of the quotation feature, this is now totally obsolete. | |||
| 2016-02-02 | Removing a source of type-unsafeness in Pcoq. | Pierre-Marie Pédrot | |
| 2016-01-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-23 | Implement support for universe binder lists in Instance and Program ↵ | Matthieu Sozeau | |
| Fixpoint/Definition. | |||
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-21 | Stronger invariants on the use of the introduction pattern (pat1,...,patn). | Hugo Herbelin | |
| The length of the pattern should now be exactly the number of assumptions and definitions introduced by the destruction or induction, including the induction hypotheses in case of an induction. Like for pattern-matching, the local definitions in the argument of the constructor can be skipped in which case a name is automatically created for these. | |||
| 2016-01-20 | Update copyright headers. | Maxime Dénès | |
| 2016-01-17 | Simplification and type-safety of Pcoq thanks to GADTs in Genarg. | Pierre-Marie Pédrot | |
| 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-17 | Removing dynamic entries from Pcoq. | Pierre-Marie Pédrot | |
| 2016-01-17 | ML extensions use untyped representation of user entries. | Pierre-Marie Pédrot | |
| 2016-01-16 | Separating the parsing of user-defined entries from their intepretation. | Pierre-Marie Pédrot | |
| 2016-01-16 | Less type-unsafety in Pcoq. | Pierre-Marie Pédrot | |
| 2016-01-15 | Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. | Maxime Dénès | |
| 2016-01-14 | Removing constr generic argument. | Pierre-Marie Pédrot | |
| 2016-01-14 | Continuing 003fe3d5e on parsing positions. | Hugo Herbelin | |
| - Being stricter on the ordinal suffix accepted (only st for 1, 21, etc, nd for 2, 22, etc., etc.) - Reporting when the suffix is not the expected one (rather than considering that, e.g. 2st, is two tokens, a number then an identifier). | |||
| 2016-01-11 | CLEANUP: removing unused field | Matej Kosik | |
| I have removed the second field of the "Constrexpr.CRecord" variant because once it was set to "None" it never changed to anything else. It was just carried and copied around. | |||
| 2016-01-02 | Remove some useless type declarations. | Guillaume Melquiond | |
| 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 | Separation of concern in TacAlias API. | Pierre-Marie Pédrot | |
| The TacAlias node now only contains the arguments fed to the tactic notation. The binding variables are worn by the tactic representation in Tacenv. | |||
| 2015-12-30 | External tactics and notations now accept any tactic argument. | Pierre-Marie Pédrot | |
| This commit has deep consequences in term of tactic evaluation, as it allows to pass any tac_arg to ML and alias tactics rather than mere generic arguments. This makes the evaluation much more uniform, and in particular it removes the special evaluation function for notations. This last point may break some notations out there unluckily. I had to treat in an ad-hoc way the tactic(...) entry of tactic notations because it is actually not interpreted as a generic argument but rather as a proper tactic expression instead. There is for now no syntax to pass any tactic argument to a given ML or notation tactic, but this should come soon. Also fixes bug #3849 en passant. | |||
| 2015-12-28 | Removing unused parsing entries. | 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-25 | Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.ml | Hugo Herbelin | |
| to g_tactic.ml4 so as to leave room for "IntroPattern []" to mean "no introduction". | |||
| 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-23 | Partial backtrack on commit 20641795624. | Pierre-Marie Pédrot | |
| The parsing rules were broken and disallowed tactic replacement of the form Ltac ident ::= expr. | |||
| 2015-12-18 | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified | Matej Kosik | |
| 2015-12-18 | CLEANUP: Vernacexpr.VernacDeclareTacticDefinition | Matej Kosik | |
| The definition of Vernacexpr.VernacDeclareTacticDefinition was changed. The original definition allowed us to represent non-sensical value such as: VernacDeclareTacticDefinition(Qualid ..., false, ...) The new definition prevents that. | |||
| 2015-12-18 | ALPHA-CONVERSION: in "parsing/g_vernac.ml4" file | Matej Kosik | |
| 2015-12-18 | CLEANUP: Vernacexpr.vernac_expr | Matej Kosik | |
| Originally, "VernacTime" and "VernacRedirect" were defined like this: type vernac_expr = ... | VernacTime of vernac_list | VernacRedirect of string * vernac_list ... where type vernac_list = located_vernac_expr list Currently, that list always contained one and only one element. So I propose changing the definition of these two variants in the following way: | VernacTime of located_vernac_expr | VernacRedirect of string * located_vernac_expr which covers all our current needs and enforces the invariant related to the number of commands that are part of the "VernacTime" and "VernacRedirect" variants. | |||
| 2015-12-15 | Adding a token "index" representing positions (1st, 2nd, etc.). | Hugo Herbelin | |
| 2015-12-15 | Tactics: Generalizing the use of the experimental clearing modifier to | Hugo Herbelin | |
| all cases of rewrite. | |||
| 2015-12-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-10 | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn. | Hugo Herbelin | |
| Marking it as experimental. | |||
| 2015-12-08 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-05 | Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction) | Hugo Herbelin | |
| based on a suggestion of Guillaume M. (done like this in ssreflect). This is actually consistent with the hack of using "destruct (1)" to mean the term 1 by opposition to the use of "destruct 1" to mean the first non-dependent hypothesis of the goal. | |||
| 2015-12-03 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-02 | Improving syntax of pat/constr introduction pattern so that | Hugo Herbelin | |
| pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat. Open to other suggestions of syntax though. | |||
| 2015-12-02 | Dead code from August 2014 in apply in. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |