aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2018-04-30Merge PR #6958: [lib] Move global options to their proper place.Maxime Dénès
2018-04-26[api] Move `hint_info_expr` to `Typeclasses`.Emilio Jesus Gallego Arias
2018-04-23Merge PR #7152: [api] Remove dependency of library on Vernacexpr.Pierre-Marie Pédrot
2018-04-17Deprecate mixing univ minimization and evm normalization functions.Gaëtan Gilbert
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-04-13Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contain...Pierre-Marie Pédrot
2018-04-12Fixing the 3 cases of a "Stream.Error" ended with two periods.Hugo Herbelin
2018-04-07Fixes #7192 (Print Assumptions does not enter implementation of submodules).Hugo Herbelin
2018-04-06[api] Remove dependency of library on Vernacexpr.Emilio Jesus Gallego Arias
2018-04-05Merge PR #7016: Make parsing independent of the cumulativity flag.Enrico Tassi
2018-04-04Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.Enrico Tassi
2018-04-02[lib] Move global options to their proper place.Emilio Jesus Gallego Arias
2018-04-01[stm] Move VernacBacktrack to the toplevel.Emilio Jesus Gallego Arias
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-30Remove deprecated commands Arguments Scope and Implicit ArgumentsJasper Hugunin
2018-03-29Fix #6770: fixpoint loses locality info in proof mode.Gaëtan Gilbert
2018-03-27Merge PR #7062: Slightly refining some error messages about unresolvable evars.Pierre-Marie Pédrot
2018-03-24Slightly refining some error messages about unresolvable evars.Hugo Herbelin
2018-03-22bool option -> (VernacCumulative | VernacNonCumulative) optionGaëtan Gilbert
2018-03-21Make parsing independent of the cumulativity flag.Gaëtan Gilbert
2018-03-11[vernac] Move `Quit` and `Drop` to the toplevel layer.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-09Merge PR #6775: Allow using cumulativity without forcing strict constraints.Maxime Dénès
2018-03-09Merge PR #6923: Export optionsMaxime Dénès
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-09Implement the Export Set/Unset feature.Pierre-Marie Pédrot
2018-03-09Export the various option localities in the API.Pierre-Marie Pédrot
2018-03-09allow Prop as source for coercionscharguer
2018-03-09Merge PR #6941: [toplevel] Respect COQ_COLORS environment variableMaxime Dénès
2018-03-09Merge PR #6945: Fix error with univ binders on monomorphic records.Maxime Dénès
2018-03-09Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesMaxime Dénès
2018-03-08Merge PR #6816: Adding mention of shelved/given-up status in Show ExistentialsMaxime Dénès
2018-03-08Merge PR #6893: Cleanup UState API usageMaxime Dénès
2018-03-08Fix error with univ binders on monomorphic records.Gaëtan Gilbert
2018-03-08Fix SR breakage due to allowing fixpoints on non-rec valuesMatthieu Sozeau
2018-03-07[toplevel] Respect COQ_COLORS environment variableThomas Hebb
2018-03-07[vernac] Warn when using “Require” in a sectionVincent Laporte
2018-03-07Merge PR #6790: Allow universe declarations for [with Definition].Maxime Dénès
2018-03-07Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Maxime Dénès
2018-03-06Rename some universe minimizing "normalize" functions to "minimize"Gaëtan Gilbert
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-03-06Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...Maxime Dénès
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
2018-03-05Allow universe declarations for [with Definition].Gaëtan Gilbert
2018-03-05Sanitize universe declaration in Context (stop using a ref...)Gaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04[compat] Remove NOOP and alias deprecated options.Emilio Jesus Gallego Arias
2018-03-04Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Maxime Dénès
2018-03-04Merge PR #6676: [proofview] goals come with a stateMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 12:51:58 +0000