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
*
Removing a fishy use of pervasive equality in Ltac backtrace printing.
Pierre-Marie Pédrot
2014-03-01
*
Removing Pervasives.compare in Termdn.
Pierre-Marie Pédrot
2014-02-28
*
Tacinterp: more refactoring.
Arnaud Spiwack
2014-02-27
*
Tacinterp: refactoring using Monad.
Arnaud Spiwack
2014-02-27
*
Code refactoring thanks to the new Monad module.
Arnaud Spiwack
2014-02-27
*
Remove unsafe code (Obj.magic) in Tacinterp.
Arnaud Spiwack
2014-02-27
*
Proofview.Notations: Now that (>>=) is free, use it for tclBIND.
Arnaud Spiwack
2014-02-27
*
Get rid of the enterl/glist API for Proofview.Goal.
Arnaud Spiwack
2014-02-27
*
Tacinterp: yet another superfluous enterl.
Arnaud Spiwack
2014-02-27
*
Tacinterp: spurious enterl.
Arnaud Spiwack
2014-02-27
*
Dead code: eval_ltac_constr.
Arnaud Spiwack
2014-02-27
*
Tacinterp: remove the is_value check in Ltac's let-in.
Arnaud Spiwack
2014-02-25
*
Tacinterp: fewer enterl still.
Arnaud Spiwack
2014-02-25
*
Tacinterp: fewer Proofview.Goal.enterl.
Arnaud Spiwack
2014-02-25
*
Tacinterp: clean up.
Arnaud Spiwack
2014-02-25
*
Tacinterp: remove unnecessary return/bind pairs.
Arnaud Spiwack
2014-02-25
*
TacticMatching: avoid some closure allocation in (<*>).
Arnaud Spiwack
2014-02-24
*
Removed some trailing whitespaces.
Arnaud Spiwack
2014-02-24
*
IStream: a concat_map primitive.
Arnaud Spiwack
2014-02-24
*
A view type for IStream.
Arnaud Spiwack
2014-02-24
*
Removing non-marshallable data from the Agram constructor. Instead of
Pierre-Marie Pédrot
2014-02-16
*
The constructor tactic now returns several successes.
Pierre-Marie Pédrot
2014-02-04
*
Fixing bug #3226.
Pierre-Marie Pédrot
2014-02-02
*
In Ltac's exact tactic: avoid checking the type of the term twice.
Arnaud Spiwack
2014-01-31
*
Fixing dependent inversion. Some exceptions were not caught by the tactic
Pierre-Marie Pédrot
2014-01-28
*
Adding a default object to generic argument registering mechanism.
Pierre-Marie Pédrot
2014-01-19
*
Fixing bug #1758: Print Hint output can be misleading if variable shadows hyp...
Pierre-Marie Pédrot
2014-01-17
*
Removing unused tactics in rewrite.
Pierre-Marie Pédrot
2014-01-14
*
Exporting the full pretyper options in Goal.constr_of_raw.
Pierre-Marie Pédrot
2014-01-10
*
Fix bug#2080: error message on Ltac name clash with primitive tactics
xclerc
2014-01-10
*
Algebraized "No such hypothesis" errors
Pierre-Marie Pédrot
2014-01-06
*
Code cleaning in Rewrite, may also result faster.
Pierre-Marie Pédrot
2014-01-04
*
Qed: feedback when type checking is done
Enrico Tassi
2013-12-24
*
Simplifying the use of hypinfos in Rewrite.
Pierre-Marie Pédrot
2013-12-24
*
Rewrite.ml: removing direction flag from hypinfo.
Pierre-Marie Pédrot
2013-12-23
*
Do not pass unification flags around in Rewrite.
Pierre-Marie Pédrot
2013-12-22
*
Slight code cleaning ensuring more static invariants in Rewrite.
Pierre-Marie Pédrot
2013-12-22
*
Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at
Pierre-Marie Pédrot
2013-12-22
*
Removing the useless pattern ident genarg.
Pierre-Marie Pédrot
2013-12-19
*
Using interp_genarg in tactic notations where possible, instead of an ad-hoc
Pierre-Marie Pédrot
2013-12-19
*
Bad use of Obj.magic in interpretation of TacAlias arguments.
Pierre Boutillier
2013-12-19
*
Printing function for Stdargs in debugger
Pierre Boutillier
2013-12-19
*
Removing the need of evarmaps in constr internalization.
Pierre-Marie Pédrot
2013-12-17
*
Get rid of messages "emitting ..." when compiling .v files
Pierre Letouzey
2013-12-16
*
Dedicated inductive for return values of rewrite strategies.
Pierre-Marie Pédrot
2013-12-16
*
Fixing backtrace registering of various tactic-related try-with blocks.
Pierre-Marie Pédrot
2013-12-11
*
Stylistic change.
Arnaud Spiwack
2013-12-09
*
Vernac classification: allow for commands which start proofs but must be sync...
Arnaud Spiwack
2013-12-04
*
Porting type interpretation in Tacinterp to the new tactics.
Pierre-Marie Pédrot
2013-12-02
*
Writing [cut] tactic using the new monad.
Pierre-Marie Pédrot
2013-12-02
[next]