Suite du commit 9760 : l'uniformisation du comportement de one_step_reduce,

reduce_to_ind et reduce_to_ref a révélé que ceux-ci pouvaient contourner 
l'opacité des constantes lorsque celles-ci apparaissaient comme argument 
d'un match ou d'un fix (et ce depuis la V5.10 environ). Exemple:

  Definition f (A B:Set) := pair A B. Opaque f.
  Goal fst (f unit unit) -> True. intro H. destruct H. (* bypassed opacity *)

  Definition f (A:Set) := A. Opaque f.
  Goal (f unit) -> True. intro H. destruct H. (* didn't bypass opacity *)

Contourner le statut Opaque quand on recherche un inductif (ce qui est
le rôle de reduce_to_ind) ne paraît pas problématique (et il se trouve
d'ailleurs que CoRN/ftc/TaylorLemma.v en profitait). Ce contournement
de l'opacité a donc été généralisé au cas de constantes arrivant en
tête sans être argument d'un match ou d'un fix.

Contourner le statut Opaque quand on recherche une constante
particulière (ce qui est le rôle général de reduce_to_ref qui est
maintenant le seul à reposer sur one_step_reduce) paraît en revanche
plus douteux. Plus de contournement d'opacité pour reduce_to_ref donc.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9768 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions