aboutsummaryrefslogtreecommitdiff
path: root/theories/micromega/VarMap.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/micromega/VarMap.v')
-rw-r--r--theories/micromega/VarMap.v5
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/micromega/VarMap.v b/theories/micromega/VarMap.v
index c2472f6303..e28c27f400 100644
--- a/theories/micromega/VarMap.v
+++ b/theories/micromega/VarMap.v
@@ -33,6 +33,11 @@ Inductive t {A} : Type :=
| Branch : t -> A -> t -> t .
Arguments t : clear implicits.
+Register Branch as micromega.VarMap.Branch.
+Register Elt as micromega.VarMap.Elt.
+Register Empty as micromega.VarMap.Empty.
+Register t as micromega.VarMap.type.
+
Section MakeVarMap.
Variable A : Type.