aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.ml
Commit message (Expand)AuthorAge
* 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
* Revert "Chasing the goal entering backward while interpreting tactics. This r...Gravatar Pierre-Marie Pédrot2014-05-24
* Chasing the goal entering backward while interpreting tactics. This requiredGravatar Pierre-Marie Pédrot2014-05-24
* Moving the "specialize" tactic out of the AST. Also removed an obsoleteGravatar Pierre-Marie Pédrot2014-05-22
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-09 11:46:41 +0000