aboutsummaryrefslogtreecommitdiff
path: root/user-contrib/Ltac2/tac2entries.ml
AgeCommit message (Expand)Author
2021-04-23Provide a reinit data for Ltac2 notations with entry level 4.Pierre-Marie Pédrot
2021-04-17Properly pass the Ltac2 notation level to the gramlib API.Pierre-Marie Pédrot
2021-04-08Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular.Pierre-Marie Pédrot
2021-03-25Fix the redeclaration check for Ltac2 entry points.Pierre-Marie Pédrot
2021-03-24Merge PR #13973: Factorize goal selector handlingPierre-Marie Pédrot
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and notat...Michael Soegtrop
2021-03-22Factorize goal selector handlingGaëtan Gilbert
2021-03-18Implement ! goal selector for Ltac2.Pierre-Marie Pédrot
2021-03-10Allow to register deprecation status in Ltac2 term and notation declarations.Pierre-Marie Pédrot
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-10-27Rename tac2type -> ltac2_type,Jim Fehrle
2020-10-26Ltac2: use ComTactic infrastructureGaëtan Gilbert
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
2020-05-11Allow to rebind the old value of a mutable Ltac2 entry.Pierre-Marie Pédrot
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-13pass filters aroundGaëtan Gilbert
2020-03-25[pcoq] Inline the exported Gramlib interface instead of exposing it as GEmilio Jesus Gallego Arias
2020-03-25[parsing] Remove extend AST in favor of gramlib constructorsEmilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar rules private.Emilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar extension type private.Emilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-03[exn] Keep information from multiple extra exn handlersEmilio Jesus Gallego Arias
2020-02-25Merge PR #11498: [exn] Forbid raising in exn printers, make them return Pp.t ...Pierre-Marie Pédrot
2020-02-24[exn] Forbid raising in exn printers, make them return Pp.t optionEmilio Jesus Gallego Arias
2020-02-21[parsing] Track need to reinit by typingEmilio Jesus Gallego Arias
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2019-11-04Prevent double definition of Ltac2 constructors inside a module; Fix #11046Kenji Maillard
2019-11-04Prevent redefinition of Ltac2 types; fix #10097Kenji Maillard
2019-11-01enforcing Ltac2 cosntructors name are uppercase in open typesKenji Maillard
2019-10-31enforcing Ltac2 constructor name are uppercasedKenji Maillard
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.Pierre-Marie Pédrot
2019-07-11[proof] Minor cleanup in proof.mlEmilio Jesus Gallego Arias
2019-07-07[error] Remove special error printing pre-processingEmilio Jesus Gallego Arias
2019-06-17Update headers of files that were stuck on older headers.Théo Zimmermann
2019-06-09[proof] Uniformize Proof_global APIEmilio Jesus Gallego Arias
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-05-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:22:02 +0000