diff options
| -rw-r--r-- | kernel/cClosure.ml | 11 | ||||
| -rw-r--r-- | kernel/retroknowledge.ml | 2 | ||||
| -rw-r--r-- | kernel/retroknowledge.mli | 1 |
3 files changed, 0 insertions, 14 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 17feeb9b5a..e7cab24aa7 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1085,16 +1085,6 @@ module FNativeEntries = fNInf := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNInf) }; fNaN := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNaN) }; | None -> defined_f_class := false - let defined_refl = ref false - - let frefl = ref dummy - - let init_refl retro = - match retro.Retroknowledge.retro_refl with - | Some crefl -> - defined_refl := true; - frefl := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs crefl) } - | None -> defined_refl := false let defined_array = ref false @@ -1111,7 +1101,6 @@ module FNativeEntries = init_cmp !current_retro; init_f_cmp !current_retro; init_f_class !current_retro; - init_refl !current_retro; init_array !current_retro let check_env env = diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index f7c4b62d1f..505f6c648d 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -35,7 +35,6 @@ type retroknowledge = { (* PNormal, NNormal, PSubn, NSubn, PZero, NZero, PInf, NInf, NaN *) - retro_refl : constructor option } let empty = { @@ -48,7 +47,6 @@ let empty = { retro_cmp = None; retro_f_cmp = None; retro_f_class = None; - retro_refl = None; } type action = diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index fd412cdd0a..80c0baaf95 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -29,7 +29,6 @@ type retroknowledge = { (* PNormal, NNormal, PSubn, NSubn, PZero, NZero, PInf, NInf, NaN *) - retro_refl : constructor option } val empty : retroknowledge |