aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2018-07-03[vernac] mk_atts: an atts record with default valuesVincent Laporte
2018-07-03[vernac] attribute_of_flagsVincent Laporte
2018-07-03Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsPierre-Marie Pédrot
2018-07-02Merge PR #7703: Add an option to force parameters to be uniformMatthieu Sozeau
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-07-02Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points...Emilio Jesus Gallego Arias
2018-07-01Add flag Uniform Inductive ParametersJasper Hugunin
2018-07-01Implement uniform parameters in ComInductiveJasper Hugunin
2018-07-01[api] Fix wrong deprecation warning (#7915)Emilio Jesus Gallego Arias
2018-07-01Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...Emilio Jesus Gallego Arias
2018-07-01Merge PR #7759: Workaround to fix #7731 (printing not splitting line at break...Emilio Jesus Gallego Arias
2018-06-29Port g_vernac to the homebrew GEXTEND parser.Pierre-Marie Pédrot
2018-06-29Port g_proofs to the homebrew GEXTEND parser.Pierre-Marie Pédrot
2018-06-29Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Pierre-Marie Pédrot
2018-06-29Workaround to fix #7731 (printing not splitting line at break hint).Hugo Herbelin
2018-06-29Fixes #7712 (an anomaly in reporting bad recursive notation format).Hugo Herbelin
2018-06-29Merge PR #7080: Swapping Context and Constr and defining declarations on cons...Maxime Dénès
2018-06-28Make Environ.globals abstract.Gaëtan Gilbert
2018-06-28Merge PR #7866: Implementation of mutual records in the higher strataMaxime Dénès
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-27Merge PR #7863: Remove Sorts.contentsPierre-Marie Pédrot
2018-06-26Merge PR #7906: universes_of_constr don't include universes of monomorphic co...Pierre-Marie Pédrot
2018-06-26Merge PR #7775: Fix handling of universe context for expanded program obligat...Maxime Dénès
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-26universes_of_constr don't include universes of monomorphic constantsGaëtan Gilbert
2018-06-25Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...Matthieu Sozeau
2018-06-25Merge PR #7559: Existing Class noop when already a class + warning.Matthieu Sozeau
2018-06-24Further cleaning of the side-effect API.Pierre-Marie Pédrot
2018-06-24Share the role type between the implementations of side-effects.Pierre-Marie Pédrot
2018-06-24Handle mutual record at the vernac level.Pierre-Marie Pédrot
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-22Fix handling of universe context for expanded program obligations.Matthieu Sozeau
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
2018-06-19Merge PR #7797: Remove reference name type.Enrico Tassi
2018-06-19Merge PR #7801: [vernac] Add option to force building really mutual induction...Enrico Tassi
2018-06-18Remove reference name type.Maxime Dénès
2018-06-14Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...Pierre-Marie Pédrot
2018-06-13[vernac] Add option to force building really mutual induction schemesMatthieu Sozeau
2018-06-12[api] Add compatiblity Misctypes module.Emilio Jesus Gallego Arias
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-06-08Existing Class noop when already a class + warning.Gaëtan Gilbert
2018-06-07Merge PR #6874: [econstr] Some minor tweaksPierre-Marie Pédrot
2018-06-05Merge PR #7453: Refuse to parse empty [Context] command.Matthieu Sozeau
2018-06-04Merge PR #7315: An attempt to clarify error message for Arguments needing "re...Maxime Dénès
2018-06-04Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Pierre-Marie Pédrot
2018-06-04[econstr] Remove some Unsafe.to_constr use.Emilio Jesus Gallego Arias
2018-06-04[vernac] Switch back `auto_ind_decl` to Constr.Emilio Jesus Gallego Arias
2018-06-04Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 07:35:49 +0000