index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
vernac
Commit message (
Expand
)
Author
Age
...
*
|
|
|
|
|
|
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 #7260: Fix #6951: Unexpected error during scheme creation.
Maxime Dénès
2018-05-30
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #7558: [api] Make `vernac/` self-contained.
Maxime Dénès
2018-05-30
|
\
\
\
\
\
\
\
|
|
|
|
*
|
|
|
Fix #7113: Program Let Fixpoint in section causes anomaly
Gaëtan Gilbert
2018-05-30
|
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
Fix #6951: Unexpected error during scheme creation.
Pierre-Marie Pédrot
2018-05-29
|
|
/
/
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
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
|
|
*
|
|
|
|
[api] Make `vernac/` self-contained.
Emilio Jesus Gallego Arias
2018-05-27
|
|
*
|
|
|
|
[tactics] Turn boolean locality hint parameter into a named one.
Emilio Jesus Gallego Arias
2018-05-27
|
|
*
|
|
|
|
[api] [parsing] Move Egram* to `vernac/`
Emilio Jesus Gallego Arias
2018-05-27
|
|
/
/
/
/
/
*
/
/
/
/
/
Remove some occurrences of Evd.empty
Maxime Dénès
2018-05-25
|
/
/
/
/
/
|
|
|
*
/
An attempt to clarify error message for Arguments needing "rename" flag.
Hugo Herbelin
2018-05-25
|
|
_
|
/
/
|
/
|
|
|
*
|
|
|
Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...
Pierre-Marie Pédrot
2018-05-24
|
\
\
\
\
|
*
|
|
|
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
|
\
\
\
\
|
|
*
|
|
Fix an anomaly when calling Obligation 0 or Obligation -1.
Théo Zimmermann
2018-05-21
*
|
|
|
|
[ide] Remove special option `-ideslave`
Emilio Jesus Gallego Arias
2018-05-21
*
|
|
|
|
[stm] Make toplevels standalone executables.
Emilio Jesus Gallego Arias
2018-05-21
|
|
/
/
/
|
/
|
|
|
*
|
|
|
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
|
|
*
|
|
Remove unused argument to solve_constraints_system
Gaëtan Gilbert
2018-05-17
|
|
*
|
|
Move solve_constraint_system near its only use site (comInductive)
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
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge PR #7359: Reduce usage of evar_map references
Pierre-Marie Pédrot
2018-05-17
|
\
\
\
\
*
\
\
\
\
Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in `comDefiniti...
Pierre-Marie Pédrot
2018-05-17
|
\
\
\
\
\
|
|
*
|
|
|
Deprecate Typing.e_* functions
Gaëtan Gilbert
2018-05-14
*
|
|
|
|
|
Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).
Hugo Herbelin
2018-05-10
|
|
/
/
/
/
|
/
|
|
|
|
|
|
*
|
|
[api] Move universe syntax to `Glob_term`
Emilio Jesus Gallego Arias
2018-05-08
|
|
/
/
/
|
/
|
|
|
|
*
|
|
[vernac] taint two out-of-api `to_constr` use in `comDefinition`.
Emilio Jesus Gallego Arias
2018-05-07
|
/
/
/
*
|
|
Merge PR #6156: [api] Rename `global_reference` to `GlobRef.t` to follow kern...
Maxime Dénès
2018-05-06
|
\
\
\
|
*
|
|
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-05-04
*
|
|
|
Merge PR #7416: Fix #7415. Printing Width was not applied to error messages.
Emilio Jesus Gallego Arias
2018-05-04
|
\
\
\
\
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.
Pierre-Marie Pédrot
2018-05-04
|
\
\
\
\
|
|
*
|
|
Fix #7415. Printing Width was not applied to error messages.
Pierre Courtieu
2018-05-03
*
|
|
|
|
Making explicit that errors happen in one of five executation phases.
Hugo Herbelin
2018-05-02
|
|
/
/
/
|
/
|
|
|
*
|
|
|
[api] Move bullets and goals selectors to `proofs/`
Emilio Jesus Gallego Arias
2018-05-01
*
|
|
|
Merge PR #6935: Separate universe minimization and evar normalization functions
Pierre-Marie Pédrot
2018-04-30
|
\
\
\
\
*
\
\
\
\
Merge PR #6958: [lib] Move global options to their proper place.
Maxime Dénès
2018-04-30
|
\
\
\
\
\
|
|
|
*
|
|
[api] Move `hint_info_expr` to `Typeclasses`.
Emilio Jesus Gallego Arias
2018-04-26
|
|
_
|
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #7152: [api] Remove dependency of library on Vernacexpr.
Pierre-Marie Pédrot
2018-04-23
|
\
\
\
\
\
|
|
|
*
|
|
Deprecate mixing univ minimization and evm normalization functions.
Gaëtan Gilbert
2018-04-17
|
|
_
|
/
/
/
|
/
|
|
|
|
*
|
|
|
|
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
|
\
\
\
\
\
*
|
|
|
|
|
Fixing the 3 cases of a "Stream.Error" ended with two periods.
Hugo Herbelin
2018-04-12
|
|
|
|
|
*
Fixes #7192 (Print Assumptions does not enter implementation of submodules).
Hugo Herbelin
2018-04-07
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
*
|
|
[api] Remove dependency of library on Vernacexpr.
Emilio Jesus Gallego Arias
2018-04-06
|
|
/
/
/
|
/
|
|
|
[prev]
[next]