index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
evarsolve.ml
Commit message (
Expand
)
Author
Age
*
Evar-normalizing functions now act on EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
Removing compatibility layers in Retyping
Pierre-Marie Pédrot
2017-02-14
*
Removing some return type compatibility layers in Termops.
Pierre-Marie Pédrot
2017-02-14
*
Reductionops now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
Eliminating parts of the right-hand side compatibility layer
Pierre-Marie Pédrot
2017-02-14
*
Hints API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Cleaning up opening of the EConstr module in pretyping folder.
Pierre-Marie Pédrot
2017-02-14
*
Unification API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Pretyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Evarsolve API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Retyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Reductionops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Termops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-24
|
\
|
*
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Matthieu Sozeau
2016-10-21
|
|
\
|
|
*
Revert "unification.ml: fix for bug #4763, unif regression"
Maxime Dénès
2016-10-21
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-18
|
\
|
|
|
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-18
|
|
\
|
|
|
*
Fixing to #3209 (Not_found due to an occur-check cycle).
Hugo Herbelin
2016-10-17
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-08
|
\
|
|
|
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-08
|
|
\
|
|
|
*
unification.ml: fix for bug #4763, unif regression
Matthieu Sozeau
2016-10-06
*
|
|
CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...
Matej Kosik
2016-08-30
*
|
|
CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function
Matej Kosik
2016-08-24
|
/
/
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-07-07
|
\
|
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2016-07-04
|
\
\
|
|
*
congruence: Restrict refreshing to Set
Matthieu Sozeau
2016-07-04
|
|
*
congruence/univs: properly refresh (fix #4609)
Matthieu Sozeau
2016-07-04
|
|
/
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
|
*
Refine fix for bug #4097, avoid proj expansion
Matthieu Sozeau
2016-06-27
*
|
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
\
*
|
|
Monotonizing the Evarutil module.
Pierre-Marie Pédrot
2016-02-15
|
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
/
/
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
merge
Matej Kosik
2016-01-11
|
\
\
|
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
|
|
/
*
/
Remove some unused functions.
Guillaume Melquiond
2016-01-02
|
/
*
Optimize occur_evar_upto_types, avoiding repeateadly looking into the
Matthieu Sozeau
2015-12-11
*
Fix bug #4293: ensure let-ins do not contain algebraic universes in
Matthieu Sozeau
2015-11-11
*
Univs: missing checks in evarsolve with candidates and missing a
Matthieu Sozeau
2015-11-04
*
Univs: compatibility with 8.4.
Matthieu Sozeau
2015-11-04
*
Refresh rigid universes as well, and in 8.4 compatibility mode,
Matthieu Sozeau
2015-11-02
*
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
*
Occur-check in evar_define was not strong enough.
Matthieu Sozeau
2015-10-14
*
Fix rechecking of applications: it can be given ill-typed terms. Fixes math-c...
Matthieu Sozeau
2015-10-12
[next]