index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
proofview.ml
Commit message (
Expand
)
Author
Age
*
Remove some dead-code (thanks to ocaml warnings)
Pierre Letouzey
2014-03-05
*
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: fewer Proofview.Goal.enterl.
Arnaud Spiwack
2014-02-25
*
Fixing backtrace handling here and there.
Pierre-Marie Pédrot
2014-01-30
*
Fixing backtrace registering of various tactic-related try-with blocks.
Pierre-Marie Pédrot
2013-12-11
*
Allow proofs to start with dependent goals.
Arnaud Spiwack
2013-12-04
*
Reducing allocation in tclDISPATCHGEN, by doing a List.map at the same time
ppedrot
2013-11-05
*
Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was sol...
aspiwack
2013-11-04
*
Fix the tactical ; [ … ] : the "incorrect number of goal" error was not cau...
aspiwack
2013-11-04
*
Allowing proofs starting with a non-empty evarmap.
ppedrot
2013-11-04
*
A try/with was catching every exception.
aspiwack
2013-11-02
*
Update comments.
aspiwack
2013-11-02
*
Fix destruct: nf_evar prior to tactic interpretation.
aspiwack
2013-11-02
*
Adds a tactic give_up.
aspiwack
2013-11-02
*
A tactic shelve_unifiable.
aspiwack
2013-11-02
*
Corrects a bug on Proofview.Goal.enter whereby sigmas were captured and used ...
aspiwack
2013-11-02
*
Adds a shelve tactic.
aspiwack
2013-11-02
*
Adds an experimental exactly_once tactical.
aspiwack
2013-11-02
*
Made Proofview.Goal.hyps a named_context.
aspiwack
2013-11-02
*
A dedicated view type for Proofview_gen.split.
aspiwack
2013-11-02
*
Adds a tactical once.
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
*
Try to remove intermediate allocations when dealing with goal-specific tactics.
aspiwack
2013-11-02
*
Various rewriting, mostly for speed purposes.
aspiwack
2013-11-02
*
Makes the Ltac debugger usable again.
aspiwack
2013-11-02
*
Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...
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
*
Cleanup of comments.
aspiwack
2013-11-02
*
Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.
aspiwack
2013-11-02
*
Bases tactics on an IO monad.
aspiwack
2013-11-02
*
Getting rid of Goal.here, and all the related exceptions and combinators.
aspiwack
2013-11-02
*
Uses Proofview.tclEXTEND more sparingly.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
Moving side effects into evar_map. There was no reason to keep another
ppedrot
2013-10-05
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Partly replacing list-based access functions in Evd. This is still
ppedrot
2013-09-03
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Fixing bug #3030.
ppedrot
2013-06-06
*
Getting rid of LtacLocated exception transformer.
ppedrot
2013-05-28
*
Removing Exc_located and using the new exception enrichement
ppedrot
2013-02-18
*
Added propagation of evars unification failure reasons for better
herbelin
2013-02-17
*
Revised the Ltac trace mechanism so that trace breaking due to
herbelin
2013-02-17
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Monomorphization (proof)
ppedrot
2012-11-25
[next]