index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
proofview.mli
Commit message (
Expand
)
Author
Age
*
Simplification of the tclCHECKINTERRUPT tactic.
Pierre-Marie Pédrot
2014-08-28
*
Cleaning and documenting a bit the Proofview.Refine module.
Pierre-Marie Pédrot
2014-08-28
*
"allows to", like "allowing to", is improper
Jason Gross
2014-08-25
*
Removing unused parts of the Goal.sensitive monad.
Pierre-Marie Pédrot
2014-08-21
*
New primitive allowing to modify refine handles.
Pierre-Marie Pédrot
2014-08-19
*
Adding a [make] primitive to the NonLogical monad.
Pierre-Marie Pédrot
2014-08-05
*
Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].
Arnaud Spiwack
2014-08-05
*
Cleaning of the new implementation of the tactic monad.
Arnaud Spiwack
2014-08-04
*
Add primtive [num_goal] to Proofview.
Arnaud Spiwack
2014-08-01
*
Clean outdated comment in Proofview.Notations.
Arnaud Spiwack
2014-08-01
*
Adding a tclBREAK primitive to the tactic monad.
Pierre-Marie Pédrot
2014-07-28
*
Add a tactic [swap i j] to swap the position of goals [i] and [j].
Arnaud Spiwack
2014-07-25
*
Adds a cycle tactic to reorder goals in a loop.
Arnaud Spiwack
2014-07-25
*
A handful of useful primitives in Proofview.Refine.
Arnaud Spiwack
2014-07-24
*
Proof_global.start_dependent_proof: properly threads the sigma through the te...
Arnaud Spiwack
2014-07-23
*
Adding a "time" tactical for benchmarking purposes. In case the tactic
Hugo Herbelin
2014-07-13
*
check_for_interrupt: better (but slower) in threading mode
Enrico Tassi
2014-07-10
*
Exporting Proof.split in proofview.
Pierre-Marie Pédrot
2014-07-08
*
Revert "time tac" (committed by mistake).
Hugo Herbelin
2014-07-07
*
time tac
Hugo Herbelin
2014-07-07
*
Adding a raw_goals primitive for Tacinterp.
Pierre-Marie Pédrot
2014-06-19
*
Proofs now take and return an evar_universe_context, simplifying interfaces
Matthieu Sozeau
2014-06-18
*
The tactic interpreter now uses a new type of tactics, through
Pierre-Marie Pédrot
2014-06-03
*
Revert "Chasing the goal entering backward while interpreting tactics. This r...
Pierre-Marie Pédrot
2014-05-24
*
Chasing the goal entering backward while interpreting tactics. This required
Pierre-Marie Pédrot
2014-05-24
*
- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...
Matthieu Sozeau
2014-05-08
*
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
*
Transfering the initial goals from the proofview to the proof object.
Pierre-Marie Pédrot
2014-04-07
*
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
*
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
*
Typos in comment.
Arnaud Spiwack
2014-01-31
*
Allow proofs to start with dependent goals.
Arnaud Spiwack
2013-12-04
*
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
*
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
*
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
*
Adds a tactical once.
aspiwack
2013-11-02
[next]