diff options
| author | ppedrot | 2013-11-06 14:52:19 +0000 |
|---|---|---|
| committer | ppedrot | 2013-11-06 14:52:19 +0000 |
| commit | a09f5ba40039c0f367c320986011c2d08b953c5b (patch) | |
| tree | 8e7b660793838c6c07847698ecf33ecf59c872cb /kernel/esubst.ml | |
| parent | 84d1ea3dc63fed962757d3100122382c2e8fb4d6 (diff) | |
Less partial applications in Vars, as well as better memory allocation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17065 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/esubst.ml')
| -rw-r--r-- | kernel/esubst.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 998bba4926..32ccebea68 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -87,7 +87,7 @@ let subs_shft = function | (0, s) -> s | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1) | (n, s) -> SHIFT (n,s) -let subs_shft (n,a) = if Int.equal n 0 then a else subs_shft(n,a) +let subs_shft s = if Int.equal (fst s) 0 then snd s else subs_shft s let subs_shift_cons = function (0, s, t) -> CONS(t,s) @@ -136,7 +136,7 @@ let rec comp mk_cl s1 s2 = | ESID _, _ -> s2 | SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2) | _, CONS(x,s') -> - CONS(Array.map (fun t -> mk_cl(s1,t)) x, comp mk_cl s1 s') + CONS(CArray.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s') | CONS(x,s), SHIFT(k,s') -> let lg = Array.length x in if k == lg then comp mk_cl s s' |