From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:10 +0200 Subject: Imported Upstream version 8.4pl2dfsg --- pretyping/detyping.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/detyping.ml') 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) -- cgit v1.2.3