The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi list,

In both 8.4 and trunk, the following program leaves one obligation:

  Require Import List Program.

  Program Fixpoint zip
          {A B : Set} (a : list A) (b : list B)
          (p: length a = length b) : { l: list (A * B) | (length l = length 
a) } :=
    match a, b with
    | [], [] => []
    | x :: y, x' :: y' => (x, x') :: (zip y y' _)
    | x :: y, [] => !
    | [], x :: y => !
    end.

[Solve Obligations using program_simpl] doesn't solve that remaining 
obligation, but the following does:

  Next Obligation.
    program_simpl.
  Defined.

Is there something fishy going on here, or am I making an incorrect 
assumption?

Clément.

Attachment: signature.asc
Description: OpenPGP digital signature