diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 20a1e9c10..14d2ceac4 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -2458,13 +2458,6 @@ sig
       A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. *)
   val is_pull_quant : Expr.expr -> bool
 
-  (** Indicates whether the term is a proof for pulling quantifiers out.
-
-      A proof for (iff P Q) where Q is in prenex normal form.
-      This proof object is only used if the parameter PROOF_MODE is 1.
-      This proof object has no antecedents *)
-  val is_pull_quant_star : Expr.expr -> bool
-
   (** Indicates whether the term is a proof for pushing quantifiers in.
 
       A proof for:
@@ -2658,22 +2651,6 @@ sig
       (and (or r_1 r_2) (or r_1' r_2'))) *)
   val is_nnf_neg : Expr.expr -> bool
 
-  (** Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.
-
-      A proof for (~ P Q) where Q is in negation normal form.
-
-      This proof object is only used if the parameter PROOF_MODE is 1.
-
-      This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. *)
-  val is_nnf_star : Expr.expr -> bool
-
-  (** Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.
-
-      A proof for (~ P Q) where Q is in conjunctive normal form.
-      This proof object is only used if the parameter PROOF_MODE is 1.
-      This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.           *)
-  val is_cnf_star : Expr.expr -> bool
-
   (** Indicates whether the term is a proof for a Skolemization step
 
       Proof for:
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index e68d7280d..d4ff556fe 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -368,9 +368,6 @@ class AstRef(Z3PPObject):
     def __copy__(self):
         return self.translate(self.ctx)
 
-    def __deepcopy__(self):
-        return self.translate(self.ctx)
-
     def hash(self):
         """Return a hashcode for the `self`.
 
diff --git a/src/api/z3_algebraic.h b/src/api/z3_algebraic.h
index faa41bfea..49c61afef 100644
--- a/src/api/z3_algebraic.h
+++ b/src/api/z3_algebraic.h
@@ -31,7 +31,7 @@ extern "C" {
     /** @name Algebraic Numbers */
     /*@{*/
     /**
-       \brief Return Z3_TRUE if \c can be used as value in the Z3 real algebraic
+       \brief Return Z3_TRUE if \c a can be used as value in the Z3 real algebraic
        number package.
 
        def_API('Z3_algebraic_is_value', BOOL, (_in(CONTEXT), _in(AST)))
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 88d6aa1cf..87bb4d818 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -4350,7 +4350,7 @@ extern "C" {
     Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a);
 
     /**
-       \brief Return true if the give AST is a real algebraic number.
+       \brief Return true if the given AST is a real algebraic number.
 
        def_API('Z3_is_algebraic_number', BOOL, (_in(CONTEXT), _in(AST)))
     */