summaryrefslogtreecommitdiff
path: root/src/expr/expr_manager_template.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/expr_manager_template.h')
-rw-r--r--src/expr/expr_manager_template.h10
1 files changed, 6 insertions, 4 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index f38acd153..561d99392 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -438,8 +438,9 @@ public:
* not a LAMBDA, or is ill-typed, or if CVC4 fails at proving that
* the resulting predicate subtype is inhabited.
*/
- Type mkPredicateSubtype(Expr lambda)
- throw(TypeCheckingException);
+ // not in release 1.0
+ //Type mkPredicateSubtype(Expr lambda)
+ // throw(TypeCheckingException);
/**
* Make a predicate subtype type defined by the given LAMBDA
@@ -448,8 +449,9 @@ public:
* a LAMBDA, or is ill-typed, or if the witness is not a witness or
* ill-typed.
*/
- Type mkPredicateSubtype(Expr lambda, Expr witness)
- throw(TypeCheckingException);
+ // not in release 1.0
+ //Type mkPredicateSubtype(Expr lambda, Expr witness)
+ // throw(TypeCheckingException);
/**
* Make an integer subrange type as defined by the argument.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback