diff options
| author | xclerc | 2013-09-19 12:59:04 +0000 |
|---|---|---|
| committer | xclerc | 2013-09-19 12:59:04 +0000 |
| commit | 826eb7c6d11007dfd747d49852e71a22e0a3850a (patch) | |
| tree | 25dce16a7107de4e0d3903e2808fb8f083d1f9ea /kernel/closure.ml | |
| parent | 33eea163c72c70eaa3bf76506c1d07a8cde911fd (diff) | |
Get rid of the uses of deprecated OCaml elements (still remaining compatible with OCaml 3.12.1).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 49fd1ae8ed..faa67be46b 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -669,11 +669,11 @@ let rec to_constr constr_fun lfts v = let term_of_fconstr = let rec term_of_fconstr_lift lfts v = match v.term with - | FCLOS(t,env) when is_subs_id env & is_lift_id lfts -> t - | FLambda(_,tys,f,e) when is_subs_id e & is_lift_id lfts -> + | FCLOS(t,env) when is_subs_id env && is_lift_id lfts -> t + | FLambda(_,tys,f,e) when is_subs_id e && is_lift_id lfts -> compose_lam (List.rev tys) f - | FFix(fx,e) when is_subs_id e & is_lift_id lfts -> mkFix fx - | FCoFix(cfx,e) when is_subs_id e & is_lift_id lfts -> mkCoFix cfx + | FFix(fx,e) when is_subs_id e && is_lift_id lfts -> mkFix fx + | FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> mkCoFix cfx | _ -> to_constr term_of_fconstr_lift lfts v in term_of_fconstr_lift el_id |