diff options
| author | Gaëtan Gilbert | 2020-11-23 15:49:44 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-23 15:49:44 +0100 |
| commit | 8c2caf0caee19fd8e67e52e05bfc4a8d9ca8d186 (patch) | |
| tree | 3e4d9b348c7ce7ab1d748af82d38dbe241f9370f /kernel/cClosure.ml | |
| parent | 94d579844817edcbb2454dd9dc79071b2cd1d12a (diff) | |
Remove unused retro_refl
Diffstat (limited to 'kernel/cClosure.ml')
| -rw-r--r-- | kernel/cClosure.ml | 11 |
1 files changed, 0 insertions, 11 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 = |