aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2014-06-27Add an init_setoid check in rewrite to avoid trying to get undefined references.Matthieu Sozeau
2014-06-26Properly refresh the local hintdb database in case an external tactic changedMatthieu Sozeau
2014-06-25Incorrect folding of evars in let_tac_gen made remember fail to storeMatthieu Sozeau
2014-06-25In rewrite, wrong computation of the sort of the term to be rewritten inMatthieu Sozeau
2014-06-25In exact check, use e_type_of to ensure that universe constraints necessaryMatthieu Sozeau
2014-06-24Fix program cases and inversion tactic to correctly record universe constraints.Matthieu Sozeau
2014-06-24Clenvtac.clenv_refine in the new monad. Not satisfactory though, because itPierre-Marie Pédrot
2014-06-24Clenvtac.res_pf is in the new tactic monad.Pierre-Marie Pédrot
2014-06-23Clenvtac.unify is in the new monad.Pierre-Marie Pédrot
2014-06-23Removing opens to Clenvtac to track its use more easily.Pierre-Marie Pédrot
2014-06-23Oops, I fixed the .ml'sMatthieu Sozeau
2014-06-23Fix semantics of change p with c to typecheck c at each specific occurrence o...Matthieu Sozeau
2014-06-22Less goal-entering.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 09:13:10 +0000