diff options
Diffstat (limited to 'pretyping/clenv.ml')
| -rw-r--r-- | pretyping/clenv.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index d79910c99..b18034b50 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -127,6 +127,16 @@ let clenv_environments_evars env evd bound c = in clrec (evd,[]) bound c +let clenv_conv_leq env sigma t c bound = + let ty = Retyping.get_type_of env sigma c in + let evd = Evd.create_evar_defs sigma in + let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in + let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in + let evars,_ = Evarconv.consider_remaining_unif_problems env evars in + let args = List.map (whd_evar (Evd.evars_of evars)) args in + check_evars env sigma evars (applist (c,args)); + args + let mk_clenv_from_n gls n (c,cty) = let evd = create_evar_defs gls.sigma in let (env,args,concl) = clenv_environments evd n cty in |