aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.ml
Commit message (Expand)AuthorAge
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Slight simplification of naming of tactics in equality.ml (hopefully).Gravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* Moving the TacAlias node out of atomic tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Better printing of Ltac values.Gravatar Pierre-Marie Pédrot2014-08-16
* Removing unused Refiner.tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
* Better structure for Ltac pretyping environments.Gravatar Pierre-Marie Pédrot2014-08-07
* Removing simple induction / destruct from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Instead of relying on a trick to make the constructor tactic parse, putGravatar Pierre-Marie Pédrot2014-08-07
* Removing the "constructor" tactic from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Revert the change in Constrintern introduced by "Add a type of untyped term t...Gravatar Arnaud Spiwack2014-08-06
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
* Removing "intros untils" from the AST.Gravatar Pierre-Marie Pédrot2014-08-06
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
* Ltac's [idtac] is now interpreted outside of a goal if possible.Gravatar Arnaud Spiwack2014-08-05
* Ltac's idtac is now implemented using the new API.Gravatar Arnaud Spiwack2014-08-05
* Tacinterp: [interp_message] and associate now only require an environment rat...Gravatar Arnaud Spiwack2014-08-05
* Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].Gravatar Arnaud Spiwack2014-08-05
* Fix interpretation bug in [uconstr].Gravatar Arnaud Spiwack2014-08-05
* Cleaning of the new implementation of the tactic monad.Gravatar Arnaud Spiwack2014-08-04
* Better struture for Ltac internalization environments in Constrintern.Gravatar Pierre-Marie Pédrot2014-08-02
* New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Gravatar Arnaud Spiwack2014-08-01
* Add [numgoal] to Ltac.Gravatar Arnaud Spiwack2014-08-01
* Untyped terms in tactic: function [type_term c] to give a typed version of [c].Gravatar Arnaud Spiwack2014-07-29
* Add a type of untyped term to Ltac's value.Gravatar Arnaud Spiwack2014-07-29
* Clean up obsolete comment.Gravatar Arnaud Spiwack2014-07-29
* CPS-style tactic matching. We use the tactic monad as the target of the CPS.Gravatar Pierre-Marie Pédrot2014-07-28
* A slightly more fine grained way to check whether a TACTIC EXTEND is global o...Gravatar Arnaud Spiwack2014-07-25
* Distinguish tactics t1;t2 and t1;[t2..].Gravatar Arnaud Spiwack2014-07-24
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* Fix a oversight in 5bf9e67b .Gravatar Arnaud Spiwack2014-07-10
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
* time tacGravatar Hugo Herbelin2014-07-07
* More efficient implementation of Ltac match, by inlining a stream map.Gravatar Pierre-Marie Pédrot2014-07-03
* Fixing the place where to insert a space in "Tactic failure"Gravatar Hugo Herbelin2014-07-01
* Useless keeping of dirpath in tactic aliases.Gravatar Pierre-Marie Pédrot2014-06-30
* Fix semantics of change p with c to typecheck c at each specific occurrence o...Gravatar Matthieu Sozeau2014-06-23
* Less goal-entering.Gravatar Pierre-Marie Pédrot2014-06-22
* Adding a raw_goals primitive for Tacinterp.Gravatar Pierre-Marie Pédrot2014-06-19
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
* Fixes the lost evars when interpreting a change with pattern tactic.Gravatar Arnaud Spiwack2014-06-06
* Moving the [split] tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-06-06
* The tactic interpreter now uses a new type of tactics, throughGravatar Pierre-Marie Pédrot2014-06-03
* Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Gravatar Hugo Herbelin2014-05-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 02:19:17 +0000