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
*
Stronger invariants in unification signature.
Pierre-Marie Pédrot
2018-06-04
*
Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ta...
Matthieu Sozeau
2018-06-04
|
\
*
\
Merge PR #7216: Replace uses of Termops.dependent by more specific functions.
Matthieu Sozeau
2018-06-04
|
\
\
*
\
\
Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".
Matthieu Sozeau
2018-06-04
|
\
\
\
*
\
\
\
Merge PR #7234: Reduce circular dependency constants <-> projections
Maxime Dénès
2018-06-01
|
\
\
\
\
*
|
|
|
|
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
2018-05-31
*
|
|
|
|
Merge PR #6969: [api] Remove functions deprecated in 8.8
Maxime Dénès
2018-05-31
|
\
\
\
\
\
|
|
*
|
|
|
Reduce circular dependency constants <-> projections
Gaëtan Gilbert
2018-05-31
*
|
|
|
|
|
Move interning the [hint_pattern] outside the Typeclasses hooks.
Gaëtan Gilbert
2018-05-30
|
|
/
/
/
/
|
/
|
|
|
|
|
*
|
|
|
[api] Remove deprecated object from `Term`
Emilio Jesus Gallego Arias
2018-05-30
|
/
/
/
/
*
|
|
|
Merge PR #7521: Fix soundness bug with VM/native and cofixpoints
Pierre-Marie Pédrot
2018-05-28
|
\
\
\
\
|
*
|
|
|
Unify pre_env and env
Maxime Dénès
2018-05-28
*
|
|
|
|
Remove some occurrences of Evd.empty
Maxime Dénès
2018-05-25
|
/
/
/
/
*
|
|
|
Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...
Pierre-Marie Pédrot
2018-05-24
|
\
\
\
\
|
|
*
|
|
Fix #7586: Anomaly "Uncaught exception Not_found".
Pierre-Marie Pédrot
2018-05-23
|
*
|
|
|
Moving Option.smart_map to Option.Smart.map.
Hugo Herbelin
2018-05-23
|
*
|
|
|
Collecting List.smart_* functions into a module List.Smart.
Hugo Herbelin
2018-05-23
|
*
|
|
|
Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.
Hugo Herbelin
2018-05-23
|
*
|
|
|
Collecting Array.smart_* functions into a module Array.Smart.
Hugo Herbelin
2018-05-23
|
|
/
/
/
*
|
|
|
[api] Move `Vernacexpr` to parsing.
Emilio Jesus Gallego Arias
2018-05-23
*
|
|
|
[api] Move `opacity_flag` to `Proof_global`.
Emilio Jesus Gallego Arias
2018-05-23
|
/
/
/
*
|
|
Merge PR #7384: Split Universes
Pierre-Marie Pédrot
2018-05-22
|
\
\
\
*
\
\
\
Merge PR #6965: [api] Move universe syntax to `Glob_term`
Pierre-Marie Pédrot
2018-05-18
|
\
\
\
\
|
|
*
|
|
Split off Universes functions about substitutions and constraints
Gaëtan Gilbert
2018-05-17
|
|
*
|
|
Split off Universes functions dealing with generating new universes.
Gaëtan Gilbert
2018-05-17
|
|
*
|
|
Split off Universes functions dealing with names.
Gaëtan Gilbert
2018-05-17
|
|
*
|
|
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
|
\
\
\
\
\
[next]