diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 6e0e098c03..49106c9125 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -483,7 +483,7 @@ let infer env constr = let (j,(cst,_)) = execute env constr (empty_constraint, universes env) in assert (eq_constr j.uj_val constr); - ({ j with uj_val = constr }, cst) + (j, cst) let infer_type env constr = let (j,(cst,_)) = |