Search results

Should auto-generated schemes be moved inside there own modules/records

Status: Open.

#22 In rocq-archive/stdlib2;

· Matafou opened on Apr 17, 2020

Compatibility with std++ ?

Status: Open.

#20 In rocq-archive/stdlib2;

· spitters opened on Mar 21, 2020

Universes

Status: Open.

#17 In rocq-archive/stdlib2;

· Zimmi48 opened on Mar 25, 2019

Finite maps and finite sets

Status: Open.

#15 In rocq-archive/stdlib2;

· jakobbotsch opened on Mar 12, 2019

discussion of modularity mechanisms

Status: Open.

#13 In rocq-archive/stdlib2;

· andres-erbsen opened on Dec 6, 2018

Make the roadmap of the library more explicit and add dates

Status: Open.

#12 In rocq-archive/stdlib2;

· Zimmi48 opened on Nov 8, 2018

Policy for the superficial layout (spacing, newlines, ...).

Status: Open.

#11 In rocq-archive/stdlib2;

· herbelin opened on Sep 28, 2018

Plan for backwards compatibility and deprecation

Status: Open.

#10 In rocq-archive/stdlib2;

· langston-barrett opened on Jul 20, 2018

What should go in stdlib?

Status: Open.

#7 In rocq-archive/stdlib2;

· gmalecha opened on Jun 24, 2018

Strict behavior for hint databases

Status: Open.

#6 In rocq-archive/stdlib2;

· Zimmi48 opened on Jun 8, 2018

all functions should come with parametricity proofs

Status: Open.

#5 In rocq-archive/stdlib2;

· andres-erbsen opened on Jun 6, 2018

one smallest partial equivalence relation for each type

Status: Open.

#4 In rocq-archive/stdlib2;

· andres-erbsen opened on Jun 5, 2018