diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-07 00:56:12 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-07 00:56:12 +0200 |
commit | 82f18a32e4740c1429ac62506faff83955423417 (patch) | |
tree | fa1fba2891811139dfa30c1df7cfaad0581fb4d0 /engine/termops.ml | |
parent | 6748d06e9618a91a63cd09b4809e67b665818acd (diff) | |
parent | 31a35fe712a836c90562edebc01bfcf3d1c6646a (diff) |
Merge PR #6874: [econstr] Some minor tweaks
Diffstat (limited to 'engine/termops.ml')
-rw-r--r-- | engine/termops.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 0c567754a..eacc36107 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -781,24 +781,23 @@ let map_constr_with_full_binders sigma g f l cstr = let fold_constr_with_full_binders sigma g f n acc c = let open RelDecl in - let inj c = EConstr.Unsafe.to_constr c in match EConstr.kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> acc | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (LocalDef (na, inj b, inj t)) n) (f n (f n acc b) t) c + | Prod (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c + | Lambda (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g (LocalDef (na, b, t)) n) (f n (f n acc b) t) c | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (p,c) -> f n acc c | Evar (_,l) -> Array.fold_left (f n) acc l | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in + let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in + let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd |