aboutsummaryrefslogtreecommitdiff
path: root/user-contrib
AgeCommit message (Expand)Author
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
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-08Fix #10339: Anomaly in Ltac2.Pierre-Marie Pédrot
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-06-04Rename Proof_global.{pstate -> t}Gaëtan Gilbert
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-05-22[Ltac2] Add util files for Bool, List, OptionJason Gross
2019-05-23Fixing typos - Part 2JPR
2019-05-21Fixing typos - Part 1JPR
2019-05-14Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2Pierre-Marie Pédrot
2019-05-14Merge PR #10136: [ltac2] Add primitive integersPierre-Marie Pédrot
2019-05-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
2019-05-10[ltac2] Add primitive integersPierre Roux
2019-05-10Make the check flag of conversion functions mandatory.Pierre-Marie Pédrot
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 03:12:53 +0000