Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Put the "exact" family of tactic in the monad. | 2016-05-16 | |
| | |||
* | Put the "fix" tactic in the monad. | 2016-05-16 | |
| | |||
* | Put the "exact_constr" tactic in the monad. | 2016-05-16 | |
| | |||
* | Put the "clear" tactic into the monad. | 2016-05-16 | |
| | |||
* | Removing dead code and unused opens. | 2016-05-08 | |
| | |||
* | Normalizing the names of dynamic types to follow a typ_* scheme. | 2016-05-04 | |
| | |||
* | Removing external uses of Val.inject and making Geninterp.interp return Val.t | 2016-05-04 | |
| | |||
* | Removing the Value.of_* API for parameterized types. | 2016-05-04 | |
| | | | | | Although still working, it is now bad practice to use it, and it is not widely spread anyway. | ||
* | Moving the Val module to Geninterp. | 2016-05-04 | |
| | |||
* | Getting rid of the Geninterp.generic_interp function. | 2016-05-04 | |
| | |||
* | Switching to an untyped toplevel representation for Ltac values. | 2016-05-04 | |
| | |||
* | Moving Ftactic and Geninterp to the engine folder. | 2016-05-04 | |
| | |||
* | Merge branch 'v8.5' | 2016-05-04 | |
|\ | |||
| * | In Regular Subst Tactic mode, ensure that the order of hypotheses is | 2016-05-03 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | preserved, which is a source of incompatibilities w.r.t. released 8.5 but which looks to me to be the only possible canonical behavior. This is I believe a better behavior than the Regular Subst Tactic behavior in the released 8.5 and 8.5pl1. There, the order of hypotheses in which substitutions happened was respected, but their interleaving with other hypotheses was not respected. So, I consider this to be a fix to the "Regular Subst Tactic" mode. Also added a more detailed "specification" of the "Regular" behavior of "subst" in the reference manual. | ||
| * | Fix bug #4707: clearbody much slower in 8.5pl1. | 2016-05-03 | |
| | | | | | | | | | | We only retype hypotheses and conclusion when they do depend on the cleared identifier. This saves a lot of time. | ||
* | | Revert "In the short term, stronger invariant on the syntax of TacAssert, what" | 2016-04-27 | |
| | | | | | | | | This reverts commit bde36d4b00185065628324d8ca71994f84eae244. | ||
* | | In the short term, stronger invariant on the syntax of TacAssert, what | 2016-04-27 | |
| | | | | | | | | | | | | allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause. | ||
* | | Merge branch 'v8.5' | 2016-04-09 | |
|\| | |||
| * | Allow to unset the refinement mode of Instance in ML | 2016-04-07 | |
| | | | | | | | | | | | | 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. | ||
| * | Fixing an incorrect use of prod_appvect on a term which was not a | 2016-04-07 | |
| | | | | | | | | | | | | product in setoid_rewrite. Backport of d670c6b6ce from trunk. | ||
| * | Fixing the "No applicable tactic" non informative error message | 2016-04-03 | |
| | | | | | | | | regression on apply. | ||
* | | Moving Autorewrite back to tactics/. | 2016-03-25 | |
| | | |||
* | | Moving Eqdecide to tactics/. | 2016-03-25 | |
| | | |||
* | | Moving Eauto and Class_tactics to tactics/. | 2016-03-25 | |
| | | |||
* | | Creating a dedicated ltac/ folder for Hightactics. | 2016-03-21 | |
| | | |||
* | | Moving Tacsubst to hightactics. | 2016-03-20 | |
| | | |||
* | | Relying on generic arguments to represent Extern hints. | 2016-03-20 | |
| | | |||
* | | Adding a new Ltac generic argument for forced tactics returing unit. | 2016-03-20 | |
| | | |||
* | | Moving Tacenv to Hightactics. | 2016-03-20 | |
| | | |||
* | | Moving Tactic_debug to Hightactic. | 2016-03-20 | |
| | | |||
* | | Making Evarutil independent from Reductionops. | 2016-03-20 | |
| | | |||
* | | Moving Refine to its proper module. | 2016-03-20 | |
| | | |||
* | | Making Proofview independent of Logic. | 2016-03-20 | |
| | | |||
* | | Fixing the classification of Tactic Notation. | 2016-03-20 | |
| | | |||
| * | Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4. | 2016-03-20 | |
| | | | | | | | | | | | | 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. | ||
* | | Moving Tacintern to Hightactics. | 2016-03-20 | |
| | | |||
* | | Moving the Ltac definition command to an EXTEND based command. | 2016-03-20 | |
| | | |||
* | | Moving the tactic related code from Metasyntax to a new file. | 2016-03-20 | |
| | | |||
* | | Moving Print Ltac to an EXTEND based command. | 2016-03-20 | |
| | | |||
* | | Moving Tactic Notation to an EXTEND based command. | 2016-03-20 | |
| | | |||
* | | Moving Tacinterp to Hightactics. | 2016-03-20 | |
| | | |||
* | | Moving the use of Tactic_option from Obligations to G_obligations. | 2016-03-19 | |
| | | |||
* | | Removing the special status of generic arguments defined by Coq itself. | 2016-03-17 | |
| | | | | | | | | | | | | | | | | 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. | ||
* | | Removing the special status of generic entries defined by Coq itself. | 2016-03-17 | |
| | | | | | | | | | | | | | | | | | | | | | | 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. | ||
* | | Adding a universe argument to Pcoq.create_generic_entry. | 2016-03-17 | |
| | | |||
* | | Removing the registering of default values for generic arguments. | 2016-03-17 | |
| | | |||
* | | Merge branch 'v8.5' | 2016-03-09 | |
|\| | |||
* | | Redo fix init_setoid -> init_relation_classes | 2016-03-09 | |
| | | | | | | | | It got lost during a merge with the 8.5 branch. | ||
| * | Fix strategy of Keyed Unification | 2016-03-09 | |
| | | | | | | | | | | | | | | 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. | ||
* | | Moving Autorewrite to Hightatctic. | 2016-03-06 | |
| | |