index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
Commit message (
Expand
)
Author
Age
...
*
Lighter interface for creating refining tactics.
Pierre-Marie Pédrot
2014-03-28
*
Removing tactic compatibility layer from Eqdecide.
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 Inv.
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
*
Potentially unused computation in Goal.
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
*
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
*
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
*
Lazyconstr -> Opaqueproof
Enrico Tassi
2014-02-26
*
New compilation mode -vi2vo
Enrico Tassi
2014-02-26
*
Tacinterp: fewer Proofview.Goal.enterl.
Arnaud Spiwack
2014-02-25
*
cbn understands Arguments
Pierre Boutillier
2014-02-24
*
Stack operations of Reductionops in Reductionops.Stack
Pierre Boutillier
2014-02-24
*
More sharing in Logic, together with some code cleaning.
Pierre-Marie Pédrot
2014-02-21
*
TC: honor the use_typeclasses flag in pretyping
Enrico Tassi
2014-02-12
*
STM: fix valid_id coming from Qed errors
Enrico Tassi
2014-02-10
*
Tracking memory misallocation by trying to improve sharing.
Pierre-Marie Pédrot
2014-02-03
*
Fixing backtrace reporting.
Pierre-Marie Pédrot
2014-02-02
*
Typos in comment.
Arnaud Spiwack
2014-01-31
*
Fixing backtrace handling here and there.
Pierre-Marie Pédrot
2014-01-30
*
Useless Array.of_list
Pierre-Marie Pédrot
2014-01-10
*
Exporting the full pretyper options in Goal.constr_of_raw.
Pierre-Marie Pédrot
2014-01-10
*
Algebraized "No such hypothesis" errors
Pierre-Marie Pédrot
2014-01-06
*
Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, wit...
Arnaud Spiwack
2014-01-06
*
Proof_using: new syntax + suggestion
Enrico Tassi
2014-01-05
*
Proof_global: Simpler API for proof_terminator
Enrico Tassi
2014-01-04
*
Support for evars and metas in native compiler.
Maxime Dénès
2013-12-30
*
Qed: feedback when type checking is done
Enrico Tassi
2013-12-24
*
Removing the need of evarmaps in constr internalization.
Pierre-Marie Pédrot
2013-12-17
*
Fixing backtrace registering of various tactic-related try-with blocks.
Pierre-Marie Pédrot
2013-12-11
*
Fix Admitted.
Arnaud Spiwack
2013-12-04
*
Proof_global: fix start_proof comment after the preceding commits.
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
*
Allow proofs to start with dependent goals.
Arnaud Spiwack
2013-12-04
*
Fixing ltac constr variable handling in refine.
Pierre-Marie Pédrot
2013-11-30
*
Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute not
Hugo Herbelin
2013-11-29
*
Useless computation in Goal handle augmentation.
ppedrot
2013-11-12
*
Do not print tactic notation names at each interpretation step.
ppedrot
2013-11-12
[prev]
[next]