| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-04-19 | Revert "Fixing printing of surrounding parentheses in "ltac:"." | Hugo Herbelin | |
| I made a confusion between ltac: in constr and ltac: in tactics, the one needing parentheses in v8.5 but the latter needing parentheses only in trunk. This reverts commit f5dc54519f2a62bab2f7b9059e8c3c8dc53619be. | |||
| 2016-04-17 | Fixing printing of surrounding parentheses in "ltac:". | Hugo Herbelin | |
| 2016-04-12 | Fixing printing of "destruct in" after ce71ac17268f. | Hugo Herbelin | |
| 2016-04-11 | Removing the ad-hoc tactic_expr type. | Pierre-Marie Pédrot | |
| This type was actually only used by the debug printer of tactics, and only for atomic tactics. Furthermore, that type was asymmetric, as the underlying tacexpr type was set to be glob_tactic, when the semantics would have required a Val.t type. Furthermore, this type is absent from every contrib I have seen, which hints again in favour of its lack of meaning. | |||
| 2016-04-10 | Extruding the print_atom primitive. | Pierre-Marie Pédrot | |
| 2016-04-09 | Removing extra spaces in printing arguments of VERNAC EXTEND. | Hugo Herbelin | |
| 2016-04-09 | Removing automatic printing of leading space in auto_using and | Hugo Herbelin | |
| hintbases so that it does not put extra space when auto is defined as a TACTIC EXTEND. | |||
| 2016-04-09 | In pr_clauses, do not print a leading space by default so that it can | Hugo Herbelin | |
| be used in the generic printer for tactics. Allows e.g. to print "symmetry in H" correctly after its move to TACTIC EXTEND. | |||
| 2016-04-08 | Fixing printing of toplevel values. | Pierre-Marie Pédrot | |
| This is not perfect yet, in particular the whole precedence system is a real mess, as there is a real need for tidying up the Pptactic implementation. Nonetheless, printing toplevel values is only used for debugging purposes, where an ugly display is better than none at all. | |||
| 2016-04-08 | Fixing printing of Tactic Notations with tactic arguments. | Pierre-Marie Pédrot | |
| 2016-03-20 | Adding a new Ltac generic argument for forced tactics returing unit. | Pierre-Marie Pédrot | |
| 2016-03-19 | Removing the untyped representation of genargs. | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |