aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/term.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/term.ml')
-rw-r--r--checker/term.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/checker/term.ml b/checker/term.ml
index b41bebca2..0c3fc741d 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -10,7 +10,6 @@
open Errors
open Util
-open Pp
open Names
open Univ
open Esubst
@@ -134,7 +133,7 @@ let rec strip_outer_cast c = match c with
| Cast (c,_,_) -> strip_outer_cast c
| _ -> c
-let rec collapse_appl c = match c with
+let collapse_appl c = match c with
| App (f,cl) ->
let rec collapse_rec f cl2 =
match (strip_outer_cast f) with