Search code, repositories, users, issues, pull requests...

rocq-prover/rocq

#6504

· by SkySkimmer was closed

on Dec 27, 2017

Update the lower-bound of the lablgtk dependency.

rocq-prover/rocq

#6533

· by Zimmi48 was closed

on Jan 8, 2018

Document use of ocamldebug from the command line in Cygwin/Windows

rocq-prover/rocq

#6501

· by jfehrle was closed

on Jan 8, 2018

Document between and exists_between types.

rocq-prover/rocq

#6510

· by ismail-s was closed

on Jan 8, 2018

Trim more trailing whitespace in coq-makefile timing test

rocq-prover/rocq

#6517

· by JasonGross was closed

on Jan 8, 2018

More detailed error messages for Canonical Structure, #6398

kind: user messages

rocq-prover/rocq

#6418

· by psteckler was closed

on Feb 12, 2018

Build with windows line endings

part: installation

platform: Windows

rocq-prover/rocq

#6305

· by jfehrle was closed

on Dec 18, 2017

Fix #6297: handle constraints like (u+1 <= Set/Prop)

kind: anomaly

part: universes

rocq-prover/rocq

#6298

· by SkySkimmer was closed

on Jan 17, 2018

Make the micromega extraction check a regular output test.

kind: cleanup

rocq-prover/rocq

#6234

· by SkySkimmer was closed

on Dec 19, 2017

[v8.7-only] Fixing #6486, coq_makefile print all its messages.

rocq-prover/rocq

#6491

· by Matafou was closed

on Jan 9, 2018

[error] Replace msg_error by a proper exception.

rocq-prover/rocq

#6262

· by ejgallego was closed

on Feb 12, 2018

Fix CI with parallel make (messed up dependencies)

rocq-prover/rocq

#6474

· by SkySkimmer was closed

on Dec 21, 2017

Gitlab touchup

rocq-prover/rocq

#6465

· by SkySkimmer was closed

on Dec 22, 2017

Replace md5sum/md5 calls by an OCaml program

kind: redesign

rocq-prover/rocq

#6466

· by kit-ty-kate was closed

on Jan 17, 2018

[doc] Nit on the manual.

rocq-prover/rocq

#6453

· by ejgallego was closed

on Dec 18, 2017

[make] More build fixes for static plugins and ocamlfind.

rocq-prover/rocq

#6447

· by ejgallego was closed

on Dec 18, 2017

Fix #5368: Canonical structure unification fails.

rocq-prover/rocq

#6436

· by ppedrot was closed

on Dec 18, 2017

Circle CI

kind: feature

rocq-prover/rocq

#6400

· by SkySkimmer was closed

on Dec 19, 2017

In gitlab set TRAVIS_BRANCH so user overlays will work as expected.

rocq-prover/rocq

#1065

· by SkySkimmer was closed

on Sep 22, 2017

Fixing Print for inductive types with let-in in parameters

rocq-prover/rocq

#1082

· by herbelin was closed

on Feb 13, 2018

Normalize package names

rocq-prover/rocq

#6549

· by Zimmi48 was closed

on Jan 8, 2018

Allow vernacular controls before focus selector

part: RocqIDE

rocq-prover/rocq

#6652

· by psteckler was closed

on Feb 5, 2018

Update configure.ml to only warn on lablgtk >= 2.16.0 and < 2.18.3

priority: blocker

rocq-prover/rocq

#6600

· by JasonGross was closed

on Jan 17, 2018

Fix Ltac subterm matching in (co-)fixpoints.

kind: anomaly