diff options
Diffstat (limited to 'pretyping/clenv.ml')
| -rw-r--r-- | pretyping/clenv.ml | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 412763d7..a41cdd6f 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: clenv.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Pp open Util @@ -128,7 +128,7 @@ let clenv_conv_leq env sigma t c bound = let evd = Evd.create_goal_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 evars = Evarconv.consider_remaining_unif_problems env evars in let args = List.map (whd_evar evars) args in check_evars env sigma evars (applist (c,args)); args @@ -454,18 +454,23 @@ let clenv_constrain_dep_args hyps_only bl clenv = (****************************************************************) (* Clausal environment for an application *) -let make_clenv_binding_gen hyps_only n gls (c,t) = function + +let make_clenv_binding_gen hyps_only n env sigma (c,t) = function | ImplicitBindings largs -> - let clause = mk_clenv_from_n gls n (c,t) in + let clause = mk_clenv_from_env env sigma n (c,t) in clenv_constrain_dep_args hyps_only largs clause | ExplicitBindings lbind -> - let clause = mk_clenv_rename_from_n gls n (c,t) in - clenv_match_args lbind clause + let clause = mk_clenv_from_env env sigma n + (c,rename_bound_vars_as_displayed [] t) + in clenv_match_args lbind clause | NoBindings -> - mk_clenv_from_n gls n (c,t) + mk_clenv_from_env env sigma n (c,t) -let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls -let make_clenv_binding = make_clenv_binding_gen false None +let make_clenv_binding_env_apply env sigma n = + make_clenv_binding_gen true n env sigma + +let make_clenv_binding_apply gls n = make_clenv_binding_gen true n (pf_env gls) gls.sigma +let make_clenv_binding gls = make_clenv_binding_gen false None (pf_env gls) gls.sigma (****************************************************************) (* Pretty-print *) |