Commits

Branch selector

 refs/heads/master

User selector

All users

Datepicker

All time

Commit History

Commits on Oct 28, 2021

• Merge pull request #85 from ppedrot/engine-without-global

  Show description for d6cf55f
  SkySkimmer

  authored
  d6cf55f

Commits on Oct 27, 2021

• Adapt w.r.t. coq/coq#15069.

  ppedrot

  committed
  2cc62e7

Commits on Oct 8, 2021

• Merge pull request #83 from SkySkimmer/nohdr

  Show description for 7eee0a9
  SkySkimmer

  authored
  7eee0a9

• Adapt to coq/coq#15003 (user_err has no hdr argument)

  Show description for d1c0743
  SkySkimmer

  committed
  d1c0743

Commits on Oct 5, 2021

• Merge pull request #80 from ppedrot/move-opaque-out-of-kernel

  Show description for ee67af1
  ppedrot

  authored
  ee67af1

Commits on Sep 24, 2021

• Adapt w.r.t. coq/coq#14924.

  ppedrot

  committed
  35c647a

Commits on Sep 22, 2021

• Merge pull request #78 from ppedrot/split-mono-univ-entry

  Show description for 81bcb7b
  SkySkimmer

  authored
  81bcb7b

• Merge pull request #77 from herbelin/master+adapt-coq-pr14846-ind-as-ind-rather-than-rel-in-constructor-types

  Show description for cb603f7
  SkySkimmer

  authored
  cb603f7

Commits on Sep 20, 2021

• Adapt w.r.t. coq/coq#14903.

  ppedrot

  committed
  d84995d

• Merge pull request #76 from herbelin/master+adapt-coq-pr14711-univs-ctx-and-binders-centralized

  Show description for b2c96d2
  SkySkimmer

  authored
  b2c96d2

Commits on Sep 19, 2021

• Taking into account deprecations in passing.

  herbelin

  committed
  dedb341

• Adapt to Coq PR #14846: refs to inductive types are Ind instead of Rel in constructor types.

  herbelin

  committed
  7a19362

Commits on Sep 9, 2021

• Adapting to Coq PR #14711: Evd.univ_entry returns also the universe binders.

  herbelin

  committed
  263b892

Commits on Aug 25, 2021

• update meta.yml to be consistent with boilerplate

  palmskog

  committed
  4c8364f

Commits on Aug 24, 2021

• Merge pull request #72 from coq-community/refine-docs

  Show description for af479a3
  proux01

  authored
  af479a3

• More precision about tactic for solving obligations

  Show description for 8016883
  

  palmskog

  and

  proux01

  authored
  8016883

• fix spacing issue in README.md

  palmskog

  committed
  05299eb

• refactoring of documentation in meta.yml, regenerate boilerplate

  palmskog

  committed
  661c600

• Merge pull request #71 from coq-community/theories

  Show description for d0df5b0
  proux01

  authored
  d0df5b0

Commits on Aug 23, 2021

• introduce Params.v file, use standard Makefile and _CoqProject, fix Dune build

  palmskog

  committed
  fa8d21e

• Merge pull request #70 from coq-community/opam-ci-test

  Show description for 9f5882c
  proux01

  authored
  9f5882c

• run tests after make install in opam package

  palmskog

  committed
  51014d3

Commits on Aug 21, 2021

• use opam testing facilities to run tests, simplifying CI configuration

  palmskog

  committed
  21cd7d2

Commits on Aug 19, 2021

• Merge pull request #69 from herbelin/master+adapt-coq-pr14746-subst_instance_context-in-econstr

  Show description for 1afda59
  proux01

  authored
  1afda59

• Adapt to Coq PR #14746: subst_instance_context also in EConstr.

  herbelin

  committed
  bea673c

• Adapt to Coq PR #14726: extended_rel_vect -> instance.

  herbelin

  committed
  3b592be

Commits on Jul 23, 2021

• Merge pull request #68 from herbelin/master+adapt-coq-pr14692-slight-simplification-UContext

  Show description for 3f23dcc
  SkySkimmer

  authored
  3f23dcc

Commits on Jul 21, 2021

• Adapting to Coq PR #14692: UContext now includes the names by default.

  herbelin

  committed
  4db048b

Commits on Jun 3, 2021

• Revert previous commit

  Show description for 1d9409b
  proux01

  committed
  1d9409b

Commits on May 20, 2021

• Use fresh universes for parametric inductives

  Show description for d90d06b
  proux01

  committed
  d90d06b

Commits on Apr 23, 2021

• Merge pull request #65 from gares/syndef-principal-scope

  Show description for 14255f1
  ppedrot

  authored
  14255f1

Commits on Apr 8, 2021

• Merge pull request #67 from mrhaandi/mod-uniform

  Show description for 94b52b4
  proux01

  authored
  94b52b4

• Future proof for coq/coq#14086

  mrhaandi

  committed
  e9a5980

Commits on Apr 6, 2021

• Merge pull request #66 from coq-community/SkySkimmer-patch-1

  Show description for 4adb241
  SkySkimmer

  authored
  4adb241

• Disable native compile in test suite

  Show description for 1969eeb
  SkySkimmer

  authored
  1969eeb

Pagination

PreviousNext