diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/closure.ml | 10 | ||||
| -rw-r--r-- | checker/declarations.ml | 2 | ||||
| -rw-r--r-- | checker/inductive.ml | 16 | ||||
| -rw-r--r-- | checker/reduction.ml | 2 |
4 files changed, 15 insertions, 15 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 diff --git a/checker/declarations.ml b/checker/declarations.ml index a6a7f9405..dfa7d401e 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -446,7 +446,7 @@ let is_opaque cb = match cb.const_body with let subst_rel_declaration sub (id,copt,t as x) = let copt' = Option.smartmap (subst_mps sub) copt in let t' = subst_mps sub t in - if copt == copt' & t == t' then x else (id,copt',t') + if copt == copt' && t == t' then x else (id,copt',t') let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) diff --git a/checker/inductive.ml b/checker/inductive.ml index 9e1524018..2dd76c4d3 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -345,8 +345,8 @@ let type_case_branches env (ind,largs) (p,pj) c = let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if - not (eq_ind indsp ci.ci_ind) or - (mib.mind_nparams <> ci.ci_npar) or + not (eq_ind indsp ci.ci_ind) || + (mib.mind_nparams <> ci.ci_npar) || (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) then raise (TypeError(env,WrongCaseInfo(indsp,ci))) @@ -657,7 +657,7 @@ let check_one_fix renv recpos def = match f with | Rel p -> (* Test if [p] is a fixpoint (recursive call) *) - if renv.rel_min <= p & p < renv.rel_min+nfi then + if renv.rel_min <= p && p < renv.rel_min+nfi then begin List.iter (check_rec_call renv []) l; (* the position of the invoked fixpoint: *) @@ -779,11 +779,11 @@ let check_one_fix renv recpos def = let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = let nbfix = Array.length bodies in if nbfix = 0 - or Array.length nvect <> nbfix - or Array.length types <> nbfix - or Array.length names <> nbfix - or bodynum < 0 - or bodynum >= nbfix + || Array.length nvect <> nbfix + || Array.length types <> nbfix + || Array.length names <> nbfix + || bodynum < 0 + || bodynum >= nbfix then anomaly (Pp.str "Ill-formed fix term"); let fixenv = push_rec_types recdef env in let raise_err env i err = diff --git a/checker/reduction.ml b/checker/reduction.ml index 53a12295e..e07a3128b 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -144,7 +144,7 @@ type conv_pb = let sort_cmp univ pb s0 s1 = match (s0,s1) with - | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos & c2 = Null then raise NotConvertible + | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible | (Prop c1, Type u) -> (match pb with |