diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 97f86c6df72f..446106e15c59 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -203,7 +203,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
     else refresh_term_evars ~onevars:false ~top:true t
   in !evdref, t'
 
-let get_type_of_refresh  ?(polyprop=true) ?(lax=false) env evars t =
+let get_type_of_refresh ?(lax=false) env evars t =
   let tty = Retyping.get_type_of env evars t in
   let evars', tty = refresh_universes ~onlyalg:true
     ~status:(Evd.UnivFlexible false) (Some false) env evars tty in
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 78afe4634122..074723ab9e3e 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -176,7 +176,7 @@ val remove_instance_local_defs :
   evar_map -> Evar.t -> 'a list -> 'a list
 
 val get_type_of_refresh :
-  ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr
+  ?lax:bool -> env -> evar_map -> constr
   -> evar_map * types
 
 val checked_appvect_hook : (env -> evar_map -> constr -> constr array -> evar_map * constr) Hook.t