| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-03-20 | Relying on generic arguments to represent Extern hints. | Pierre-Marie Pédrot | |
| 2016-03-20 | Adding a new Ltac generic argument for forced tactics returing unit. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tacenv to Hightactics. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tactic_debug to Hightactic. | Pierre-Marie Pédrot | |
| 2016-03-20 | Making Evarutil independent from Reductionops. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Refine to its proper module. | Pierre-Marie Pédrot | |
| 2016-03-20 | Making Proofview independent of Logic. | Pierre-Marie Pédrot | |
| 2016-03-20 | Fixing the classification of Tactic Notation. | Pierre-Marie Pédrot | |
| 2016-03-20 | Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4. | Pierre-Marie Pédrot | |
| The interpretation of arguments of tactic notations were normalizing the goal beforehand, which incurred an important time penalty. We now do this argumentwise which allows to save time in frequent cases, notably tactic arguments. | |||
| 2016-03-20 | Moving Tacintern to Hightactics. | 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 the tactic related code from Metasyntax to a new file. | 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 | Moving the use of Tactic_option from Obligations to G_obligations. | Pierre-Marie Pédrot | |
| 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 | Removing the special status of generic entries defined by Coq itself. | Pierre-Marie Pédrot | |
| The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there. | |||
| 2016-03-17 | Adding a universe argument to Pcoq.create_generic_entry. | Pierre-Marie Pédrot | |
| 2016-03-17 | Removing the registering of default values for generic arguments. | Pierre-Marie Pédrot | |
| 2016-03-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-03-09 | Redo fix init_setoid -> init_relation_classes | Matthieu Sozeau | |
| It got lost during a merge with the 8.5 branch. | |||
| 2016-03-09 | Fix strategy of Keyed Unification | Matthieu Sozeau | |
| Try first to find a keyed subterm without conversion/betaiota on open terms (that is the usual strategy of rewrite), if this fails, try with full conversion, incuding betaiota. This makes the test-suite pass again, retaining efficiency in the most common cases. | |||
| 2016-03-06 | Moving Autorewrite to Hightatctic. | Pierre-Marie Pédrot | |
| 2016-03-06 | Putting Tactic_debug just below Tacinterp. | Pierre-Marie Pédrot | |
| 2016-03-06 | Removing dependency of Himsg in tactic files. | Pierre-Marie Pédrot | |
| 2016-03-06 | Moving Tactic_debug to tactics/ folder. | Pierre-Marie Pédrot | |
| 2016-03-06 | Moving Ltac traces to Tacexpr and Tacinterp. | Pierre-Marie Pédrot | |
| 2016-03-06 | Removing useless grammar.cma dependencies. | Pierre-Marie Pédrot | |
| 2016-03-06 | Moving Eauto to a simple ML file. | Pierre-Marie Pédrot | |
| 2016-03-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-03-05 | Exporting build_selector, a component of discriminate, for use in congruence. | Hugo Herbelin | |
| 2016-03-04 | Adding some standard arguments in tactic scopes. | Pierre-Marie Pédrot | |
| This is not perfect and repeats what we do in Pcoq, but it is hard to factorize because rules defined in Pcoq do not have the same precedence. For instance, constr as a Tactic Notation argument is a Pcoq.Constr.constr while as a quotation argument is a Pcoq.Constr.lconstr. We should think of a fix in the long run, but for now it is reasonable to duplicate code. | |||
| 2016-03-04 | Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations]. | Pierre-Marie Pédrot | |
| 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-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-28 | Fixing bug #4596: [rewrite] broke in the past few weeks. | Pierre-Marie Pédrot | |
| Checking that a term was indeed a relation was made too early, as the decomposition function recognized relations of the form "f (g .. (h x y)) with f, g unary and only h binary. We postpone this check to the very end. | |||
| 2016-02-27 | Removing Tacmach.New qualification in Tacinterp. | Pierre-Marie Pédrot | |
| 2016-02-27 | Removing some compatibility layers in Tacinterp. | Pierre-Marie Pédrot | |
| 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-24 | Getting rid of the "<:tactic< ... >>" quotations. | Pierre-Marie Pédrot | |
| It used to allow to represent parts of tactic AST directly in ML code. Most of the uses were trivial, only calling a constant, except for tauto that had an important code base written in this style. Removing this reduces the dependency to CAMLPX and the preeminence of Ltac in ML code. | |||
| 2016-02-23 | Moving tauto.ml4 to a proper ML file. | Pierre-Marie Pédrot | |
| 2016-02-23 | Fix bug #4544: Backtrack on using full betaiota reduction during keyed ↵ | Matthieu Sozeau | |
| unification. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |