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
*
Rewriting [lapply] tactic in the new monad.
Pierre-Marie Pédrot
2014-04-27
*
Giving true proof-terms in inversion instead of metas.
Pierre-Marie Pédrot
2014-04-27
*
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
*
Writing tclABSTRACT in the new monad. In particular the unsafe status is now
Pierre-Marie Pédrot
2014-04-24
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Removing the compatibility layer from Leminv. Also removed an undocumented
Pierre-Marie Pédrot
2014-04-22
*
Using the new monad tactic in Inv.
Pierre-Marie Pédrot
2014-04-22
*
Removing tactic compatibility layer from Elim.
Pierre-Marie Pédrot
2014-04-22
*
Small code cleaning in Tacticals.
Pierre-Marie Pédrot
2014-04-22
*
Simplifying interface of elimination tactics. They used dummy clausenvs, and
Pierre-Marie Pédrot
2014-04-22
*
Fixing bug #3285.
Pierre-Marie Pédrot
2014-04-20
*
Closing bug #3260
Julien Forest
2014-04-14
*
Removing unused functions in Refiner.
Pierre-Marie Pédrot
2014-04-06
*
Closing bug #3164
Julien Forest
2014-04-04
*
Removing the Change_evar refiner rule.
Pierre-Marie Pédrot
2014-03-31
*
Removing dead code in Tactics.
Pierre-Marie Pédrot
2014-03-31
*
Using the new refine interface to define ML tactics.
Pierre-Marie Pédrot
2014-03-28
*
Define Tactics.bring_hyps in the new monad.
Pierre-Marie Pédrot
2014-03-28
*
Removing tactic compatibility layer from Eqdecide.
Pierre-Marie Pédrot
2014-03-27
*
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
*
Removing tactic compatibility layer in Equality.
Pierre-Marie Pédrot
2014-03-26
*
Removing Tacmach compatibility layer in Inv.
Pierre-Marie Pédrot
2014-03-26
*
Removing tactic compatibility layer from Inv.
Pierre-Marie Pédrot
2014-03-26
*
Adding an interface to Eqdecide and putting the grammar rules in a dedicated
Pierre-Marie Pédrot
2014-03-26
*
Moving some tactic code to the new engine.
Pierre-Marie Pédrot
2014-03-26
*
Using non-normalized goals in tactic interpretation.
Pierre-Marie Pédrot
2014-03-19
*
Adding phantom types to discriminate normalized goals, and adding a way to
Pierre-Marie Pédrot
2014-03-19
*
Fix test-suite 2255.v
Pierre Boutillier
2014-03-17
*
Useless tactic bindings in Tacticals.
Pierre-Marie Pédrot
2014-03-07
*
Tentative fix for a very strange pervasive equality in Auto.
Pierre-Marie Pédrot
2014-03-07
*
Fixing generic equality in Auto.
Pierre-Marie Pédrot
2014-03-07
*
Remove some dead-code (thanks to ocaml warnings)
Pierre Letouzey
2014-03-05
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Fixing pervasive equalities. In particular, I removed the code that deleted
Pierre-Marie Pédrot
2014-03-03
*
Term dnets do no need to contain the afferent constr pattern in their nodes.
Pierre-Marie Pédrot
2014-03-03
*
Removing Termdn, and putting the relevant code in Btermdn. The current Termdn
Pierre-Marie Pédrot
2014-03-03
*
Extruding code not depending of the functor argument in Termdn.
Pierre-Marie Pédrot
2014-03-03
*
Replacing arguments of Trie by a cancellable monoid.
Pierre-Marie Pédrot
2014-03-03
*
Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)
Pierre Letouzey
2014-03-02
*
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
Pierre Letouzey
2014-03-02
*
Fixing pervasive comparisons
Pierre-Marie Pédrot
2014-03-01
*
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
[next]