index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
Commit message (
Expand
)
Author
Age
*
closing bug 3037
Julien Forest
2014-04-05
*
Using HMaps in global references.
Pierre-Marie Pédrot
2014-03-08
*
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 some generic equalities in Micromega.
Pierre-Marie Pédrot
2014-03-03
*
Fixing Pervasives.equality in extraction.
Pierre-Marie Pédrot
2014-03-03
*
Getting rid of generic hashes in cc plugin.
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
*
Removing generic equality in Syntax plugin.
Pierre-Marie Pédrot
2014-03-02
*
Fixing pervasive comparisons
Pierre-Marie Pédrot
2014-03-01
*
Proofview.Notations: Now that (>>=) is free, use it for tclBIND.
Arnaud Spiwack
2014-02-27
*
Lazyconstr -> Opaqueproof
Enrico Tassi
2014-02-26
*
New compilation mode -vi2vo
Enrico Tassi
2014-02-26
*
Stack operations of Reductionops in Reductionops.Stack
Pierre Boutillier
2014-02-24
*
Removing non-marshallable data from the Agram constructor. Instead of
Pierre-Marie Pédrot
2014-02-16
*
fast correction of bug #3234
Julien Forest
2014-02-14
*
Less dependencies in Omega.
Pierre-Marie Pédrot
2014-02-08
*
Relaunch all Unix.waitpid when they ended with EINTR
Pierre Letouzey
2014-01-30
*
bug correction in proving principles of function
jforest
2014-01-20
*
Omega: avoiding distinct proof-terms on repeated identical runs
Pierre Letouzey
2014-01-10
*
Qed: feedback when type checking is done
Enrico Tassi
2013-12-24
*
micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...
Frédéric Besson
2013-12-20
*
Removing the need of evarmaps in constr internalization.
Pierre-Marie Pédrot
2013-12-17
*
Fix g_derive.ml4.
Arnaud Spiwack
2013-12-04
*
Derive plugin.
Arnaud Spiwack
2013-12-04
*
Factoring(continued).
Arnaud Spiwack
2013-12-04
*
Refactoring: storing more information in the terminator closure.
Arnaud Spiwack
2013-12-04
*
The commands that initiate proofs are now in charge of what happens when proo...
Arnaud Spiwack
2013-12-04
*
Vernac classification: allow for commands which start proofs but must be sync...
Arnaud Spiwack
2013-12-04
*
Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.
Guillaume Melquiond
2013-12-03
*
Silence compilation warning by avoiding some deprecated constructs.
Guillaume Melquiond
2013-12-03
*
Writing [cut] tactic using the new monad.
Pierre-Marie Pédrot
2013-12-02
*
Getting rid of goal-dependency in declarative mode argument evaluation.
Pierre-Marie Pédrot
2013-11-27
*
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-11-27
*
Do not use ugly Dyn features in the Quote plugin. Use instead the
Pierre-Marie Pédrot
2013-11-26
*
Remove the Hiddentac module.
Arnaud Spiwack
2013-11-25
*
Field_theory: nicer notations for constants 0 1 ...
Pierre Letouzey
2013-11-21
*
Add Acc_intro_generator on top of all wf function proof (much much faster exe...
Julien Forest
2013-11-21
*
bugfix micromega: solved an ambiguous symbol resolution
fbesson
2013-11-15
*
Porting Tactics.assumption to the new engine.
ppedrot
2013-11-08
*
Fix congruence: normalise hypotheses with respect to evars.
aspiwack
2013-11-02
*
Made Proofview.Goal.hyps a named_context.
aspiwack
2013-11-02
*
Less use of the list-based interface for goal-bound tactics.
aspiwack
2013-11-02
*
Tachmach.New is now in Proofview.Goal.enter style.
aspiwack
2013-11-02
*
More Proofview.Goal.enter.
aspiwack
2013-11-02
*
Small syntax fix to be compatible with Ocaml 3.11.
aspiwack
2013-11-02
*
Adds a new goal selector "all:".
aspiwack
2013-11-02
*
Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).
aspiwack
2013-11-02
*
The tactic [admit] exits with the "unsafe" status.
aspiwack
2013-11-02
[next]