| Age | Commit message (Expand) | Author |
|---|
| 2014-10-16 | Proofview.Refine: remove the handle type, and simplify the API. | Arnaud Spiwack |
| 2014-10-15 | Fix for bug #3618. | Matthieu Sozeau |
| 2014-10-15 | Remaining tactics of the Auto module were put in the monad. | Pierre-Marie Pédrot |
| 2014-10-14 | Fix bug #3698: stack overflow due to eta+canonical structures in | Matthieu Sozeau |
| 2014-10-13 | Fixing "change" and "fold" after convert_hyp/convert_concl moved to | Hugo Herbelin |
| 2014-10-13 | Add support for deactivating type class inference from induction/destruct. | Hugo Herbelin |
| 2014-10-10 | Fix segfault in native compiler on int31 division. | Maxime Dénès |
| 2014-10-09 | Propagating name of goal to main subgoal in cut and conversion tactics. | Hugo Herbelin |
| 2014-10-09 | A version of convert_concl and convert_hyp in new proof engine. | Hugo Herbelin |
| 2014-10-08 | Forgotten hints.ml{,i} files in 38b34dfffcc. | Hugo Herbelin |
| 2014-10-07 | Splitting out of auto.ml a file hints.ml dedicated to hints so as to | Hugo Herbelin |
| 2014-10-07 | Removing debugging information committed by mistake. | Hugo Herbelin |
| 2014-10-06 | Make tclEFFECTS also update the env in the proof monad | Enrico Tassi |
| 2014-10-05 | Semantic fix of a refine in Rewrite. | Pierre-Marie Pédrot |
| 2014-10-05 | Check compatibility of types in change depending on whether it is a | Hugo Herbelin |
| 2014-10-03 | Fixing #3657 (check that both sides of a "change with" have the same | Hugo Herbelin |
| 2014-10-02 | Fixing bug #2810 (autounfold on local variable declared as hint but cleared). | Hugo Herbelin |
| 2014-10-01 | Fixing nice printing of error reporting with ml tactics bound to ltac names. | Hugo Herbelin |
| 2014-10-01 | Made Tacsubst independent of Auto at linking time so that Tacenv does | Hugo Herbelin |
| 2014-09-30 | Seeing IntroWildcard as an action intro pattern rather than as a naming pattern | Hugo Herbelin |
| 2014-09-30 | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin |
| 2014-09-29 | Merging some functions from evarutil.ml/evd.ml. | Hugo Herbelin |
| 2014-09-27 | Keyed unification option, compiling the whole standard library | Matthieu Sozeau |
| 2014-09-27 | Remove auto's use of dummy goal, use the proper sigma for pattern_of_constr. | Matthieu Sozeau |
| 2014-09-27 | Make pattern_of_constr typed so that we can infer the proper patterns | Matthieu Sozeau |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-27 | Changed semantics of induction !id when a clause is given: don't | Hugo Herbelin |
| 2014-09-27 | Removing the last use of tclSENSITIVE in favour of tclNEWGOALS. | Pierre-Marie Pédrot |
| 2014-09-24 | Rename eq_constr functions in Evd to not break backward compatibility | Matthieu Sozeau |
| 2014-09-24 | Make eq_pattern_test/eq_test work up to the equivalence of primitive | Matthieu Sozeau |
| 2014-09-24 | Using an or_var rather than the hack with loc for coding a pure ident | Hugo Herbelin |
| 2014-09-24 | Added support for interpreting hyp lists in tactic notations. | Hugo Herbelin |
| 2014-09-23 | ATBR can't compile without the fix, as it uses setoid_rewrite to rewrite | Matthieu Sozeau |
| 2014-09-23 | Fix bug in setoid_rewrite introduced by PMP's commits, which was creating | Matthieu Sozeau |
| 2014-09-21 | Rewrite.apply_lemma is written in state passing style. | Pierre-Marie Pédrot |
| 2014-09-21 | More invariants in the code of Refine. | Pierre-Marie Pédrot |
| 2014-09-21 | Removing a nonsensical Errors.push. | Pierre-Marie Pédrot |
| 2014-09-18 | Fixing strange evarmap leak in goals. | Pierre-Marie Pédrot |
| 2014-09-17 | Be more conservative and keep the use of eq_constr in pretyping/ functions. | Matthieu Sozeau |
| 2014-09-17 | Fix bug #3593, making constr_eq and progress work up to | Matthieu Sozeau |
| 2014-09-17 | Fix bug #3633 properly, by delaying the interpetation of constrs in | Matthieu Sozeau |
| 2014-09-17 | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau |
| 2014-09-15 | Add a "Hint Mode ref (+ | -)*" hint for setting a global mode | Matthieu Sozeau |
| 2014-09-15 | Fix timing of evar-normalisation of goals in [Ftactic.nf_enter]. | Arnaud Spiwack |
| 2014-09-15 | Ltac names in binders: some Ltac values can be seen both as terms and identif... | Arnaud Spiwack |
| 2014-09-15 | A small pass of code cleaning and clenv removing in Rewrite. | Pierre-Marie Pédrot |
| 2014-09-15 | Avoid backtracking in typeclass search if a solution for a closed | Matthieu Sozeau |
| 2014-09-15 | Rework typeclass resolution and control of backtracking. | Matthieu Sozeau |
| 2014-09-15 | Removing one Evd.merge in Rewrite. | Pierre-Marie Pédrot |
| 2014-09-15 | More invariants in Rewrite unification. | Pierre-Marie Pédrot |
