| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-04-27 | In the short term, stronger invariant on the syntax of TacAssert, what | Hugo Herbelin | |
| allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause. | |||
| 2016-04-15 | Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh | Pierre Courtieu | |
| 2016-04-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-04-07 | Allow to unset the refinement mode of Instance in ML | Matthieu Sozeau | |
| Falling back to the global setting if not given. Useful to make Add Morphism fail correctly when the given proof terms are incomplete. Adapt test-suite file #2848 accordingly. | |||
| 2016-04-07 | Fixing an incorrect use of prod_appvect on a term which was not a | Hugo Herbelin | |
| product in setoid_rewrite. Backport of d670c6b6ce from trunk. | |||
| 2016-04-03 | Fixing the "No applicable tactic" non informative error message | Hugo Herbelin | |
| regression on apply. | |||
| 2016-03-25 | Moving Autorewrite back to tactics/. | Pierre-Marie Pédrot | |
| 2016-03-25 | Moving Eqdecide to tactics/. | Pierre-Marie Pédrot | |
| 2016-03-25 | Moving Eauto and Class_tactics to tactics/. | Pierre-Marie Pédrot | |
| 2016-03-21 | Creating a dedicated ltac/ folder for Hightactics. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tacsubst to hightactics. | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |