diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a74e4cb4..0166b64c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -272,7 +272,7 @@ let is_nondep_branch c n = try let sign,ccl = decompose_lam_n_assum n c in noccur_between 1 (rel_context_length sign) ccl - with _ -> (* Not eta-expanded or not reduced *) + with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *) false let extract_nondep_branches test c b n = @@ -386,7 +386,7 @@ let rec detype (isgoal:bool) avoid env t = | Var id -> (try let _ = Global.lookup_named id in GRef (dl, VarRef id) - with _ -> + with e when Errors.noncritical e -> GVar (dl, id)) | Sort s -> GSort (dl,detype_sort s) | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> @@ -492,7 +492,7 @@ and detype_eqns isgoal avoid env ci computable constructs consnargsl bl = let mat = build_tree Anonymous isgoal (avoid,env) ci bl in List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env c)) mat - with _ -> + with e when Errors.noncritical e -> Array.to_list (array_map3 (detype_eqn isgoal avoid env) constructs consnargsl bl) |