diff options
| author | Pierre Roux | 2020-09-12 09:10:26 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-10-30 14:11:19 +0100 |
| commit | 2d44c8246eccba7c1c452cbfbc6751cd222d0a6a (patch) | |
| tree | 93683ff83a5d70c8aeca9161381aa4d0640dd949 /plugins/syntax | |
| parent | 473160ebe4a835dde50d6c209ab17c7e1b84979c (diff) | |
Renaming Numeral.v into Number.v
Diffstat (limited to 'plugins/syntax')
| -rw-r--r-- | plugins/syntax/numeral.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 2db76719b8..fbf43be91f 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -64,7 +64,7 @@ let locate_numeral () = let hex = "num.hexadecimal.type" in let int = "num.num_int.type" in let uint = "num.num_uint.type" in - let num = "num.numeral.type" in + let num = "num.number.type" in if Coqlib.has_ref dint && Coqlib.has_ref duint && Coqlib.has_ref dec && Coqlib.has_ref hint && Coqlib.has_ref huint && Coqlib.has_ref hex && Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref num |