diff options
| author |  xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-14 07:33:57 +0000 |
|---|---|---|
| committer | xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-14 07:33:57 +0000 |
| commit | ec5ed7870b4b59e05c5e994c9bad35e28685b8bd (patch) | |
| tree | 6b735f9c86df8102f132946afbf7b728f5b19edc /checker/closure.ml | |
| parent | 38d9a3342f626d16bcf5c993bf15ff3e6e8ee8d9 (diff) | |
Getting rid of the use of deprecated elements (from the OCaml standard library).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/closure.ml')
| -rw-r--r-- | checker/closure.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index 3ed9dd27a..55c91b93e 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -345,7 +345,7 @@ let compact_stack head stk = (* Put an update mark in the stack, only if needed *) let zupdate m s = - if !share & m.norm = Red + if !share && m.norm = Red then let s' = compact_stack m s in let _ = m.term <- FLOCKED in @@ -541,11 +541,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 -> Fix fx - | FCoFix(cfx,e) when is_subs_id e & is_lift_id lfts -> CoFix cfx + | FFix(fx,e) when is_subs_id e && is_lift_id lfts -> Fix fx + | FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> CoFix cfx | _ -> to_constr term_of_fconstr_lift lfts v in term_of_fconstr_lift el_id |