The Coq mailing list

[Frederic GAVA <frederic.gava AT wanadoo.fr>]

Bonjour � tous.
 

J'ai un petit problème de d�veloppement (que je suppose classique mais 
qui me parrait important).

Voilà, j'utilise le type option:

***************************************
Inductive option [A:Set] : Set := 
   None : (option A)
|  Some : A -> (option A). 
***************************************

et j'ai par exemple une liste de "Z option".

Je recherche à avoir la fonction caml suivante:

***************************************
let noSome (Some x) = x;;
***************************************

Bien sur, ceci est impossible en Coq puisqu'il manque le cas "None". Or je 
voudrais
quand même cette fonction car je peux donner la preuve que la donnée est 
belle et bien
un "Some x".

En gros je recherche, dans un "Refine", à utiliser cette fonction pour me 
débarasser des " 'a options"
quand le résultat est prouvé "Some x".

Merci de votre aide.

Frédéric Gava.