index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
Unifying betazeta_applist and prod_applist into a clearer interface.
Hugo Herbelin
2015-12-05
*
Moving extended_rel_vect/extended_rel_list to the kernel.
Hugo Herbelin
2015-12-05
*
Simplifying an instantiation function using subst_of_rel_context_instance.
Hugo Herbelin
2015-12-05
*
About building of substitutions from instances.
Hugo Herbelin
2015-12-05
*
An example in centralizing similar functions to a common place so that
Hugo Herbelin
2015-12-05
*
Removing dynamic inclusion of constrs in tactic AST.
Pierre-Marie Pédrot
2015-12-04
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-03
|
\
|
*
Add an option to deactivate compatibility printing of primitive
Matthieu Sozeau
2015-12-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
|
*
Univs: entirely disallow instantiation of polymorphic constants with
Matthieu Sozeau
2015-11-27
*
|
More efficient implementation of equality-up-to-universes in Universes.
Pierre-Marie Pédrot
2015-11-26
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-26
|
\
|
|
*
Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej).
Hugo Herbelin
2015-11-25
|
*
Fixing an old typo in Retyping, found by Matej.
Hugo Herbelin
2015-11-24
|
*
Fixing a vm_compute bug in the presence of let-ins among the
Hugo Herbelin
2015-11-22
|
*
Fixing a bug of adjust_subst_to_rel_context.
Hugo Herbelin
2015-11-22
|
*
Fixing kernel bug in typing match with let-ins in the arity.
Hugo Herbelin
2015-11-22
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
|
\
|
|
*
Fix bug #4433, removing hack on evars appearing in a pattern from a
Matthieu Sozeau
2015-11-19
|
*
Performance fix for destruct.
Pierre-Marie Pédrot
2015-11-17
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-15
|
\
|
|
*
Ensure that conversion is called on terms of the same type in
Matthieu Sozeau
2015-11-11
|
*
Fix bug #3998: when using typeclass resolution for conversion, allow
Matthieu Sozeau
2015-11-11
|
*
Fix bug #4293: ensure let-ins do not contain algebraic universes in
Matthieu Sozeau
2015-11-11
*
|
Revert "Fixing #1225: we now skip the canonically built binding contexts of"
Hugo Herbelin
2015-11-10
*
|
Fixing #1225: we now skip the canonically built binding contexts of
Hugo Herbelin
2015-11-10
*
|
Merge origin/v8.5 into trunk
Hugo Herbelin
2015-11-10
|
\
|
|
*
Pushing the backtrace in conversion anomalies.
Pierre-Marie Pédrot
2015-11-09
*
|
Experimenting printing the type of the defined term of a LetIn when
Hugo Herbelin
2015-11-07
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
*
Univs: missing checks in evarsolve with candidates and missing a
Matthieu Sozeau
2015-11-04
|
*
Univs: update refman, better printers for universe contexts.
Matthieu Sozeau
2015-11-04
|
*
Univs: compatibility with 8.4.
Matthieu Sozeau
2015-11-04
|
*
Fix bug #4151: discrepancy between exact and eexact/eassumption.
Matthieu Sozeau
2015-11-02
|
*
Refresh rigid universes as well, and in 8.4 compatibility mode,
Matthieu Sozeau
2015-11-02
|
*
Handle side-effects of Vernacular commands inside proofs better, so that
Matthieu Sozeau
2015-10-29
*
|
Removing some goal unsafeness in inductive schemes.
Pierre-Marie Pédrot
2015-10-29
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
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
|
*
Fix bug in native compiler with universe polymorphism.
Maxime Dénès
2015-10-28
|
*
Refine Gregory Malecha's patch on VM and universe polymorphism.
Maxime Dénès
2015-10-28
|
*
Conversion of polymorphic inductive types was incomplete in VM and native.
Maxime Dénès
2015-10-28
|
*
Adds support for the virtual machine to perform reduction of universe polymor...
Gregory Malecha
2015-10-28
|
*
Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"
Hugo Herbelin
2015-10-28
|
*
Documenting a bit more interpretation functions in passing.
Hugo Herbelin
2015-10-26
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-26
|
\
|
|
*
Fix lemma-overloading
Matthieu Sozeau
2015-10-20
|
*
Do occur-check w.r.t existential's types also when instantiating an evar.
Matthieu Sozeau
2015-10-19
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-19
|
\
|
[next]