diff options
Diffstat (limited to 'contrib/subtac/subtac_pretyping_F.ml')
| -rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index c32971289..9339d7387 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -162,8 +162,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* in environment [env], with existential variables [(evars_of isevars)] and *) (* the type constraint tycon *) let rec pretype (tycon : type_constraint) env isevars lvar c = - let _ = Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ - str " with tycon " ++ Evarutil.pr_tycon env tycon) in + let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ + str " with tycon " ++ Evarutil.pr_tycon env tycon) + with _ -> () + in match c with | RRef (loc,ref) -> inh_conv_coerce_to_tycon loc env isevars |