aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2018-05-24Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...Pierre-Marie Pédrot
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-23[api] Move `Vernacexpr` to parsing.Emilio Jesus Gallego Arias
2018-05-23[api] Move `opacity_flag` to `Proof_global`.Emilio Jesus Gallego Arias
2018-05-22Merge PR #7384: Split UniversesPierre-Marie Pédrot
2018-05-21[ide] Remove special option `-ideslave`Emilio Jesus Gallego Arias
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
2018-05-18Merge PR #6965: [api] Move universe syntax to `Glob_term`Pierre-Marie Pédrot
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-17Remove unused argument to solve_constraints_systemGaëtan Gilbert
2018-05-17Move solve_constraint_system near its only use site (comInductive)Gaëtan Gilbert
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
2018-05-17Merge PR #7359: Reduce usage of evar_map referencesPierre-Marie Pédrot
2018-05-17Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in `comDefiniti...Pierre-Marie Pédrot
2018-05-14Deprecate Typing.e_* functionsGaëtan Gilbert
2018-05-10Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Hugo Herbelin
2018-05-08[api] Move universe syntax to `Glob_term`Emilio Jesus Gallego Arias
2018-05-07[vernac] taint two out-of-api `to_constr` use in `comDefinition`.Emilio Jesus Gallego Arias
2018-05-06Merge PR #6156: [api] Rename `global_reference` to `GlobRef.t` to follow kern...Maxime Dénès
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-05-04Merge PR #7416: Fix #7415. Printing Width was not applied to error messages.Emilio Jesus Gallego Arias
2018-05-04Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.Pierre-Marie Pédrot
2018-05-03Fix #7415. Printing Width was not applied to error messages.Pierre Courtieu
2018-05-02Making explicit that errors happen in one of five executation phases.Hugo Herbelin
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
2018-04-30Merge PR #6935: Separate universe minimization and evar normalization functionsPierre-Marie Pédrot
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 10:23:50 +0000