index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
evd.ml
Commit message (
Expand
)
Author
Age
*
Performance fix for destruct.
Pierre-Marie Pédrot
2015-11-17
*
Univs: update refman, better printers for universe contexts.
Matthieu Sozeau
2015-11-04
*
Fix bug #4151: discrepancy between exact and eexact/eassumption.
Matthieu Sozeau
2015-11-02
*
Handle side-effects of Vernacular commands inside proofs better, so that
Matthieu Sozeau
2015-10-29
*
Univs: local names handling.
Matthieu Sozeau
2015-10-28
*
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-10-28
*
Fixing evarmap implementation.
Pierre-Marie Pédrot
2015-10-14
*
Univs: fix bug #3807
Matthieu Sozeau
2015-10-08
*
Univs: fix FingerTree contrib.
Matthieu Sozeau
2015-10-07
*
Univs: add Strict Universe Declaration option (on by default)
Matthieu Sozeau
2015-10-07
*
Fix bug #4354: interpret hints in the right env and sigma.
Matthieu Sozeau
2015-10-06
*
Univs: fix after rebase (from_ctx/from_env)
Matthieu Sozeau
2015-10-02
*
Univs (evd): deal with global universes and sideff
Matthieu Sozeau
2015-10-02
*
Forcing i > Set for global universes (incomplete)
Matthieu Sozeau
2015-10-02
*
Univs: force all universes to be >= Set.
Matthieu Sozeau
2015-10-02
*
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
*
Fixing loss of extra data in Evd.
Pierre-Marie Pédrot
2015-09-27
*
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
Fix bug #4254 with the help of J.H. Jourdan
Matthieu Sozeau
2015-06-26
*
Fixup for 866c41b
Enrico Tassi
2015-05-28
*
Fix bug #4159
Matthieu Sozeau
2015-05-27
*
Adding an extensible global state to evarmaps.
Pierre-Marie Pédrot
2015-05-19
*
Tactical `progress` compares term up to potentially equalisable universes.
Arnaud Spiwack
2015-04-22
*
Add function to fix the non-substituted universe variables of an evar_map.
Matthieu Sozeau
2015-03-17
*
[Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...
Arnaud Spiwack
2015-02-24
*
Compensating 6fd763431 on postponing subtyping evar-evar problems.
Hugo Herbelin
2015-02-23
*
Continuing experimentation on what part of the instance of an evar
Hugo Herbelin
2015-02-21
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
*
Update headers.
Maxime Dénès
2015-01-12
*
Fix merging of name maps in union of universe contexts.
Matthieu Sozeau
2014-12-14
*
Tentatively more informative report of failure when inferring
Hugo Herbelin
2014-12-11
*
Improved tracking of the origin of evars.
Hugo Herbelin
2014-12-07
*
More consistent printing of evars in evar_map debugging printer.
Hugo Herbelin
2014-12-05
*
New approach to deal with evar-evar unification problems in different
Hugo Herbelin
2014-12-04
*
Option -type-in-type continued (deactivate test for inferred sort of
Hugo Herbelin
2014-11-19
*
new: Optimize Proof, Optimize Heap
Enrico Tassi
2014-11-09
*
Fixing a bug in change of subst_defined_metas in bcba6d1bc9f769da:
Hugo Herbelin
2014-11-08
*
Experimentally applying eager evar substitution at the same time as
Hugo Herbelin
2014-11-04
*
Removing dead code from Evd.
Pierre-Marie Pédrot
2014-10-27
*
Removing the Evd.diff function.
Pierre-Marie Pédrot
2014-10-27
*
Removing the Evd.merge function.
Pierre-Marie Pédrot
2014-10-27
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
Add more primitives to the [Monad.Make] arguments.
Arnaud Spiwack
2014-10-22
*
Dead code.
Hugo Herbelin
2014-10-21
*
Refine: proper scoping of the future goals.
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
*
Evd: a few comments to document the increasingly wide internal [evar_map] type.
Arnaud Spiwack
2014-10-16
*
Evd: remove/update obsolete comments.
Arnaud Spiwack
2014-10-16
*
Adding a tactic which fails if one of the goals under focus is dependent in a...
Hugo Herbelin
2014-10-13
[next]