| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-03-20 | Adding a new Ltac generic argument for forced tactics returing unit. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving the Ltac definition command to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Print Ltac to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tactic Notation to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tacinterp to Hightactics. | Pierre-Marie Pédrot | |
| 2016-03-19 | Fixing compilation with old versions of CAMLP5. | Pierre-Marie Pédrot | |
| 2016-03-19 | Further reducing the dependencies of the EXTEND macros. | Pierre-Marie Pédrot | |
| 2016-03-19 | Moving VernacSolve to an EXTEND-based definition. | Pierre-Marie Pédrot | |
| 2016-03-19 | Moving the parsing of the Ltac proof mode to G_ltac. | Pierre-Marie Pédrot | |
| 2016-03-19 | Moving the proof mode parsing management to Pcoq. | Pierre-Marie Pédrot | |
| 2016-03-19 | Allowing generalized rules in typed symbols. | Pierre-Marie Pédrot | |
| 2016-03-19 | Do not export entry_key from Pcoq anymore. | Pierre-Marie Pédrot | |
| 2016-03-19 | Simplifying the code of Entry. | Pierre-Marie Pédrot | |
| 2016-03-18 | Removing dead code in Pcoq. | Pierre-Marie Pédrot | |
| 2016-03-18 | Making the EXTEND macros almost self-contained. | Pierre-Marie Pédrot | |
| 2016-03-18 | ARGUMENT EXTEND made of only one entry share the same grammar. | Pierre-Marie Pédrot | |
| This fixes parsing conflicts with the [fix ... with] tactic. | |||
| 2016-03-17 | Removing the special status of generic arguments defined by Coq itself. | Pierre-Marie Pédrot | |
| This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They now have to be reachable in the ML code. Note that this has some consequences, as the previous macro was potentially mixing grammar entries and arguments as long as their name was the same. Now, each genarg comes with its grammar instead, so there is no way to abuse the macro. | |||
| 2016-03-17 | Code factorization in Pcoq. | Pierre-Marie Pédrot | |
| 2016-03-17 | Adding a universe argument to Pcoq.create_generic_entry. | Pierre-Marie Pédrot | |
| 2016-03-17 | Relying on parsing rules rather than genarg to check if an argument is empty. | Pierre-Marie Pédrot | |
| 2016-03-13 | Adopting the same rules for interpreting @, abbreviations and | Hugo Herbelin | |
| notations in patterns than in terms, wrt implicit arguments and scopes. See file Notations2.v for the conventions in use in terms. Somehow this could be put in 8.5 since it puts in agreement the interpretation of abbreviations and notations in "symmetric patterns" to what is done in terms (even though the interpretation rules for terms are a bit ad hoc). There is one exception: in terms, "(foo args) args'" deactivates the implicit arguments and scopes in args'. This is a bit complicated to implement in patterns so the syntax is not supported (and anyway, this convention is a bit questionable). | |||
| 2016-03-13 | Supporting "(@foo) args" in patterns, where "@foo" has no arguments. | Hugo Herbelin | |
| 2016-03-06 | Moving Autorewrite to Hightatctic. | Pierre-Marie Pédrot | |
| 2016-03-06 | Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move. | Pierre-Marie Pédrot | |
| 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. | |||
| 2016-03-04 | Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations]. | Pierre-Marie Pédrot | |
| 2016-03-04 | Exchanging roles of tactic_arg and tactic_top_or_arg entries. | Pierre-Marie Pédrot | |
| The tactic_arg entry was essentially a hack to keep parsing constrs as tactic arguments. We rather use tactic_top_or_arg as the true entry for tactic arguments now. | |||
| 2016-03-04 | Removing the UConstr entry of the tactic_arg AST. | Pierre-Marie Pédrot | |
| This was redundant with the wit_uconstr generic argument, so there was no real point on keeping it there. | |||
| 2016-03-04 | Making parentheses mandatory in tactic scopes. | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |