aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Expand)AuthorAge
...
* Refine tactic: simplify the conclusion only at the end of the tactic.Gravatar Arnaud Spiwack2014-10-22
* Remove an unnecessary use of [Proofview.Unsafe.tclEVARS] in [convert_concl].Gravatar Arnaud Spiwack2014-10-22
* Split [Proofview] into a file where the basic operations on the state are def...Gravatar Arnaud Spiwack2014-10-22
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Remove the deprecated open-constr based refine.Gravatar Arnaud Spiwack2014-10-22
* Remove duplicate code.Gravatar Arnaud Spiwack2014-10-22
* Removing re-typecheking from "refine" in no-check mode of the newGravatar Hugo Herbelin2014-10-20
* Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...Gravatar Hugo Herbelin2014-10-17
* Essai où assert_style n'est utilisé que si pas visuellement une équation;Gravatar Hugo Herbelin2014-10-17
* Relaxing again the test on types of replacements in tactic changeGravatar Hugo Herbelin2014-10-16
* In convert_concl/convert_hyp: nf_enter -> enter.Gravatar Hugo Herbelin2014-10-16
* Refresh to avoid algebraic universes on the right.Gravatar Matthieu Sozeau2014-10-16
* Goal: remove most of the API (make [Goal.goal] concrete).Gravatar Arnaud Spiwack2014-10-16
* Proofview.Refine: remove the handle type, and simplify the API.Gravatar Arnaud Spiwack2014-10-16
* Fix bug #3698: stack overflow due to eta+canonical structures inGravatar Matthieu Sozeau2014-10-14
* Fixing "change" and "fold" after convert_hyp/convert_concl moved toGravatar Hugo Herbelin2014-10-13
* Add support for deactivating type class inference from induction/destruct.Gravatar Hugo Herbelin2014-10-13
* Propagating name of goal to main subgoal in cut and conversion tactics.Gravatar Hugo Herbelin2014-10-09
* A version of convert_concl and convert_hyp in new proof engine.Gravatar Hugo Herbelin2014-10-09
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Removing debugging information committed by mistake.Gravatar Hugo Herbelin2014-10-07
* Make tclEFFECTS also update the env in the proof monadGravatar Enrico Tassi2014-10-06
* Check compatibility of types in change depending on whether it is aGravatar Hugo Herbelin2014-10-05
* Fixing #3657 (check that both sides of a "change with" have the sameGravatar Hugo Herbelin2014-10-03
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Changed semantics of induction !id when a clause is given: don'tGravatar Hugo Herbelin2014-09-27
* Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.Gravatar Pierre-Marie Pédrot2014-09-27
* Rename eq_constr functions in Evd to not break backward compatibilityGravatar Matthieu Sozeau2014-09-24
* Make eq_pattern_test/eq_test work up to the equivalence of primitiveGravatar Matthieu Sozeau2014-09-24
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Fix bug #3633 properly, by delaying the interpetation of constrs inGravatar Matthieu Sozeau2014-09-17
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Commit 682aa67cc80 about enforcing that apply does not create newGravatar Hugo Herbelin2014-09-12
* Keeping a sub-optimal behavior of intros_possibly_replacing for compatibility...Gravatar Hugo Herbelin2014-09-11
* Other bugs with "inversion as" (collision between user-provided names and gen...Gravatar Hugo Herbelin2014-09-11
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
* More small bugs in intros_replacing.Gravatar Hugo Herbelin2014-09-10
* Fixing inversion after having fixed intros_replacingGravatar Hugo Herbelin2014-09-10
* Fix [induction] wrt inductive records and non-recursive variants.Gravatar Arnaud Spiwack2014-09-08
* Fixing a bug in intros_replacing which was causing inversion notGravatar Hugo Herbelin2014-09-07
* Fixing clearbody : typecheck definitions in context.Gravatar Pierre-Marie Pédrot2014-09-06
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-05
* At last a working clearbody!Gravatar Pierre-Marie Pédrot2014-09-05
* Revert the two previous commits. I was testing in the wrong branch.Gravatar Pierre-Marie Pédrot2014-09-04
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 03:02:54 +0000