aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Expand)AuthorAge
* [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
* 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
* | | | [api] Move `opacity_flag` to `Proof_global`.Gravatar Emilio Jesus Gallego Arias2018-05-23
|/ / /
* | | Merge PR #7384: Split UniversesGravatar Pierre-Marie Pédrot2018-05-22
|\ \ \
| | * | Fix an anomaly when calling Obligation 0 or Obligation -1.Gravatar Théo Zimmermann2018-05-21
* | | | [ide] Remove special option `-ideslave`Gravatar Emilio Jesus Gallego Arias2018-05-21
* | | | [stm] Make toplevels standalone executables.Gravatar Emilio Jesus Gallego Arias2018-05-21
| |/ / |/| |
* | | Merge PR #6965: [api] Move universe syntax to `Glob_term`Gravatar Pierre-Marie Pédrot2018-05-18
|\ \ \
| | * | Split off Universes functions about substitutions and constraintsGravatar Gaëtan Gilbert2018-05-17
| | * | Remove unused argument to solve_constraints_systemGravatar Gaëtan Gilbert2018-05-17
| | * | Move solve_constraint_system near its only use site (comInductive)Gravatar Gaëtan Gilbert2018-05-17
| | * | Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
| | * | Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
| |/ / |/| |
* | | Merge PR #7359: Reduce usage of evar_map referencesGravatar Pierre-Marie Pédrot2018-05-17
|\ \ \
* \ \ \ Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in `comDefiniti...Gravatar Pierre-Marie Pédrot2018-05-17
|\ \ \ \
| | * | | Deprecate Typing.e_* functionsGravatar Gaëtan Gilbert2018-05-14
* | | | | Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Gravatar Hugo Herbelin2018-05-10
| |/ / / |/| | |
| | * | [api] Move universe syntax to `Glob_term`Gravatar Emilio Jesus Gallego Arias2018-05-08
| |/ / |/| |
| * | [vernac] taint two out-of-api `to_constr` use in `comDefinition`.Gravatar Emilio Jesus Gallego Arias2018-05-07
|/ /