Extraction: ad-hoc identifier type with annotations for reductions

 * An inductive constructor Dummy instead of a constant dummy_name
 * The Tmp constructor indicates that the corresponding MLlam or
   MLletin is extraction-specific and can be reduced if possible
 * When inlining a glob (for instance a recursor), we tag some
   lambdas as reducible. In (nat_rect Fo Fs n), the head lams of
   Fo and Fs are treated this way, in order for the recursive call
   inside nat_rect to be correctly pushed as deeper as possible.
 * This way, we can stop allowing by default linear beta/let
   reduction even under binders (can be activated back via
   Set Extraction Flag).
 * Btw, fix the strange definition of non_stricts for (x y).

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

0 files changed, 0 insertions, 0 deletions