diff options
| author |  xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-19 12:59:04 +0000 |
|---|---|---|
| committer | xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-19 12:59:04 +0000 |
| commit | 826eb7c6d11007dfd747d49852e71a22e0a3850a (patch) | |
| tree | 25dce16a7107de4e0d3903e2808fb8f083d1f9ea /plugins/quote | |
| 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 'plugins/quote')
| -rw-r--r-- | plugins/quote/quote.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 998e54767..c09e2d743 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -245,7 +245,7 @@ let compute_ivs gl f cs = (* Then we test if the RHS is the RHS for variables *) else begin match decompose_app bodyi with | vmf, [_; _; a3; a4 ] - when isRel a3 & isRel a4 & + when isRel a3 && isRel a4 && pf_conv_x gl vmf (Lazy.force coq_varmap_find)-> v_lhs := Some (compute_lhs @@ -260,7 +260,7 @@ let compute_ivs gl f cs = end) lci; - if !c_lhs = None & !v_lhs = None then i_can't_do_that (); + if !c_lhs = None && !v_lhs = None then i_can't_do_that (); (* The Cases predicate is a lambda; we assume no dependency *) let p = match kind_of_term p with @@ -295,7 +295,7 @@ binary search trees (see file \texttt{Quote.v}) *) and variables (open terms) *) let rec closed_under cset t = - (ConstrSet.mem t cset) or + (ConstrSet.mem t cset) || (match (kind_of_term t) with | Cast(c,_,_) -> closed_under cset c | App(f,l) -> closed_under cset f && Array.for_all (closed_under cset) l @@ -357,7 +357,7 @@ let path_of_int n = (* This function does not descend under binders (lambda and Cases) *) let rec subterm gl (t : constr) (t' : constr) = - (pf_conv_x gl t t') or + (pf_conv_x gl t t') || (match (kind_of_term t) with | App (f,args) -> Array.exists (fun t -> subterm gl t t') args | Cast(t,_,_) -> (subterm gl t t') |