aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* 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 some functions from the compatibility layer.Gravatar Arnaud Spiwack2014-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 for bug #3618.Gravatar Matthieu Sozeau2014-10-15
* Remaining tactics of the Auto module were put in the monad.Gravatar Pierre-Marie Pédrot2014-10-15
* 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
* Fix segfault in native compiler on int31 division.Gravatar Maxime Dénès2014-10-10
* 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
* Forgotten hints.ml{,i} files in 38b34dfffcc.Gravatar Hugo Herbelin2014-10-08
* 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
* Semantic fix of a refine in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-05
* 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
* Fixing bug #2810 (autounfold on local variable declared as hint but cleared).Gravatar Hugo Herbelin2014-10-02
* Fixing nice printing of error reporting with ml tactics bound to ltac names.Gravatar Hugo Herbelin2014-10-01
* Made Tacsubst independent of Auto at linking time so that Tacenv doesGravatar Hugo Herbelin2014-10-01
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* Remove auto's use of dummy goal, use the proper sigma for pattern_of_constr.Gravatar Matthieu Sozeau2014-09-27
* Make pattern_of_constr typed so that we can infer the proper patternsGravatar Matthieu Sozeau2014-09-27
* 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
* Using an or_var rather than the hack with loc for coding a pure identGravatar Hugo Herbelin2014-09-24
* Added support for interpreting hyp lists in tactic notations.Gravatar Hugo Herbelin2014-09-24
* ATBR can't compile without the fix, as it uses setoid_rewrite to rewriteGravatar Matthieu Sozeau2014-09-23
* Fix bug in setoid_rewrite introduced by PMP's commits, which was creatingGravatar Matthieu Sozeau2014-09-23
* Rewrite.apply_lemma is written in state passing style.Gravatar Pierre-Marie Pédrot2014-09-21
* More invariants in the code of Refine.Gravatar Pierre-Marie Pédrot2014-09-21
* Removing a nonsensical Errors.push.Gravatar Pierre-Marie Pédrot2014-09-21
* Fixing strange evarmap leak in goals.Gravatar Pierre-Marie Pédrot2014-09-18
* 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
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
* Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].Gravatar Arnaud Spiwack2014-09-15
* Ltac names in binders: some Ltac values can be seen both as terms and identif...Gravatar Arnaud Spiwack2014-09-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 03:41:22 +0000