diff options
Diffstat (limited to 'library/redinfo.ml')
| -rw-r--r-- | library/redinfo.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/redinfo.ml b/library/redinfo.ml index 7cc35efca..f289273ec 100644 --- a/library/redinfo.ml +++ b/library/redinfo.ml @@ -68,7 +68,7 @@ let constant_eval sp = let cb = Global.lookup_constant sp in match cb.const_body with | None -> NotAnElimination - | Some c -> compute_consteval c + | Some v -> let c = cook_constant v in compute_consteval c in eval_table := Spmap.add sp v !eval_table; v |