aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Expand)AuthorAge
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-04
* Reimplementing the clearbody tactic.Gravatar Pierre-Marie Pédrot2014-09-04
* Proofview refiner is now type-safe by default.Gravatar Pierre-Marie Pédrot2014-09-04
* Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Gravatar Pierre-Marie Pédrot2014-09-04
* Yes another remaining clearing bug with 'apply in'.Gravatar Hugo Herbelin2014-09-03
* Another fix than 19a7a5789c to avoid descend_in_conjunction to useGravatar Hugo Herbelin2014-09-02
* Not using a "cut" in descend_in_conjunctions induced more success. WeGravatar Hugo Herbelin2014-08-29
* Removing spurious tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-27
* Fixing previous commit.Gravatar Pierre-Marie Pédrot2014-08-25
* Fixing a bug introduced in the extension of 'apply in' + simplifying code.Gravatar Hugo Herbelin2014-08-25
* Tactics.is_quantified_hypothesis does not reduce anymore to decide whetherGravatar Pierre-Marie Pédrot2014-08-23
* Tactics.unify in the new monad.Gravatar Pierre-Marie Pédrot2014-08-23
* Removing unused parts of the Goal.sensitive monad.Gravatar Pierre-Marie Pédrot2014-08-21
* 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
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* Fixing too restrictive detection of resolution of evars in "apply in"Gravatar Hugo Herbelin2014-08-16
* Restore the error-handling behavior of [change], which was silently failingGravatar Matthieu Sozeau2014-08-14
* In Hipattern: some functions not working modulo evar instantiation.Gravatar Arnaud Spiwack2014-08-07
* 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
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
* Cleaning of the new implementation of the tactic monad.Gravatar Arnaud Spiwack2014-08-04
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Removing more tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
* Removing some tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
* Add an option to solve typeclass goals generated by apply which can't beGravatar Matthieu Sozeau2014-07-31
* Restore proper order of effects in letin_tac_gen. Fixes CFGV again.Gravatar Matthieu Sozeau2014-07-03
* Synchronized names from the "as" clause with the skeleton of theGravatar Hugo Herbelin2014-06-30
* Small refinement about whether it is tolerated for compatibility thatGravatar Hugo Herbelin2014-06-28
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
* Extra check for indirect dependency when abstracting a term which isGravatar Hugo Herbelin2014-06-28
* Made the subterm finding function make_abstraction independent of theGravatar Hugo Herbelin2014-06-28
* Incorrect folding of evars in let_tac_gen made remember fail to storeGravatar Matthieu Sozeau2014-06-25
* In exact check, use e_type_of to ensure that universe constraints necessaryGravatar Matthieu Sozeau2014-06-25
* Clenvtac.clenv_refine in the new monad. Not satisfactory though, because itGravatar Pierre-Marie Pédrot2014-06-24
* Clenvtac.res_pf is in the new tactic monad.Gravatar Pierre-Marie Pédrot2014-06-24
* Removing opens to Clenvtac to track its use more easily.Gravatar Pierre-Marie Pédrot2014-06-23
* Fix semantics of change p with c to typecheck c at each specific occurrence o...Gravatar Matthieu Sozeau2014-06-23
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Check resolution of Metas turned into Evars by pose_all_metas_as_evarsGravatar Hugo Herbelin2014-06-13
* Passing some tactics to the new monad type.Gravatar Pierre-Marie Pédrot2014-06-12
* fix handling of side effects in abstract (fixes QArithSternBrocot)Gravatar Enrico Tassi2014-06-11
* Preserve compatibility on examples such as "intros []." on goals suchGravatar Hugo Herbelin2014-06-06
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* Fixing introduction patterns * and ** when used in a branch so that they do n...Gravatar Hugo Herbelin2014-05-31
* 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-07-02 05:42:00 +0000