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 /interp/notation_ops.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 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index b571d03442..0e4cd80df4 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -151,14 +151,14 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2 | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> - on_true_do (f ty1 ty2 & f c1 c2) add na1 + on_true_do (f ty1 ty2 && f c1 c2) add na1 | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> - on_true_do (f ty1 ty2 & f c1 c2) add na1 + on_true_do (f ty1 ty2 && f c1 c2) add na1 | GHole _, GHole _ -> true | GSort (_,s1), GSort (_,s2) -> glob_sort_eq s1 s2 | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 -> - on_true_do (f b1 b2 & f c1 c2) add na1 + on_true_do (f b1 b2 && f c1 c2) add na1 | (GCases _ | GRec _ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ | _,(GCases _ | GRec _ @@ -315,8 +315,8 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) = let () = List.iter check foundrecbinding in let check_bound x = if not (List.mem x found) then - if List.mem_assoc x foundrec or List.mem_assoc x foundrecbinding - or list_rev_mem_assoc x foundrec or list_rev_mem_assoc x foundrecbinding + if List.mem_assoc x foundrec || List.mem_assoc x foundrecbinding + || list_rev_mem_assoc x foundrec || list_rev_mem_assoc x foundrecbinding then error ((Id.to_string x)^" should not be bound in a recursive pattern of the right-hand side.") else @@ -424,7 +424,7 @@ let rec subst_notation_constr subst bound raw = (cpl',r')) branches in - if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' & + if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' && rl' == rl && branches' == branches then raw else NCases (sty,rtntypopt',rl',branches') |