aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Expand)AuthorAge
* Merge PR #7906: universes_of_constr don't include universes of monomorphic co...Gravatar Pierre-Marie Pédrot2018-06-26
|\
* \ Merge PR #7775: Fix handling of universe context for expanded program obligat...Gravatar Maxime Dénès2018-06-26
|\ \
| | * universes_of_constr don't include universes of monomorphic constantsGravatar Gaëtan Gilbert2018-06-26
* | | Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...Gravatar Matthieu Sozeau2018-06-25
|\ \ \
* \ \ \ Merge PR #7559: Existing Class noop when already a class + warning.Gravatar Matthieu Sozeau2018-06-25
|\ \ \ \
* | | | | Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
| |_|_|/ |/| | |
| | | * Fix handling of universe context for expanded program obligations.Gravatar Matthieu Sozeau2018-06-22
| |_|/ |/| |
| | * Remove hack skipping comparison of algebraic universes in subtyping.Gravatar Gaëtan Gilbert2018-06-22
| |/ |/|
* | Merge PR #7797: Remove reference name type.Gravatar Enrico Tassi2018-06-19
|\ \
* \ \ Merge PR #7801: [vernac] Add option to force building really mutual induction...Gravatar Enrico Tassi2018-06-19
|\ \ \
| | * | Remove reference name type.Gravatar Maxime Dénès2018-06-18
| |/ / |/| |
* | | Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...Gravatar Pierre-Marie Pédrot2018-06-14
|\ \ \
| | * | [vernac] Add option to force building really mutual induction schemesGravatar Matthieu Sozeau2018-06-13
| |/ / |/| |
* | | [api] Add compatiblity Misctypes module.Gravatar Emilio Jesus Gallego Arias2018-06-12
* | | [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
* | | [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* | | [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | * Existing Class noop when already a class + warning.Gravatar Gaëtan Gilbert2018-06-08
| |/ |/|
* | Merge PR #6874: [econstr] Some minor tweaksGravatar Pierre-Marie Pédrot2018-06-07
|\ \
* \ \ Merge PR #7453: Refuse to parse empty [Context] command.Gravatar Matthieu Sozeau2018-06-05
|\ \ \
* \ \ \ Merge PR #7315: An attempt to clarify error message for Arguments needing "re...Gravatar Maxime Dénès2018-06-04
|\ \ \ \
* \ \ \ \ Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Gravatar Pierre-Marie Pédrot2018-06-04
|\ \ \ \ \
| | | | * | [econstr] Remove some Unsafe.to_constr use.Gravatar Emilio Jesus Gallego Arias2018-06-04
| | | | * | [vernac] Switch back `auto_ind_decl` to Constr.Gravatar Emilio Jesus Gallego Arias2018-06-04
| |_|_|/ / |/| | | |
* | | | | Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomalyGravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7349: Fix an anomaly when calling Obligation 0 or Obligation -1.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7657: Fix a couple typos in deprecation messagesGravatar Pierre-Marie Pédrot2018-06-04
|\ \ \ \ \ \ \ \
| | | | | | | * | Refuse to parse empty [Context] command.Gravatar Gaëtan Gilbert2018-06-02
| |_|_|_|_|_|/ / |/| | | | | | |
| * | | | | | | Fix a couple typos in deprecation messagesGravatar Armaël Guéneau2018-05-31
| | | | | * | | Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Gravatar Armaël Guéneau2018-05-31
| | |_|_|/ / / | |/| | | | |
* | | | | | | [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
* | | | | | | [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
|/ / / / / /
* | | | | | Merge PR #6969: [api] Remove functions deprecated in 8.8Gravatar Maxime Dénès2018-05-31
|\ \ \ \ \ \
* | | | | | | Move interning the [hint_pattern] outside the Typeclasses hooks.Gravatar Gaëtan Gilbert2018-05-30
| * | | | | | [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
|/ / / / / /
* | | | | | Merge PR #7260: Fix #6951: Unexpected error during scheme creation.Gravatar Maxime Dénès2018-05-30
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7558: [api] Make `vernac/` self-contained.Gravatar Maxime Dénès2018-05-30
|\ \ \ \ \ \ \
| | | | * | | | Fix #7113: Program Let Fixpoint in section causes anomalyGravatar Gaëtan Gilbert2018-05-30
| |_|_|/ / / / |/| | | | | |
| | * | | | | Fix #6951: Unexpected error during scheme creation.Gravatar Pierre-Marie Pédrot2018-05-29
| |/ / / / / |/| | | | |
* | | | | | Merge PR #7521: Fix soundness bug with VM/native and cofixpointsGravatar Pierre-Marie Pédrot2018-05-28
|\ \ \ \ \ \
| * | | | | | Unify pre_env and envGravatar Maxime Dénès2018-05-28
| | * | | | | [api] Make `vernac/` self-contained.Gravatar Emilio Jesus Gallego Arias2018-05-27
| | * | | | | [tactics] Turn boolean locality hint parameter into a named one.Gravatar Emilio Jesus Gallego Arias2018-05-27
| | * | | | | [api] [parsing] Move Egram* to `vernac/`Gravatar Emilio Jesus Gallego Arias2018-05-27
| |/ / / / /
* / / / / / Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
|/ / / / /
| | | * / An attempt to clarify error message for Arguments needing "rename" flag.Gravatar Hugo Herbelin2018-05-25
| |_|/ / |/| | |
* | | | Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...Gravatar Pierre-Marie Pédrot2018-05-24
|\ \ \ \
| * | | | Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
* | | | | [api] Move `Vernacexpr` to parsing.Gravatar Emilio Jesus Gallego Arias2018-05-23