Barsotti--Weil formula over separably closed fields

Let $S$ be a noetherian scheme and let $A$ be an abelian scheme on $S$ with dual $A^\vee$. The generalised Barsotti Weil formula states that there is a canonical and functorial (in $S$ and $A$) isomorphism of groups

$$A^\vee(S) \cong \mathrm{Ext}^1_S(A,\mathbb G_m)$$

the classical version being the special case where $S$ is the spectrum of an algebraically closed field. There are at least two references for this in the literture: The standard one is Oort's LNM on commutative group schemes, where he proves that the Barsotti--Weil formula over $S$ holds if it holds over all residue fields of $S$. He then says that the formula is known to hold over any field and quotes Serre's Groupes algébriques et corps de classes, VII.16, théorème 6. The other one is by Milne, exactly along the same lines and also quoting Serre.

My problem with this is that Serre makes right at the beginning of chapter VII in loc. cit. the assumption that the ground field is algebraically closed.

Hence, as long as all residue fields of $S$ are perfect Oort's proof is fine (functoriality in $S$, so one can go down with Galois). For the general case one should/must check that Serre's arguments also work over separably closed fieds. A first careless walkthrough didn't reveal any serious problem with that, so probably everything is just fine. Since "probably just fine" is not good enough:

Here is my request: A proof of the Barsotti--Weil formula over separably closed fields, preferably a reference, but I will appreciate any text or note where this is carefully checked.

By the way: Even if one is only interested in abelian varieties over, say, a finite field, it is important to have Barsotti--Weil over all schemes of finite type over that field, the reason is that one often wants to fppf--sheafify the Barsotti--Weil isomorphism so to get an isomorpihsm of abelian varieties $A^\vee \cong \underline{\mathrm{Ext}}^1(A,\mathbb G_m)$ over the ground field.

-
Serre's argument works verbatim over separably closed fields since smooth schemes have dense locus of rational pts in such cases (e.g., the non-empty smooth fiber of $C \rightarrow A$ over $e \in A(k)$, in Serre's notation). To verify some asserted equalities of maps one may pass to alg. closure if it feels reassuring, but not really necessary. So may not exist a reference, since copying Serre literally. Serre was just in my office so I asked him about that hypothesis, and it was as I expected: foundations of alg. geom. at that time (e.g., his FAC) were worked out only for alg. closed field. –  BCnrd May 12 '10 at 23:23
Thanks for taking the opportunity. –  Xandi Tuni May 13 '10 at 7:22