diff options
Diffstat (limited to 'theories/micromega/DeclConstant.v')
| -rw-r--r-- | theories/micromega/DeclConstant.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/micromega/DeclConstant.v b/theories/micromega/DeclConstant.v index bd8490d796..2e50481b13 100644 --- a/theories/micromega/DeclConstant.v +++ b/theories/micromega/DeclConstant.v @@ -35,6 +35,7 @@ Require Import List. (** Ground terms (see [GT] below) are built inductively from declared constants. *) Class DeclaredConstant {T : Type} (F : T). +Register DeclaredConstant as micromega.DeclaredConstant.type. Class GT {T : Type} (F : T). |