Simplifications autour de typed_type (renommé types par analogie avec sorts); documentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7

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