summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
47 hoursMerge PR #18947: deprecate Bvectormastercoqbot-app[bot]
3 daysMerge PR #18957: Properly flush -time-file at exitcoqbot-app[bot]
4 daysMerge PR #18974: Fix build on master (parallel merges of erelevance and ltac2...coqbot-app[bot]
4 daysFix build on master (parallel merges of erelevance and ltac2 API)refs/pull/18974/headGaëtan Gilbert
4 daysMerge PR #18764: Add some Ltac2.Constr.Unsafe combinatorscoqbot-app[bot]
4 daysdeprecate Bvectorrefs/pull/18947/headAndres Erbsen
5 daysMerge PR #18938: Add EConstr.ERelevance abstraction barrier to force normaliz...coqbot-app[bot]
7 daysMerge PR #18952: Cleanup some STM related APIs in declare.mlcoqbot-app[bot]
8 daysMerge PR #18936: remove NArith.Ndigits, NArith.Ndist, and Strings.ByteVectorcoqbot-app[bot]
9 daysAdd Constr.Unsafe.{iter,iter_with_binders,map}refs/pull/18764/headGaëtan Gilbert
9 daysAdd Ltac2.Constr.Unsafe.kind_nocastGaëtan Gilbert
9 daysProperly flush -time-file at exitrefs/pull/18957/headGaëtan Gilbert
9 daysAdd EConstr.ERelevance abstraction barrier to force normalizing relevancesrefs/pull/18938/headGaëtan Gilbert
9 daysRemove Declare.return_partial_proofrefs/pull/18952/headGaëtan Gilbert
9 daysStop returning globref list from save_lemma_proved_delayedGaëtan Gilbert
9 daysRemove unused Declare.Proof.proof_object `name` fieldGaëtan Gilbert
9 daysMerge PR #17403: Deprecating change directorycoqbot-app[bot]
9 daysMerge PR #18910: Set some basic rewriting primitives in Type opaque for TC se...coqbot-app[bot]
9 daysMerge PR #18949: Remove unsafe_typ argument of Declare.prepare_proofcoqbot-app[bot]
9 daysMerge PR #18950: Fix CI_INSTALL_DIR when building locallycoqbot-app[bot]
10 daysMerge PR #18867: Don't make Prop inductives template to control eliminator ge...coqbot-app[bot]
10 daysChange log for #17403refs/pull/17403/headHugo Herbelin
10 daysDeprecate argument-free "Cd" in favor of "Pwd".Hugo Herbelin
10 daysDeprecating Cd in favor of -output-directory or Set Extraction Output Directory.Hugo Herbelin
10 daysFix CI_INSTALL_DIR when building locallyrefs/pull/18950/headGaëtan Gilbert
10 daysRemove unsafe_typ argument of Declare.prepare_proofrefs/pull/18949/headGaëtan Gilbert
10 daysMerge PR #18877: A cleaning step around apply_impargs and find_appl_head_data...coqbot-app[bot]
10 daysDocument the changes.refs/pull/18910/headPierre-Marie Pédrot
10 daysSet some basic rewriting primitives in Type opaque for TC search.Pierre-Marie Pédrot
10 daysMerge PR #18874: Ignore universes of inlined side effects in build_by_tacticcoqbot-app[bot]
10 daysAdd commentrefs/pull/18874/headGaëtan Gilbert
10 daysMerge PR #18895: Set the warning for raw constr hints default to error.coqbot-app[bot]
11 daysMerge PR #18424: [stm] Remove support for .vio filescoqbot-app[bot]
11 daysMerge PR #18859: A few more list, context and term combinatorscoqbot-app[bot]
11 daysMerge PR #18918: Fixes #13979: share universe instance in measure-based Progr...coqbot-app[bot]
11 daysDocument the changes.refs/pull/18895/headPierre-Marie Pédrot
11 daysSlightly tweak the phrasing of the fragile-hint-constr warning.Pierre-Marie Pédrot
11 daysSet the warning for raw constr hints default to error.Pierre-Marie Pédrot
11 daysSlightly more lenient syntax for global reference hints.Pierre-Marie Pédrot
12 daysremove bignums overlayrefs/pull/18936/headAndres Erbsen
12 dayschangelog: mention deprecation timeAndres Erbsen
12 daysMerge PR #18928: Indent body and type when printing local definitions over se...coqbot-app[bot]
12 daysMerge PR #18729: zify Nat.double and Nat.div2coqbot-app[bot]
12 daysMerge PR #18934: Fast path in Unification.make_abstraction_core.coqbot-app[bot]
12 daysMerge PR #18926: Fixes coq-elpi#618: remove synterp code from add_instance_basecoqbot-app[bot]
12 daysMerge PR #18935: Full EConstr-based API for Inductiveops.coqbot-app[bot]
12 daysMerge PR #18771: Improve handling of Dropcoqbot-app[bot]
12 daysAdd overlays.refs/pull/18935/headPierre-Marie Pédrot
12 daysStop normalizing universe instances in Typing.judge_of_projection.Pierre-Marie Pédrot
12 daysFull EConstr-based API for Inductiveops.Pierre-Marie Pédrot
generated by cgit v0.10.2-6-g49f6 at 2024-04-28 11:57:27 (GMT)