summaryrefslogtreecommitdiff
path: root/contrib/interface/blast.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/blast.ml')
-rw-r--r--contrib/interface/blast.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 9e450068..dc27cf98 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -92,7 +92,7 @@ let rec def_const_in_term_rec vl x =
| Case(_,x,t,a)
-> def_const_in_term_rec vl x
| Cast(x,_,t)-> def_const_in_term_rec vl t
- | Const(c) -> def_const_in_term_rec vl (lookup_constant c vl).const_type
+ | Const(c) -> def_const_in_term_rec vl (Typeops.type_of_constant vl c)
| _ -> def_const_in_term_rec vl (type_of vl Evd.empty x)
;;
let def_const_in_term_ x =