-
Notifications
You must be signed in to change notification settings - Fork 21
/
Constants.v
36 lines (29 loc) · 1.71 KB
/
Constants.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
(* *********************************************************************** *)
(* This is part of aac_tactics, it is distributed under the terms of the *)
(* GNU Lesser General Public License version 3 *)
(* (see file LICENSE for more details) *)
(* *)
(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *)
(* *********************************************************************** *)
Register Init.Datatypes.O as aac_tactics.nat.O.
Register Init.Datatypes.S as aac_tactics.nat.S.
Register Init.Datatypes.nat as aac_tactics.nat.type.
Register Init.Datatypes.pair as aac_tactics.pair.pair.
Register Init.Datatypes.prod as aac_tactics.pair.prod.
Register Init.Datatypes.option as aac_tactics.option.typ.
Register Init.Datatypes.Some as aac_tactics.option.Some.
Register Init.Datatypes.None as aac_tactics.option.None.
Register Init.Datatypes.list as aac_tactics.list.typ.
Register Init.Datatypes.nil as aac_tactics.list.nil.
Register Init.Datatypes.cons as aac_tactics.list.cons.
From Coq Require BinNums.
Register BinNums.positive as aac_tactics.pos.typ.
Register BinNums.xI as aac_tactics.pos.xI.
Register BinNums.xO as aac_tactics.pos.xO.
Register BinNums.xH as aac_tactics.pos.xH.
From Coq Require Classes.Morphisms.
Register Morphisms.Proper as aac_tactics.coq.classes.morphisms.Proper.
From Coq Require Classes.RelationClasses.
Register RelationClasses.Equivalence as aac_tactics.coq.RelationClasses.Equivalence.
Register RelationClasses.Reflexive as aac_tactics.coq.RelationClasses.Reflexive.
Register RelationClasses.Transitive as aac_tactics.coq.RelationClasses.Transitive.