aboutsummaryrefslogtreecommitdiff
path: root/printing/ppvernac.ml
AgeCommit message (Expand)Author
2018-05-27[api] [parsing] Move Egram* to `vernac/`Emilio Jesus Gallego Arias
2018-05-23[api] Move `opacity_flag` to `Proof_global`.Emilio Jesus Gallego Arias
2018-05-04Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.Pierre-Marie Pédrot
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
2018-04-26[api] Move `hint_info_expr` to `Typeclasses`.Emilio Jesus Gallego Arias
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-01[stm] Move VernacBacktrack to the toplevel.Emilio Jesus Gallego Arias
2018-03-30Remove deprecated commands Arguments Scope and Implicit ArgumentsJasper Hugunin
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] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-09Implement the Export Set/Unset feature.Pierre-Marie Pédrot
2018-03-07Merge PR #6790: Allow universe declarations for [with Definition].Maxime Dénès
2018-03-05Allow universe declarations for [with Definition].Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-20Change default for notations with variables bound to both terms and binders.Hugo Herbelin
2018-02-20Notations: Adding modifiers to tell which kind of binder a constr can parse.Hugo Herbelin
2018-02-20Notations: A step in cleaning constr_entry_key.Hugo Herbelin
2018-02-20Adding support for parsing subterms of a notation as "pattern".Hugo Herbelin
2018-02-20Introducing an intermediary type "constr_prod_entry_key" for grammar producti...Hugo Herbelin
2018-02-01[vernac] Mutual theorems (VernacStartTheoremProof) always have namesVincent Laporte
2018-02-01[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionVincent Laporte
2018-01-22[printing] Remove duplicate definitions of pr_lident and pr_lnameVincent Laporte
2018-01-16Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprMaxime Dénès
2018-01-08[vernac] vernac_expr no longer recursiveVincent Laporte
2018-01-05Brackets support single numbered goal selectors.Théo Zimmermann
2017-12-23[flags] Move global time flag into an attribute.Emilio Jesus Gallego Arias
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
2017-11-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès
2017-11-25Allow local universe renaming in Print.Gaëtan Gilbert
2017-11-21[api] Miscellaneous consolidation + moves to engine.Emilio Jesus Gallego Arias
2017-11-04Finish removing Show Goal uidGaëtan Gilbert
2017-10-10Parse [Proof using Type] without translating Type to an id.Gaëtan Gilbert
2017-10-10[vernac] Remove "Proof using" hacks from parser.Emilio Jesus Gallego Arias
2017-10-03Implementing a generic mechanism for locating named objects from Coq side.Pierre-Marie Pédrot
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
2017-09-26Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Maxime Dénès
2017-09-19Remove STM vernaculars.Maxime Dénès
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-09-15Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...Maxime Dénès
2017-09-08Parse directly to Sorts.family when appropriate.Gaëtan Gilbert
2017-08-29[vernac] Store Infix Modifier in Vernac Notation.Pierre-Marie Pédrot
2017-07-31Improve errors for cumulativity when monomorphicAmin Timany
2017-07-19Merge PR #770: [proof] Move bullets to their own module.Maxime Dénès
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-21[vernac] Remove stale bool parameter from `VernacStartTheoremProof`Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:43:50 +0000