Remove unused "polyprop" argument in Evarsolve.get_type_of_refresh

It being unused in the implementation was a bug, but since nobody used it when calling the function it doesn't matter.
SkySkimmer · Dec 20, 2024 · 43f3579 · 43f3579
1 parent bc65d93
commit 43f3579
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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