diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 8aac75e39f..3f0570dc9e 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -76,7 +76,7 @@ let split_evar_to_arrow sigma c = let (sigma1,dom) = new_type_var evenv sigma in let hyps = named_context evenv in let nvar = next_ident_away (id_of_string "x") (ids_of_named_context hyps) in - let newenv = push_named_assum (nvar,make_typed dom (Type dummy_univ)) evenv in + let newenv = push_named_assum (nvar, dom) evenv in let (sigma2,rng) = new_type_var newenv sigma1 in let prod = mkProd (named_hd newenv dom Anonymous, dom, subst_var nvar rng) in let sigma3 = Evd.define sigma2 ev prod in |