Commits

Breadcrumbs

History for

onmaster

User selector

All users

Datepicker

All time

Commit History

Commits on Jul 19, 2024

• done with simple refine

  Tragicus

  committed
  6bd95e0

  Copy full SHA for 6bd95e0

• Merge PR coq#19382: [ssr] Remove no longer used not_locked_false_eq_true

  Show description for aaa0c13
  

  coqbot-app[bot]

  and

  gares

  authored
  aaa0c13

  Copy full SHA for aaa0c13

• [ssr] Remove no longer used not_locked_false_eq_true

  proux01

  committed
  de8f034

  Copy full SHA for de8f034

Commits on Jul 16, 2024

• improve done

  Show description for dd069dd
  Tragicus

  committed
  dd069dd

  Copy full SHA for dd069dd

Commits on May 31, 2024

• Add a warning for notations with incompatible common prefixes

  Show description for bd48bda
  proux01

  committed
  bd48bda

  Copy full SHA for bd48bda

Commits on May 27, 2024

• Warn about postfix notations not at level 1

  proux01

  committed
  5ec92cf

  Copy full SHA for 5ec92cf

• Warn about closed notations not at level 0

  proux01

  committed
  6ef5873

  Copy full SHA for 6ef5873

Commits on May 17, 2024

• ssr/have: use opaque constants

  gares

  committed
  97213c5

  Copy full SHA for 97213c5

Commits on Dec 6, 2023

• Backport from MathComp

  pi8027

  committed
  312497a

  Copy full SHA for 312497a

Commits on Nov 30, 2023

• Fix typo in documentation

  Show description for 15a8e8a
  createyourpersonalaccount

  committed
  15a8e8a

  Copy full SHA for 15a8e8a

Commits on Nov 9, 2023

• Deprecate % in Arguments command and replace it with %_

  Show description for 8d8edd2
  proux01

  committed
  8d8edd2

  Copy full SHA for 8d8edd2

Commits on Oct 3, 2023

• Dropping two cast notations whose effect is done at in/externalization time.

  Show description for 65c7c58
  

  herbelin

  authored and

  proux01

  committed
  65c7c58

  Copy full SHA for 65c7c58

Commits on Sep 24, 2023

• [ssreflect] Remove "x : p" notation

  Show description for 6703fb9
  proux01

  committed
  6703fb9

  Copy full SHA for 6703fb9

Commits on Jun 7, 2022

• Merge PR coq#16073: [build] [mltop] Distinguish plugin loading API from module loading API

  Show description for 3ffbd1c
  

  coqbot-app[bot]

  and

  SkySkimmer

  authored
  3ffbd1c

  Copy full SHA for 3ffbd1c

Commits on May 31, 2022

• [build] Use compatibility format in stdlib plugin loading.

  ejgallego

  committed
  267af15

  Copy full SHA for 267af15

• Stop inferring template universes in the kernel.

  Show description for f0d9e44
  ppedrot

  committed
  f0d9e44

  Copy full SHA for f0d9e44

Commits on Nov 19, 2021

• ssr: make cutlike tactics compatible with SProp

  gares

  committed
  6e8fe79

  Copy full SHA for 6e8fe79

Commits on Apr 30, 2021

• fix some typos in the doc of theories/ssr

  affeldt-aist

  committed
  2ba38f2

  Copy full SHA for 2ba38f2

Commits on Nov 24, 2020

• Fixing [dup] and [swap]

  CohenCyril

  committed
  5eb1828

  Copy full SHA for 5eb1828

Commits on Nov 22, 2020

• Adapting standard library, doc and test suite to ident->name renaming.

  herbelin

  committed
  df8b5c7

  Copy full SHA for df8b5c7

Commits on Nov 16, 2020

• Explicitly annotate all hint declarations of the standard library.

  Show description for 68cd077
  ppedrot

  committed
  68cd077

  Copy full SHA for 68cd077

Commits on Nov 6, 2020

• Intro pattern extensions for dup, swap and apply

  CohenCyril

  committed
  79c45ec

  Copy full SHA for 79c45ec

Commits on Mar 18, 2020

• Update headers in the whole code base.

  Show description for a99776e
  Zimmi48

  committed
  a99776e

  Copy full SHA for a99776e

Commits on Feb 19, 2020

• Only parsing in Reserved Notation: turning notice into a warning.

  herbelin

  committed
  9dc88f3

  Copy full SHA for 9dc88f3

Commits on Feb 13, 2020

• [build] Consolidate stdlib's .v files under a single directory.

  Show description for 9193769
  ejgallego

  committed
  9193769

  Copy full SHA for 9193769

Loading