diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
commit | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /pretyping/detyping.ml | |
parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
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) |