index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
proof.ml
Commit message (
Expand
)
Author
Age
*
Add an invariant on future goals in Proof.run_tactic.
Hugo Herbelin
2018-03-08
*
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-05
|
\
*
|
[econstr] Continue consolidation of EConstr API under `interp`.
Emilio Jesus Gallego Arias
2018-02-28
|
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
|
/
*
[proof] [api] Rename proof types in preparation for functionalization.
Emilio Jesus Gallego Arias
2017-11-29
*
[proof] Attempt to deprecate some V82 parts of the proof API.
Emilio Jesus Gallego Arias
2017-11-19
*
[api] Insert miscellaneous API deprecation back to core.
Emilio Jesus Gallego Arias
2017-11-13
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
A fix to #5414 (ident bound by ltac names now known for "match").
Hugo Herbelin
2017-06-09
*
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
Adding a printer for Proof.proof reflecting the focusing layout.
Hugo Herbelin
2017-01-26
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-12
|
\
|
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-12
|
|
\
|
|
*
Fix bug #5123: mark all shelved evars unresolvable
Matthieu Sozeau
2016-10-11
*
|
|
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
*
|
|
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-08-19
|
/
/
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
Moving Refine to its proper module.
Pierre-Marie Pédrot
2016-03-20
*
|
Extruding the code for the Existential command from Proofview.
Pierre-Marie Pédrot
2016-03-20
|
/
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Proof: suggest Admitted->Qed only if the proof is really complete (#4349)
Enrico Tassi
2015-09-20
*
STM/Univ: save initial univs (the ones in the statement) in Proof.proof
Enrico Tassi
2015-05-29
*
Update headers.
Maxime Dénès
2015-01-12
*
Make sure the goals on the shelve are identified as goal and unresolvable for...
Arnaud Spiwack
2014-12-12
*
Fix (somewhat obsolete) [Existential] command, which conflicted with the shelf.
Arnaud Spiwack
2014-11-28
*
new: Optimize Proof, Optimize Heap
Enrico Tassi
2014-11-09
*
Add [Info] command.
Arnaud Spiwack
2014-11-01
*
An API for info traces.
Arnaud Spiwack
2014-11-01
*
Evd.future_goals: forgot to revert the list in two places.
Arnaud Spiwack
2014-10-23
*
Proofview: move [list_goto] to the [CList] module.
Arnaud Spiwack
2014-10-22
*
Proofview: remove a redundant primitive.
Arnaud Spiwack
2014-10-22
*
Proofview: move more functions to the Unsafe module.
Arnaud Spiwack
2014-10-22
*
Remove unused functions for side effects.
Arnaud Spiwack
2014-10-22
*
Refactoring proofview: make the definition of the logic monad polymorphic.
Arnaud Spiwack
2014-10-16
*
Put evars remaining after a tactic on the shelf.
Arnaud Spiwack
2014-10-16
*
Goal: remove [advance] from the API.
Arnaud Spiwack
2014-10-16
*
Factored out IDE goal structure.
Carst Tankink
2014-10-01
*
Small reorganisation in proof.ml.
Arnaud Spiwack
2014-07-25
*
Fail gracefully when focusing on non-existing goals with user commands.
Arnaud Spiwack
2014-07-25
*
Proof_global.start_dependent_proof: properly threads the sigma through the te...
Arnaud Spiwack
2014-07-23
*
Transfering the initial goals from the proofview to the proof object.
Pierre-Marie Pédrot
2014-04-07
*
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
*
Allowing proofs starting with a non-empty evarmap.
ppedrot
2013-11-04
*
Update comments.
aspiwack
2013-11-02
*
Adds a tactic give_up.
aspiwack
2013-11-02
*
Adds a shelve tactic.
aspiwack
2013-11-02
*
The tactic [admit] exits with the "unsafe" status.
aspiwack
2013-11-02
*
Getting rid of Goal.here, and all the related exceptions and combinators.
aspiwack
2013-11-02
*
Moving side effects into evar_map. There was no reason to keep another
ppedrot
2013-10-05
[next]