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
*
- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...
Matthieu Sozeau
2014-05-08
*
- Fix eq_constr_universes restricted to Sorts.equal
Matthieu Sozeau
2014-05-06
*
Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Fixing various backtrace recordings.
Pierre-Marie Pédrot
2014-04-25
*
Adding a [map] primitive to the tactic monad. Hopefully this should be
Pierre-Marie Pédrot
2014-04-20
*
Transfering the initial goals from the proofview to the proof object.
Pierre-Marie Pédrot
2014-04-07
*
Actually using the [modify] primitive.
Pierre-Marie Pédrot
2014-04-06
*
Evars introduced by Proofview refining are flagged as GoalEvar. For some
Pierre-Marie Pédrot
2014-04-01
*
Lighter interface for creating refining tactics.
Pierre-Marie Pédrot
2014-03-28
*
Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.
Pierre-Marie Pédrot
2014-03-26
*
Adding phantom types to discriminate normalized goals, and adding a way to
Pierre-Marie Pédrot
2014-03-19
*
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
[next]