| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-03-06 | Moving Tactic_debug to tactics/ folder. | 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-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-22 | The tactic generic argument now returns a value rather than a glob_expr. | Pierre-Marie Pédrot | |
| The glob_expr was actually always embedded as a VFun, so this patch should not change anything semantically. The only change occurs in the plugin API where one should use the Tacinterp.tactic_of_value function instead of Tacinterp.eval_tactic. Moreover, this patch allows to use tactics returning arguments from the ML side. | |||
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-20 | Update copyright headers. | Maxime Dénès | |
| 2016-01-17 | Getting rid of the awkward unpack mechanism from 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-16 | Tactic notation printing accesses all the token data. | Pierre-Marie Pédrot | |
| 2016-01-14 | Removing constr generic argument. | Pierre-Marie Pédrot | |
| 2016-01-14 | Removing ident and var generic arguments. | Pierre-Marie Pédrot | |
| 2016-01-02 | Remove some unused functions. | Guillaume Melquiond | |
| Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. | |||
| 2016-01-02 | Remove useless rec flags. | Guillaume Melquiond | |
| 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 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-27 | Tentative API fix for tactic arguments to be fed to tclWITHHOLES. | Pierre-Marie Pédrot | |
| The previous implementation was a source of evar leaks if misused, as it created values coming together with their current evar_map. This is dead wrong if the value is not used on the spot. To fix this, we rather return a ['a delayed_open] object. Two argument types were modified: bindings and constr_bindings. The open_constr argument should also be fixed, but it is more entangled and thus I leave it for another commit. | |||
| 2015-12-24 | Removing auto from the tactic AST. | Pierre-Marie Pédrot | |
| 2015-12-21 | Removing ad-hoc interpretation rules for tactic notations and their genarg. | Pierre-Marie Pédrot | |
| Now that types can share the same dynamic representation, we do not have to transtype the topelvel values dynamically and just take advantage of the standard interpretation function. | |||
| 2015-12-21 | Changing the toplevel type of the int_or_var generic type to int. | Pierre-Marie Pédrot | |
| 2015-12-21 | Removing the now useless genarg generic argument. | Pierre-Marie Pédrot | |
| 2015-12-18 | Tying the loop in tactic printing API. | Pierre-Marie Pédrot | |
| 2015-12-17 | Getting rid of some hardwired generic arguments. | Pierre-Marie Pédrot | |
| 2015-12-04 | Getting rid of the dynamic node of the tactic AST. | Pierre-Marie Pédrot | |
| 2015-12-03 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-02 | Dead code from August 2014 in apply in. | Hugo Herbelin | |
| 2015-10-19 | Type delayed_open_constr is now monotonic. | Pierre-Marie Pédrot | |
| 2015-06-25 | Remove other types not carried by interpretations in `Tacexpr`. | Arnaud Spiwack | |
| 2015-06-25 | Remove useless `and_short_name` in interpreted level in `Tacexpr`. | Arnaud Spiwack | |
| 2015-05-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-04-23 | Remove almost all the uses of string concatenation when building error messages. | Guillaume Melquiond | |
| Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure. | |||
| 2015-01-23 | Splitting ML tactics in one function per grammar entry. | Pierre-Marie Pédrot | |
| Furthermore, ML tactic dispatch is not done according to the type of its argument anymore. | |||
| 2015-01-21 | Embedding the index of the ML tactic entry in the Tacexpr AST. | Pierre-Marie Pédrot | |
| This will allow to get rid of the fragile mechanism of discriminating which entry to call depending on the dynamic type of its arguments. | |||
| 2015-01-18 | Univs: proper printing of global and local universe names (only | Matthieu Sozeau | |
| printing functions touched in the kernel). | |||
| 2015-01-17 | Univs: proper printing of global and local universe names (only | Matthieu Sozeau | |
| printing functions touched in the kernel). | |||
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2014-12-23 | A global [gfail] tactic which works like [fail] except that it fails even if ↵ | Arnaud Spiwack | |
| there is no focused goal. The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not. | |||
| 2014-12-23 | Fix compilation error in some configurations. | Arnaud Spiwack | |
| This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select". Fixes #3877. | |||
| 2014-12-19 | Add a backtracking version of Ltac's [match]. | Arnaud Spiwack | |
| [multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well. | |||
| 2014-12-12 | Add Ltac syntax for the [tclIFCATCH] primitive. | Arnaud Spiwack | |
| [tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught. | |||
| 2014-12-12 | Extend the syntax of simpl with a delta flag. | Arnaud Spiwack | |
| You can write 'simpl -[plus minus] div2'. Simpl does not use it for now. | |||
| 2014-11-19 | Print [uconstr] in genargs. | Arnaud Spiwack | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |