index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Commit message (
Expand
)
Author
Age
*
Fix segfault in native compiler on int31 division.
Maxime Dénès
2014-10-10
*
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-09
*
Forgotten hints.ml{,i} files in 38b34dfffcc.
Hugo Herbelin
2014-10-08
*
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-07
*
Make tclEFFECTS also update the env in the proof monad
Enrico Tassi
2014-10-06
*
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-05
*
Fixing #3657 (check that both sides of a "change with" have the same
Hugo Herbelin
2014-10-03
*
Fixing bug #2810 (autounfold on local variable declared as hint but cleared).
Hugo Herbelin
2014-10-02
*
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-10-01
*
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-30
*
Merging some functions from evarutil.ml/evd.ml.
Hugo Herbelin
2014-09-29
*
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-27
*
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-24
*
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-23
*
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-21
*
Fixing strange evarmap leak in goals.
Pierre-Marie Pédrot
2014-09-18
*
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-17
*
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
2014-09-15
*
The unifying functions of Rewrite uses the return types of strategies.
Pierre-Marie Pédrot
2014-09-15
*
Splitting the uses of the unification function according to the status of
Pierre-Marie Pédrot
2014-09-15
*
Rewrite.apply_strategy uses the same return type as strategies.
Pierre-Marie Pédrot
2014-09-14
*
Proper type for rewrite strategy results.
Pierre-Marie Pédrot
2014-09-14
*
Retroknowledge arguments are made VERNAC ARGUMENTS.
Pierre-Marie Pédrot
2014-09-13
*
Fixing injection bug #3616 on sigma-types.
Hugo Herbelin
2014-09-13
[next]