Fix extraction of inductive types that Coq auto-detects to be in Prop

 Typical example :

   Inductive t := T : t -> t.

 Earlier, the extraction was using a shortcut to get the sort of t
 (via some mind_arity stuff), but this was producing a less precise
 answer (here InType) than a full Retyping.get_sort_family_of
 (here InProp since t is a singleton type, with no content).
 The extraction of t was hence awkward, since the type of the
 constructor T was computed with the precise method, and its argument
 was optimized out. Now the whole t is considered logical by the
 extraction.

 NB: to avoid this clever but highly non-intuitive behavior of Coq placing
 the above t in Prop, for the moment you have to fix its sort, for instance:

  Inductive t : Set := T : t -> t.

 Using Type instead of Set still activates Coq's minimal sort detection...
 Instead, you could also use one specific TypeX obtained via
 Definition TypeX := Type.

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

0 files changed, 0 insertions, 0 deletions