aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Expand)AuthorAge
* Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsGravatar Pierre-Marie Pédrot2018-07-03
|\
* \ Merge PR #7703: Add an option to force parameters to be uniformGravatar Matthieu Sozeau2018-07-02
|\ \
| | * hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
| |/ |/|
* | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points...Gravatar Emilio Jesus Gallego Arias2018-07-02
|\ \
| | * Add flag Uniform Inductive ParametersGravatar Jasper Hugunin2018-07-01
| | * Implement uniform parameters in ComInductiveGravatar Jasper Hugunin2018-07-01
* | | [api] Fix wrong deprecation warning (#7915)Gravatar Emilio Jesus Gallego Arias2018-07-01
| |/ |/|
* | Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \
* \ \ Merge PR #7759: Workaround to fix #7731 (printing not splitting line at break...Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \ \
| | | * Port g_vernac to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
| | | * Port g_proofs to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
| | | * Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Gravatar Pierre-Marie Pédrot2018-06-29
| |_|/ |/| |
| * | Workaround to fix #7731 (printing not splitting line at break hint).Gravatar Hugo Herbelin2018-06-29
| | * Fixes #7712 (an anomaly in reporting bad recursive notation format).Gravatar Hugo Herbelin2018-06-29
| |/
* | Merge PR #7080: Swapping Context and Constr and defining declarations on cons...Gravatar Maxime Dénès2018-06-29
|\ \
* | | Make Environ.globals abstract.Gravatar Gaëtan Gilbert2018-06-28
| |/ |/|
* | Merge PR #7866: Implementation of mutual records in the higher strataGravatar Maxime Dénès2018-06-28
|\ \
| | * Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
| |/ |/|
* | Merge PR #7863: Remove Sorts.contentsGravatar Pierre-Marie Pédrot2018-06-27
|\ \
* \ \ 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
|\ \ \ \
| | | * | Remove Sorts.contentsGravatar Gaëtan Gilbert2018-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
|\ \ \ \ \
| | | | | * Handle mutual record at the vernac level.Gravatar Pierre-Marie Pédrot2018-06-24
| |_|_|_|/ |/| | | |
* | | | | 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
| |_|_|_|_|_|/ / |/| | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 20:12:51 +0000