diff options
author | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
commit | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch) | |
tree | 0de2a907ee93c795978f3c843155bee91c11ed60 /pretyping/clenv.ml | |
parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) |
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'pretyping/clenv.ml')
-rw-r--r-- | pretyping/clenv.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 0b88b14b..6113ec2d 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: clenv.ml 8688 2006-04-07 15:08:12Z msozeau $ *) +(* $Id: clenv.ml 8752 2006-04-27 19:37:33Z herbelin $ *) open Pp open Util @@ -84,10 +84,10 @@ let clenv_environments evd bound c = let dep = dependent (mkRel 1) c2 in let na' = if dep then na else Anonymous in let e' = meta_declare mv c1 ~name:na' e in - clrec (e', (mkMeta mv)::metas) (option_app ((+) (-1)) n) + clrec (e', (mkMeta mv)::metas) (option_map ((+) (-1)) n) (if dep then (subst1 (mkMeta mv) c2) else c2) | (n, LetIn (na,b,_,c)) -> - clrec (e,metas) (option_app ((+) (-1)) n) (subst1 b c) + clrec (e,metas) (option_map ((+) (-1)) n) (subst1 b c) | (n, _) -> (e, List.rev metas, c) in clrec (evd,[]) bound c @@ -100,10 +100,10 @@ let clenv_environments_evars env evd bound c = | (n, Prod (na,c1,c2)) -> let e',constr = Evarutil.new_evar e env c1 in let dep = dependent (mkRel 1) c2 in - clrec (e', constr::ts) (option_app ((+) (-1)) n) + clrec (e', constr::ts) (option_map ((+) (-1)) n) (if dep then (subst1 constr c2) else c2) | (n, LetIn (na,b,_,c)) -> - clrec (e,ts) (option_app ((+) (-1)) n) (subst1 b c) + clrec (e,ts) (option_map ((+) (-1)) n) (subst1 b c) | (n, _) -> (e, List.rev ts, c) in clrec (evd,[]) bound c |