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
...
*
Goal: remove most of the API (make [Goal.goal] concrete).
Arnaud Spiwack
2014-10-16
*
Make [Goal.goal] be exactly [Evar.t].
Arnaud Spiwack
2014-10-16
*
Goal: remove dead code.
Arnaud Spiwack
2014-10-16
*
Expose Proofview.Refine.with_type in the API.
Arnaud Spiwack
2014-10-16
*
Proofview.Refine: remove the handle type, and simplify the API.
Arnaud Spiwack
2014-10-16
*
Move the handling of the principal evar from refine to evd.
Arnaud Spiwack
2014-10-16
*
Move the handling a new evars from the [Proofview.Refine] module to [Evd].
Arnaud Spiwack
2014-10-16
*
Proofview.Refine: delay the marking of new evars as goals from [new_evar] to ...
Arnaud Spiwack
2014-10-16
*
Proofview: small optimisation/simplification.
Arnaud Spiwack
2014-10-16
*
Add support for deactivating type class inference from induction/destruct.
Hugo Herbelin
2014-10-13
*
Adding a tactic which fails if one of the goals under focus is dependent in a...
Hugo Herbelin
2014-10-13
*
Naming main goal "Main"
Hugo Herbelin
2014-10-13
*
Added support for having one subgoal inheriting the name of its father in Ref...
Hugo Herbelin
2014-10-09
*
Removing Convert_concl and Convert_hyp from Logic.
Hugo Herbelin
2014-10-09
*
A version of convert_concl and convert_hyp in new proof engine.
Hugo Herbelin
2014-10-09
*
Make tclEFFECTS also update the env in the proof monad
Enrico Tassi
2014-10-06
*
A few Global.env removed.
Hugo Herbelin
2014-10-04
*
Factored out IDE goal structure.
Carst Tankink
2014-10-01
*
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-30
*
Merging some functions from evarutil.ml/evd.ml.
Hugo Herbelin
2014-09-29
*
Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.
Pierre-Marie Pédrot
2014-09-27
*
Adding a tclNEWGOALS primitive.
Pierre-Marie Pédrot
2014-09-26
*
Fixing strange evarmap leak in goals.
Pierre-Marie Pédrot
2014-09-18
*
Be more conservative and keep the use of eq_constr in pretyping/ functions.
Matthieu Sozeau
2014-09-17
*
Fix bug #3593, making constr_eq and progress work up to
Matthieu Sozeau
2014-09-17
*
Revert "While resolving typeclass evars in clenv, touch only the ones that ap...
Matthieu Sozeau
2014-09-17
*
While resolving typeclass evars in clenv, touch only the ones that appear in the
Matthieu Sozeau
2014-09-17
*
Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].
Arnaud Spiwack
2014-09-15
*
While we don't have a clean alternative to Clenvtac, add a primitive
Matthieu Sozeau
2014-09-12
*
Add syntax [id]: to apply tactic to goal named id.
Hugo Herbelin
2014-09-12
*
Use evar name to print goal.
Hugo Herbelin
2014-09-12
*
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
No plural for only one non existing focused goal.
Hugo Herbelin
2014-09-12
*
Fix source of initial goal.
Hugo Herbelin
2014-09-12
*
A step towards better differentiating when w_unify is used for subterm
Hugo Herbelin
2014-09-10
*
Fixing localisation of tactic errors (my mistake in himsg.ml essentially).
Hugo Herbelin
2014-09-10
*
Display number of available goals in "incorrect number of goals" error message.
Arnaud Spiwack
2014-09-08
*
Add a tactic [revgoals] to reverse the list of focused goals.
Arnaud Spiwack
2014-09-08
*
Renaming goal-entering functions.
Pierre-Marie Pédrot
2014-09-06
*
Removing the old implementation of clear_body.
Pierre-Marie Pédrot
2014-09-05
*
At last a working clearbody!
Pierre-Marie Pédrot
2014-09-05
*
Only using filtered hyps in Goal.enter.
Pierre-Marie Pédrot
2014-09-04
*
Ensuring the invariant that hypotheses and named context of the environment of
Pierre-Marie Pédrot
2014-09-04
*
Revert the two previous commits. I was testing in the wrong branch.
Pierre-Marie Pédrot
2014-09-04
*
Removing the old implementation of clear_body.
Pierre-Marie Pédrot
2014-09-04
*
Fix: shelve_unifiable did not work modulo evar instantiation.
Arnaud Spiwack
2014-09-04
*
Proofview refiner is now type-safe by default.
Pierre-Marie Pédrot
2014-09-04
*
Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.
Pierre-Marie Pédrot
2014-09-04
*
Using goal-tactics to interpret arguments to idtac.
Pierre-Marie Pédrot
2014-09-04
[prev]
[next]