aboutsummaryrefslogtreecommitdiff
path: root/user-contrib
AgeCommit message (Expand)Author
2020-03-01[parser] lk_int -> lk_natMaxime Dénès
2020-03-01Refactor lookaheads using DSLMaxime Dénès
2020-03-01Move lookahead combinators to PcoqMaxime Dénès
2020-02-25Merge PR #11498: [exn] Forbid raising in exn printers, make them return Pp.t ...Pierre-Marie Pédrot
2020-02-25Merge PR #11489: [exn] remove `raise` taking optional exception information a...Pierre-Marie Pédrot
2020-02-25Merge PR #11655: [parsing] Track need to reinit by typingPierre-Marie Pédrot
2020-02-24Merge PR #11560: Fix #11549: Ltac2 is incompatible with $.Tej Chajed
2020-02-24[exn] remove `raise` taking optional exception information argumentEmilio Jesus Gallego Arias
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-19Fix #11549: Ltac2 is incompatible with $.Pierre-Marie Pédrot
2020-02-19Fix #11552: Ltac2 breaks query commands during proofs.Pierre-Marie Pédrot
2020-02-14Annotate Ltac2 match macro variables with their type.Pierre-Marie Pédrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-09Merge PR #11518: Fix #11515: Ltac2 rewrite on wildcard.Gaëtan Gilbert
2020-02-08Resolve #10342 : [Ltac2] Add array libraryMichael Soegtrop
2020-02-04Fix #11515: Ltac2 rewrite on wildcard.Pierre-Marie Pédrot
2019-11-14Rename non-unique local nonterminalsJim Fehrle
2019-11-07Merge PR #11049: Prevent redefinition of Ltac2 types and constructors inside ...Pierre-Marie Pédrot
2019-11-06Swap parsing precedence of `::` and `,` ; Fix #10116Kenji Maillard
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-01Merge PR #9867: Add primitive floats (binary64 floating-point numbers)Maxime Dénès
2019-11-01enforcing Ltac2 cosntructors name are uppercase in open typesKenji Maillard
2019-11-01Add primitive floats to Ltac2Pierre Roux
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-10-31enforcing Ltac2 constructor name are uppercasedKenji Maillard
2019-10-29Fix #10615: Notation substitution for Ltac2 terms.Pierre-Marie Pédrot
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.Pierre-Marie Pédrot
2019-10-07chmod -x some filesJason Gross
2019-09-24Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kindGaëtan Gilbert
2019-08-06[parsing] unify checks for contiguity of tokens in Ltac2 and G_primEnrico Tassi
2019-07-29Fix #10088: Incompatibility with ssreflect's ampersand syntactic sugar.Pierre-Marie Pédrot
2019-07-29Tentatively providing a localization function to ad-hoc camlp5 parsers.Pierre-Marie Pédrot
2019-07-11[proof] Minor cleanup in proof.mlEmilio Jesus Gallego Arias
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-07[error] Remove special error printing pre-processingEmilio Jesus Gallego Arias
2019-06-25Give a functional type to Ltac1 quotations with a context.Pierre-Marie Pédrot
2019-06-25Adding the ability to transfer Ltac2 variables to Ltac1 quotations.Pierre-Marie Pédrot
2019-06-25Merge PR #10219: [Ltac2] Add util files for Bool, List, OptionPierre-Marie Pédrot
2019-06-19Removed backtracking and default variants of various functions and added opti...Michael Soegtrop
2019-06-18Removed "b" from function names in Bool.vMichael Soegtrop
2019-06-18[errors] remove "is_handled" logic, turn unhandled into anomaliesEmilio Jesus Gallego Arias
2019-06-17Update headers of files that were stuck on older headers.Théo Zimmermann
2019-06-16Merge PR #10381: Fix #10090: Ltac1 destruct and Ltac2 destruct should do the ...Emilio Jesus Gallego Arias
2019-06-16Fix #10090: Ltac1 destruct and Ltac2 destruct should do the same thing.Pierre-Marie Pédrot
2019-06-16Merge PR #10345: Fix #10339: Anomaly in Ltac2.Emilio Jesus Gallego Arias
2019-06-16- added OCaml copyright header to List.v (if for no other reason than out of ...Michael Soegtrop
2019-06-11STM: encode in static types that vernac_when is only used when VtSideffGaëtan Gilbert
2019-06-09[proof] Uniformize Proof_global APIEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:40:02 +0000