diff options
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 064990f6bf..cdb86afa1a 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -249,17 +249,6 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = | Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u)) | _ -> assert false -(* Profiling *) -(* let get_type_of polyprop lax env sigma c = *) -(* let f,_,_,_ = retype ~polyprop sigma in *) -(* if lax then f env c else anomaly_on_error (f env) c *) - -(* let get_type_of_key = CProfile.declare_profile "get_type_of" *) -(* let get_type_of = CProfile.profile5 get_type_of_key get_type_of *) - -(* let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = *) -(* get_type_of polyprop lax env sigma c *) - let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = let f,_,_ = retype ~polyprop sigma in if lax then f env c else anomaly_on_error (f env) c |