aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.ml
Commit message (Expand)AuthorAge
* Removing decompose record / sum from the tactic AST.Gravatar Pierre-Marie Pédrot2014-05-21
* Moving left & right tactics out of the AST.Gravatar Pierre-Marie Pédrot2014-05-21
* Moving (e)transitivity out of the AST.Gravatar Pierre-Marie Pédrot2014-05-20
* Tactics declared through TACTIC EXTEND that are of the formGravatar Pierre-Marie Pédrot2014-05-20
* Tentative to add constr-using primitive tactics without grammar rules.Gravatar Pierre-Marie Pédrot2014-05-20
* Moving argument-free tactics out of the AST into a dedicatedGravatar Pierre-Marie Pédrot2014-05-16
* Refresh universes for Ltac's type_of, as the term can be used anywhere,Gravatar Matthieu Sozeau2014-05-09
* Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."Gravatar Hugo Herbelin2014-05-08
* Avoid "revert" to retype-check the goal, and move it to a "new" tactic.Gravatar Hugo Herbelin2014-05-08
* Isolating a function "make_abstraction", new name of "letin_abstract",Gravatar Hugo Herbelin2014-05-08
* Code cleaning in Tacinterp: factorizing some uses of tclEVARS.Gravatar Pierre-Marie Pédrot2014-05-08
* - Fix eq_constr_universes restricted to Sorts.equalGravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Rewriting [lapply] tactic in the new monad.Gravatar Pierre-Marie Pédrot2014-04-27
* Removing useless try-with clauses in Goal.enter variants.Gravatar Pierre-Marie Pédrot2014-04-25
* Fixing various backtrace recordings.Gravatar Pierre-Marie Pédrot2014-04-25
* Writing tclABSTRACT in the new monad. In particular the unsafe status is nowGravatar Pierre-Marie Pédrot2014-04-24
* Fixing bug #3285.Gravatar Pierre-Marie Pédrot2014-04-20
* Closing bug #3260Gravatar Julien Forest2014-04-14
* Using non-normalized goals in tactic interpretation.Gravatar Pierre-Marie Pédrot2014-03-19
* Adding phantom types to discriminate normalized goals, and adding a way toGravatar Pierre-Marie Pédrot2014-03-19
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* Removing a fishy use of pervasive equality in Ltac backtrace printing.Gravatar Pierre-Marie Pédrot2014-03-01
* Tacinterp: more refactoring.Gravatar Arnaud Spiwack2014-02-27
* Tacinterp: refactoring using Monad.Gravatar Arnaud Spiwack2014-02-27
* Remove unsafe code (Obj.magic) in Tacinterp.Gravatar Arnaud Spiwack2014-02-27
* Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Gravatar Arnaud Spiwack2014-02-27
* Tacinterp: yet another superfluous enterl.Gravatar Arnaud Spiwack2014-02-27
* Tacinterp: spurious enterl.Gravatar Arnaud Spiwack2014-02-27
* Dead code: eval_ltac_constr.Gravatar Arnaud Spiwack2014-02-27
* Tacinterp: remove the is_value check in Ltac's let-in.Gravatar Arnaud Spiwack2014-02-25
* Tacinterp: fewer enterl still.Gravatar Arnaud Spiwack2014-02-25
* Tacinterp: fewer Proofview.Goal.enterl.Gravatar Arnaud Spiwack2014-02-25
* Tacinterp: clean up.Gravatar Arnaud Spiwack2014-02-25
* Tacinterp: remove unnecessary return/bind pairs.Gravatar Arnaud Spiwack2014-02-25
* A view type for IStream.Gravatar Arnaud Spiwack2014-02-24
* In Ltac's exact tactic: avoid checking the type of the term twice.Gravatar Arnaud Spiwack2014-01-31
* Algebraized "No such hypothesis" errorsGravatar Pierre-Marie Pédrot2014-01-06
* Notations now accept the $(...)$ tactic-in-term syntax. They are resolved atGravatar Pierre-Marie Pédrot2013-12-22
* Removing the useless pattern ident genarg.Gravatar Pierre-Marie Pédrot2013-12-19
* Using interp_genarg in tactic notations where possible, instead of an ad-hocGravatar Pierre-Marie Pédrot2013-12-19
* Bad use of Obj.magic in interpretation of TacAlias arguments.Gravatar Pierre Boutillier2013-12-19
* Printing function for Stdargs in debuggerGravatar Pierre Boutillier2013-12-19
* Removing the need of evarmaps in constr internalization.Gravatar Pierre-Marie Pédrot2013-12-17
* Fixing backtrace registering of various tactic-related try-with blocks.Gravatar Pierre-Marie Pédrot2013-12-11
* Stylistic change.Gravatar Arnaud Spiwack2013-12-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 06:42:33 +0000