aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
Commit message (Expand)AuthorAge
* About printing of traces of failures while calling ltac code.Gravatar Hugo Herbelin2016-06-06
* Adding the Print Ltac Signature command.Gravatar Pierre-Marie Pédrot2016-06-05
* Removing "rename" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "exact" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "double induction" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Add a synonymous Set Debug Ltac for Set Ltac Debug, for uniformity.Gravatar Hugo Herbelin2016-06-02
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Put the "move" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-17
* Put the "change" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "specialize_eq" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "generalize dependent" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "*_cast_no_check" tactics in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "exact" family of tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Generate more user-readable tactic notation kernel names.Gravatar Pierre-Marie Pédrot2016-05-16
* Making the grammar command extend API purely functional.Gravatar Pierre-Marie Pédrot2016-05-11
* Moving the constr empty entry registering to the state-based API.Gravatar Pierre-Marie Pédrot2016-05-11
* Turning the grammar extend command API into a state-passing one.Gravatar Pierre-Marie Pédrot2016-05-11
* Moving the grammar summary to Pcoq.Gravatar Pierre-Marie Pédrot2016-05-11
* AlistNsep token now accepts an arbitrary separator.Gravatar Pierre-Marie Pédrot2016-05-10
* Removing the Entry module now that rules need not be marshalled.Gravatar Pierre-Marie Pédrot2016-05-10
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
* Pass user symbol to tactic notation printers.Gravatar Pierre-Marie Pédrot2016-05-08
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Normalizing the names of dynamic types to follow a typ_* scheme.Gravatar Pierre-Marie Pédrot2016-05-04
* Removing useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
* Interpretation function can return any untyped value.Gravatar Pierre-Marie Pédrot2016-05-04
* Removing external uses of Val.inject and making Geninterp.interp return Val.tGravatar Pierre-Marie Pédrot2016-05-04
* Removing the Value.of_* API for parameterized types.Gravatar Pierre-Marie Pédrot2016-05-04
* Do not generate generic arguments for data which only requires toplevel values.Gravatar Pierre-Marie Pédrot2016-05-04
* More toplevel value representation sharing.Gravatar Pierre-Marie Pédrot2016-05-04
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* Simplifying the code of Tacinterp.Gravatar Pierre-Marie Pédrot2016-05-04
* Getting rid of the Geninterp.generic_interp function.Gravatar Pierre-Marie Pédrot2016-05-04
* Switching to an untyped toplevel representation for Ltac values.Gravatar Pierre-Marie Pédrot2016-05-04
* Generate parsing rules for ML tactics in the same order as before a7917a32.Gravatar Pierre-Marie Pédrot2016-05-02
* Useless code in Tacentries.Gravatar Pierre-Marie Pédrot2016-05-02
* Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
* Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing printers for pr_auto_using and pr_firstorder_using."Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing Add Parametric Relation by adding printer for binders."Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing printing of Register retroknowledge."Gravatar Hugo Herbelin2016-04-27
* Revert "A fix to #3709: ensuring extra parentheses when a tactic entry has a"Gravatar Hugo Herbelin2016-04-27
* Revert "Passing around the precedence to the generic printer so as to solve"Gravatar Hugo Herbelin2016-04-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 15:21:31 +0000