aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacexpr.ml
AgeCommit message (Expand)Author
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-05-15Search: new clauses for searching head, conclusion, kind...Hugo Herbelin
2020-05-15Renaming search_about_item into search_item.Hugo Herbelin
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
2020-04-21[hints] Move and split Hint Declaration AST to vernacEmilio Jesus Gallego Arias
2020-04-20Move new iter_table function to Goptions.Théo Zimmermann
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-13Partial import inductive(..)Gaëtan Gilbert
2020-04-13syntax for import filtersGaëtan Gilbert
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-19Interpret the Export modifier of Set and Unset as an attribute.Théo Zimmermann
2020-03-19Make Cumulative, NonCumulative and Private attributes.Théo Zimmermann
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-04Experimenting using a record for decl_notation.Hugo Herbelin
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
2020-03-03[vernac] Use a record for VernacAddLoadPathEmilio Jesus Gallego Arias
2020-03-03[loadpath] Rework and simplify ML loadpath handlingEmilio Jesus Gallego Arias
2020-02-19Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]Emilio Jesus Gallego Arias
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
2020-02-15Reorganize type "production_level" along a more intuitive structure.Hugo Herbelin
2020-02-13Don't duplicate the inductive keyword for each block elt when parsingGaëtan Gilbert
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
2019-11-30Actually deprecate `SearchAbout`Maxime Dénès
2019-11-20make VernacArguments closer to user syntaxGaëtan Gilbert
2019-10-31Move Arguments implementation to its own file (from vernacentries)Gaëtan Gilbert
2019-08-23Merge PR #10665: [api] Move handling of variable implicit data to impargsGaëtan Gilbert
2019-08-20Merge PR #10291: Controlling typing flags with commands (no attribute)Gaëtan Gilbert
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-08-16Add [Print Typing Flags] command.SimonBoulier
2019-08-14[vernac] Refactor Vernacular Control Attributes into a listEmilio Jesus Gallego Arias
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
2019-07-23[vernacexpr] Remove duplicate fixpoint record.Emilio Jesus Gallego Arias
2019-07-23[vernacexpr] Refactor fixpoint AST.Emilio Jesus Gallego Arias
2019-07-01[api] Reduce declare_kinds even more.Emilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-24[api] [proof] Move `discharge` type to vernac_ast where it is used.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-28[elaboration] Bidirectionality hintsMaxime Dénès
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to p...Enrico Tassi
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
2019-05-10[Canonical structures] “not_canonical” annotation to field declarationsVincent Laporte
2019-05-07[Record] Une a record to gather field declaration attributesVincent Laporte
2019-04-25[vernac] [ast] Make location info an attribute of vernaculars.Emilio Jesus Gallego Arias
2019-04-17Merge PR #9876: Command-line setters for optionsEmilio Jesus Gallego Arias
2019-04-16[ast] [constrexpr] Make recursion_order_expr an AST node.Emilio Jesus Gallego Arias
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 19:15:50 +0000