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
...
|
|
*
|
|
|
|
|
|
Stop using Universes.subst(_opt)_univs_constr
Gaëtan Gilbert
2018-05-17
|
|
*
|
|
|
|
|
|
Make set minimization option internal to Universes
Gaëtan Gilbert
2018-05-17
|
|
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
Merge PR #7359: Reduce usage of evar_map references
Pierre-Marie Pédrot
2018-05-17
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #7213: Do not compute constr matching context if not used.
Matthieu Sozeau
2018-05-15
|
\
\
\
\
\
\
\
\
\
|
|
*
|
|
|
|
|
|
|
Use evd_combX in Cases.
Gaëtan Gilbert
2018-05-14
|
|
*
|
|
|
|
|
|
|
Typing implementation doesn't use evdref.
Gaëtan Gilbert
2018-05-14
|
|
*
|
|
|
|
|
|
|
Deprecate Typing.e_* functions
Gaëtan Gilbert
2018-05-14
|
|
*
|
|
|
|
|
|
|
Typing: define functional alternatives to e_* functions
Gaëtan Gilbert
2018-05-14
|
|
*
|
|
|
|
|
|
|
set_solve_evars doesn't use an evar_map ref
Gaëtan Gilbert
2018-05-11
|
|
*
|
|
|
|
|
|
|
Deprecate Evarconv.e_conv,e_cumul
Gaëtan Gilbert
2018-05-11
|
|
*
|
|
|
|
|
|
|
Deprecate most evarutil evdref functions
Gaëtan Gilbert
2018-05-11
|
|
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
[api] Move universe syntax to `Glob_term`
Emilio Jesus Gallego Arias
2018-05-08
|
|
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-05-04
*
|
|
|
|
|
|
|
Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.
Pierre-Marie Pédrot
2018-05-04
|
\
\
\
\
\
\
\
\
*
|
|
|
|
|
|
|
|
[api] Move bullets and goals selectors to `proofs/`
Emilio Jesus Gallego Arias
2018-05-01
*
|
|
|
|
|
|
|
|
Strict focusing using Default Goal Selector.
Gaëtan Gilbert
2018-04-29
*
|
|
|
|
|
|
|
|
Merge PR #7358: Fix #7356: missing lift when interpreting default instances o...
Enrico Tassi
2018-04-27
|
\
\
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
|
|
Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.
Hugo Herbelin
2018-04-26
|
|
*
|
|
|
|
|
|
|
[api] Move `hint_info_expr` to `Typeclasses`.
Emilio Jesus Gallego Arias
2018-04-26
|
|
/
/
/
/
/
/
/
/
*
/
/
/
/
/
/
/
/
Always print explanation for univ inconsistency, rm Flags.univ_print
Gaëtan Gilbert
2018-04-26
|
/
/
/
/
/
/
/
/
*
|
|
|
|
|
|
|
[api] Relocate `intf` modules according to dependency-order.
Emilio Jesus Gallego Arias
2018-04-23
*
|
|
|
|
|
|
|
Evar maps contain econstrs.
Gaëtan Gilbert
2018-04-13
*
|
|
|
|
|
|
|
Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contain...
Pierre-Marie Pédrot
2018-04-13
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #6972: [api] Deprecate a couple of aliases that we missed.
Maxime Dénès
2018-04-12
|
\
\
\
\
\
\
\
\
\
|
|
|
|
*
|
|
|
|
|
Replace uses of Termops.dependent by more specific functions.
Pierre-Marie Pédrot
2018-04-10
|
|
_
|
_
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
Do not compute constr matching context if not used.
Pierre-Marie Pédrot
2018-04-10
|
|
_
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
Fixes #7195 (missing freshness condition in Ltac pattern-matching names).
Hugo Herbelin
2018-04-08
|
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
Fix #5539: algebraic universe produced by cases.
Gaëtan Gilbert
2018-04-06
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)
Pierre-Marie Pédrot
2018-04-01
|
\
\
\
\
\
\
|
|
|
*
|
|
|
[econstr] Forbid calling `to_constr` in open terms.
Emilio Jesus Gallego Arias
2018-03-31
|
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
*
|
|
|
|
Supporting fix/cofix in Ltac pattern-matching (wish #7092).
Hugo Herbelin
2018-03-28
|
*
|
|
|
|
Patterns: Accepting patterns in PFix and PCofix and not only constr.
Hugo Herbelin
2018-03-28
|
*
|
|
|
|
Detyping: Adding a variant of share_names for patterns.
Hugo Herbelin
2018-03-28
|
*
|
|
|
|
Detyping: Making detype_fix/detype_cofix polymorphic combinator (step 1).
Hugo Herbelin
2018-03-28
|
*
|
|
|
|
Patternops: renaming an internal function to more closely match its effect.
Hugo Herbelin
2018-03-28
|
*
|
|
|
|
Glob_ops: cosmetic renaming to reflect the type of objects.
Hugo Herbelin
2018-03-28
|
|
|
|
*
|
Getting rid of some false "collision between bound variable names" warnings.
Hugo Herbelin
2018-03-28
|
|
|
_
|
/
/
|
|
/
|
|
|
|
|
*
|
|
[api] Deprecate a couple of aliases that we missed.
Emilio Jesus Gallego Arias
2018-03-28
|
|
/
/
/
|
/
|
|
|
|
|
|
*
Fixing #5547 (typability of return predicate in nested pattern-matching).
Hugo Herbelin
2018-03-27
|
|
|
*
Fixing #5500 (missing test in return clause of match leading to anomaly).
Hugo Herbelin
2018-03-27
|
|
|
/
|
|
/
|
|
|
*
Fixes #7011 (Fix/CoFix were not considered in tactic unification).
Hugo Herbelin
2018-03-26
|
|
/
*
/
Slightly refining some error messages about unresolvable evars.
Hugo Herbelin
2018-03-24
|
/
*
[located] Push inner locations in `reference` to a CAst.t node.
Emilio Jesus Gallego Arias
2018-03-09
*
[located] More work towards using CAst.t
Emilio Jesus Gallego Arias
2018-03-09
*
Merge PR #6775: Allow using cumulativity without forcing strict constraints.
Maxime Dénès
2018-03-09
|
\
*
\
Merge PR #6806: Adding missing unification constraint noticed by @skyskimmer
Maxime Dénès
2018-03-09
|
\
\
*
\
\
Merge PR #6769: Split closure cache and remove whd_both
Maxime Dénès
2018-03-09
|
\
\
\
|
|
|
*
Delayed weak constraints for cumulative inductive types.
Gaëtan Gilbert
2018-03-09
|
|
|
*
Statically enforce that ULub is only between levels.
Gaëtan Gilbert
2018-03-09
|
|
|
*
Option for messing with inference of irrelevant constraints
Gaëtan Gilbert
2018-03-09
[prev]
[next]
Gaëtan Gilbert
Pierre-Marie Pédrot
Matthieu Sozeau
Emilio Jesus Gallego Arias
Enrico Tassi
Hugo Herbelin
Maxime Dénès