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 /tactics/equality.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 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index d1d4e003d6..04d6b9d8e8 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -480,7 +480,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl = in let t1 = pf_apply get_type_of gl c1 and t2 = pf_apply get_type_of gl c2 in - if unsafe or (pf_conv_x gl t1 t2) then + if unsafe || (pf_conv_x gl t1 t2) then let e = build_coq_eq () in let sym = build_coq_eq_sym () in let eq = applist (e, [t1;c1;c2]) in @@ -1060,7 +1060,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let make_iterated_tuple env sigma dflt (z,zty) = let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in let sort_of_zty = get_sort_of env sigma zty in - let sorted_rels = Sort.list (<) (Int.Set.elements rels) in + let sorted_rels = List.sort Pervasives.compare (Int.Set.elements rels) in let (tuple,tuplety) = List.fold_left (make_tuple env sigma) (z,zty) sorted_rels in @@ -1208,7 +1208,7 @@ let postInjEqTac ipats c n = let injEq ipats = let l2r = - if use_injection_pattern_l2r_order () & ipats <> None then true else false + if use_injection_pattern_l2r_order () && ipats <> None then true else false in injEqThen (postInjEqTac ipats) l2r |