drivers/coq-realize.drv

   1
   2 prelude "(* This file is generated by Why3's Coq-realize driver *)"
   3 prelude "(* Beware! Only edit allowed sections below    *)"
   4
   5 printer "coq-realize"
   6 filename "%t.v"
   7
   8 (* Performed introductions depending on whether counterexamples are
   9    requested, as said by the meta "get_counterexmp". When this meta
  10    set, this transformation introduces the model variables that are
  11    still embedded in the goal. When it is not set, it removes all
  12    these unused-ce-related variables, even in the context.  *)
  13 transformation "counterexamples_dependent_intros"
  14
  15 transformation "inline_trivial"
  16
  17 import "coq-common.gen"