From d2c5c5e616a6e118291fe1ce9965c731adac03a8 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 19 Jan 2014 15:09:23 +0100 Subject: Imported Upstream version 8.4pl3dfsg --- pretyping/detyping.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/detyping.ml') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 0166b64c..1065aec9 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -300,7 +300,7 @@ let it_destRLambda_or_LetIn_names n c = let a = GVar (dl,x) in aux (n-1) (Name x :: nal) (match c with - | GApp (loc,p,l) -> GApp (loc,c,l@[a]) + | GApp (loc,p,l) -> GApp (loc,p,l@[a]) | _ -> (GApp (dl,c,[a]))) in aux n [] c @@ -481,7 +481,7 @@ and share_names isgoal n l avoid env c t = share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> - if n>0 then warning "Detyping.detype: cannot factorize fix enough"; + if n>0 then msg_warn "Detyping.detype: cannot factorize fix enough"; let c = detype isgoal avoid env c in let t = detype isgoal avoid env t in (List.rev l,c,t) -- cgit v1.2.3