index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
equality.ml
Commit message (
Expand
)
Author
Age
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.
Hugo Herbelin
2014-12-07
*
Reverting the following block of three commits:
Hugo Herbelin
2014-11-27
*
Experimenting always forcing convertibility on strict implicit arguments
Hugo Herbelin
2014-11-26
*
Fixing side bug in db37c9f3f32ae7 delaying interpretation of the
Hugo Herbelin
2014-11-16
*
Follow up to experimental eager evar unification in bcba6d1bc9:
Hugo Herbelin
2014-11-08
*
Proofview: split [V82] module into [Unsafe] and [V82].
Arnaud Spiwack
2014-10-22
*
Merging some functions from evarutil.ml/evd.ml.
Hugo Herbelin
2014-09-29
*
Fix bug #3593, making constr_eq and progress work up to
Matthieu Sozeau
2014-09-17
*
Fixing injection bug #3616 on sigma-types.
Hugo Herbelin
2014-09-13
*
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
*
A step towards better differentiating when w_unify is used for subterm
Hugo Herbelin
2014-09-10
*
Renaming goal-entering functions.
Pierre-Marie Pédrot
2014-09-06
*
Improving error message when applying rewrite to an expression which is not a...
Hugo Herbelin
2014-08-18
*
Factorizing cutrewrite (to be made obsolote) and dependent rewrite (to
Hugo Herbelin
2014-08-18
*
Slight simplification of naming of tactics in equality.ml (hopefully).
Hugo Herbelin
2014-08-18
*
A reorganization of the "assert" tactics (hopefully uniform naming
Hugo Herbelin
2014-08-18
*
Reorganisation of intropattern code
Hugo Herbelin
2014-08-18
*
Reorganization of tactics:
Hugo Herbelin
2014-08-18
*
In Hipattern: some functions not working modulo evar instantiation.
Arnaud Spiwack
2014-08-07
*
Experimentally adding an option for automatically erasing an
Hugo Herbelin
2014-08-05
*
A new step in the new "standard" naming policy for propositional hypotheses
Hugo Herbelin
2014-08-05
*
Remove spurious [1] in equality.ml.
Arnaud Spiwack
2014-08-01
*
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-08-01
*
Fix program cases and inversion tactic to correctly record universe constraints.
Matthieu Sozeau
2014-06-24
*
Removing opens to Clenvtac to track its use more easily.
Pierre-Marie Pédrot
2014-06-23
*
More on injection over a projectable "existT". - Fixing syntax "injection ......
Hugo Herbelin
2014-05-31
*
Fixing introduction patterns * and ** when used in a branch so that they do n...
Hugo Herbelin
2014-05-31
*
Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").
Hugo Herbelin
2014-05-31
*
When discrimination is not possible, try to project.
Maxime Dénès
2014-05-18
*
Suggest Set Injection On Proofs in error message for injection.
Maxime Dénès
2014-05-18
*
Restored old behavior of injection on proofs by default.
Maxime Dénès
2014-05-18
*
Code cleaning & factorizing functions in Equality.
Pierre-Marie Pédrot
2014-05-09
*
Encapsulating some clausenv uses. This simplifies the control flow of some
Pierre-Marie Pédrot
2014-05-08
*
Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."
Hugo Herbelin
2014-05-08
*
Avoid "revert" to retype-check the goal, and move it to a "new" tactic.
Hugo Herbelin
2014-05-08
*
Simplification and improvement of "subst x" in such a way that it
Hugo Herbelin
2014-05-08
*
Fixes after rebase. The use of pf_constr_of_global is problematic in presence...
Matthieu Sozeau
2014-05-06
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
Adapt Y. Bertot's path on private inductives (now the keyword is "Private").
Yves Bertot
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Trying to improve the error messages of injection.
Maxime Dénès
2014-04-30
*
Injection: do not fail when arguments have sort Prop.
Maxime Dénès
2014-04-29
*
Removing useless try-with clauses in Goal.enter variants.
Pierre-Marie Pédrot
2014-04-25
*
Fixing various backtrace recordings.
Pierre-Marie Pédrot
2014-04-25
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Closing bug #3260
Julien Forest
2014-04-14
*
Cosmetic changes in Equality.
Pierre-Marie Pédrot
2014-03-27
*
Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.
Pierre-Marie Pédrot
2014-03-26
*
Removing Tacmach compatibility layer in Equality.
Pierre-Marie Pédrot
2014-03-26
[next]