1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
From Stdlib.Program Require Export Utils.
From Stdlib.Program Require Export Wf.
From Stdlib.Program Require Export Equality.
From Stdlib.Program Require Export Subset.
From Stdlib.Program Require Export Basics.
From Stdlib.Program Require Export Combinators.
From Stdlib.Program Require Export Syntax.
From Stdlib.Program Require Export WfExtensionality.
|
