Block or report user



Popular repositories

  1. ltac2

    A standalone implementation of Ltac2 as a Coq plugin

    OCaml 16 8

  2. ocaml-compactor

    Small library to compute maximal sharing of OCaml datastructures.

    OCaml 5

  3. coq-forcing

    Tentative implementation of call-by-name forcing in Coq

    Coq 5 2

  4. lsh-generator

    Generate titles of conferences in philosophy!

    OCaml 4

  5. sat-coq

    A reflexive sat & tauto solver in Coq.

    Verilog 3

  6. ll-coq

    Some Coq formalizations of Linear Logic

    Coq 2 1

825 contributions in the last year

Apr May Jun Jul Aug Sep Oct Nov Dec Jan Feb Mar Apr Mon Wed Fri

Contribution activity First pull request First issue First repository Joined GitHub

April 2018

Created a pull request in coq/coq that received 10 comments

Fix #6951: Unexpected error during scheme creation.

When creating a scheme for bifinite inductive types, we do not create a fixpoint.

+12 −2 10 comments

Created an issue in coq/coq that received 14 comments

"where" clauses in record fields do not work

The following feature which is described in the manual doesn't work on 4c3564a. Reserved Notation "'bar'". Record Foo := { foo : bar where "'bar'" …


Seeing something unexpected? Take a look at the GitHub profile guide.