aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2014-06-21Reindex section variables for typeclass resolution if their type changed.Matthieu Sozeau
2014-06-20Allow more relaxed conversion between the types of the two terms of a rewriteMatthieu Sozeau
2014-06-20Add an e_type_of to avoid losing universe constraints.Matthieu Sozeau
2014-06-19Adding a raw_goals primitive for Tacinterp.Pierre-Marie Pédrot
2014-06-19- Fix bug in unification, not only named metas are turned into evars (e.g. in...Matthieu Sozeau
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu Sozeau
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-17Improve hotspot in Auto.Pierre-Marie Pédrot
2014-06-13Check resolution of Metas turned into Evars by pose_all_metas_as_evarsHugo Herbelin
2014-06-12Passing some tactics to the new monad type.Pierre-Marie Pédrot
2014-06-11Fix bug #3291, stack overflow in rewrite.Matthieu Sozeau
2014-06-11Fix bug #3289Matthieu Sozeau
2014-06-11In generalized rewrite, avoid retyping completely and constantly the conclusi...Matthieu Sozeau
2014-06-11fix handling of side effects in abstract (fixes QArithSternBrocot)Enrico Tassi
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-06-08Enforce a correct exception handling in declaration_hooksEnrico Tassi
2014-06-07Adding a new Control file centralizing the control options of Coq.Pierre-Marie Pédrot
2014-06-06Preserve compatibility on examples such as "intros []." on goals suchHugo Herbelin
2014-06-06Fixes the lost evars when interpreting a change with pattern tactic.Arnaud Spiwack
2014-06-06Moving the [split] tactic out of the AST.Pierre-Marie Pédrot
2014-06-04Collecting in Namegen those conventional default names that are used in diffe...Hugo Herbelin
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-06-03The tactic interpreter now uses a new type of tactics, throughPierre-Marie Pédrot
2014-06-02Removing symmetry from the atomic tactics.Pierre-Marie Pédrot
2014-05-31More on injection over a projectable "existT". - Fixing syntax "injection ......Hugo Herbelin
2014-05-31Fixing introduction patterns * and ** when used in a branch so that they do n...Hugo Herbelin
2014-05-31Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Hugo Herbelin
2014-05-27Removing a tclSENSITIVE from rewrite.Pierre-Marie Pédrot
2014-05-26- Fix in kernel conversion not folding the universe constraintsMatthieu Sozeau
2014-05-24Revert "Chasing the goal entering backward while interpreting tactics. This r...Pierre-Marie Pédrot
2014-05-24Chasing the goal entering backward while interpreting tactics. This requiredPierre-Marie Pédrot
2014-05-22Moving the "specialize" tactic out of the AST. Also removed an obsoletePierre-Marie Pédrot
2014-05-22Removing useless use of metaids in tactic AST.Pierre-Marie Pédrot
2014-05-21Removing decompose record / sum from the tactic AST.Pierre-Marie Pédrot
2014-05-21Allowing Ltac definitions that may be unusable because of a built-inPierre-Marie Pédrot
2014-05-21Moving left & right tactics out of the AST.Pierre-Marie Pédrot
2014-05-20Moving (e)transitivity out of the AST.Pierre-Marie Pédrot
2014-05-20Tactics declared through TACTIC EXTEND that are of the formPierre-Marie Pédrot
2014-05-20Tentative to add constr-using primitive tactics without grammar rules.Pierre-Marie Pédrot
2014-05-18When discrimination is not possible, try to project.Maxime Dénès
2014-05-18Suggest Set Injection On Proofs in error message for injection.Maxime Dénès
2014-05-18Restored old behavior of injection on proofs by default.Maxime Dénès
2014-05-16Moving argument-free tactics out of the AST into a dedicatedPierre-Marie Pédrot
2014-05-15poly: remove unused attribute to STM nodes and vernac classificaitonEnrico Tassi
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
2014-05-09Code cleaning & factorizing functions in Equality.Pierre-Marie Pédrot
2014-05-09Update and start testing rewrite-in-type code.Matthieu Sozeau
2014-05-09Refresh universes for Ltac's type_of, as the term can be used anywhere,Matthieu Sozeau
2014-05-08Encapsulating some clausenv uses. This simplifies the control flow of somePierre-Marie Pédrot
2014-05-08Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-15 00:08:20 +0000