###############################################################################
# Preliminary notes:                                                          #
# ------------------                                                          #
# Mark "-": change with an impact for users (and possibly developers).        #
# Mark "o": change with an impact for developers only.                        #
# Mark "+": change for Frama-C-commits audience (not in html version)         #
# Mark "*": bug fixed.                                                        #
# Mark "!": change that can break compatibility with existing development.    #
# '#nnn'   : BTS entry #nnn                                                   #
# '#!nnn'  : BTS private entry #nnn                                           #
# For compatibility with old change log formats:                              #
# '#?nnn'  : OLD-BTS entry #nnn                                               #
###############################################################################
# Categories:
#   Cmd: command line interface
#   Gui: graphical user interface
#   Makefile: Makefile
#   WP: proof obligation calculus
#   <Model>: memory model
#   <Prover>: prover
###############################################################################

##########################
Plugin WP 20.0 (Calcium)
##########################

- TIP         [2019/09/17] Using all selected Why-3 provers for proof search
- Gui         [2019/09/17] Updated panel for provers, models, cache, etc.
- WP          [2019/09/12] New cache mechanism for why3 provers, see -wp-cache option
-! WP         [2019/09/17] Deprecated native alt-ergo & coq output, see -wp-prover option
- WP          [2019/09/16] Deprecated & Renamed -wp-script into -wp-coq-script
- WP          [2019/09/16] Deprecated & Renamed -wp-update-script into -wp-update-coq-script
- WP          [2019/09/16] Deprecated & Renamed -wp-tactic into -wp-coq-tactic
- WP          [2019/09/16] Deprecated & Renamed -wp-tryhints into -wp-coq-tryhints
- WP          [2019/09/16] Deprecated & Renamed -wp-hints into -wp-coq-hints
- WP          [2019/09/16] Renamed -wp-why-opt into -wp-why3-opt
- WP          [2019/09/16] Renamed -wp-init-alias into -wp-alias-init
- WP          [2019/09/16] Removed -wp-include
- WP          [2019/09/16] Removed -wp-why3
- WP          [2019/09/16] Removed -wp-why-lib
- WP          [2019/09/16] Removed -wp-depth
- WP          [2019/09/16] Default -wp-extensional changed to true
- WP          [2019/09/16] Default -wp-init-const changed to true
-! WP         [2019/07/05] Default -wp-prover <p> changed to <why3:p> (including default alt-ergo)
-! WP         [2019/07/05] Use native Why3 API (now requires why3 at compile time)
- WP          [2019/06/27] Improving Cint simplifier and quantifier introduction
o Qed         [2019/06/27] More secure API for quantifier management
- Qed         [2019/05/09] Transform (some) boolean quantifications into variable assignments

##########################
Plugin WP 19.0 (Potassium)
##########################

- Wp          [2019/05/09] Fixes -wp-simplify-is-cint simplifier
- Wp          [2019/04/26] Now requires -warn-invalid-bool
- Wp          [2019/04/26] Removed option -wp-bool-range
- Wp          [2019/04/24] Support for Why3 1.* and Coq 8.{7-9}
- Wp          [2019/02/26] Support for @check ACSL annotations
- WP          [2018/02/16] Filter out some variables from separation
- TIP         [2018/02/15] Extend bitwise-eq auto-strategy on hypotheses
- TIP         [2018/02/15] Fix wrong reconciliation of sub-scripts during replay
- Wp          [2018/02/15] Better naming convention, consistent with report-classify
- WP          [2019/02/05] Auto filter properties with name "no_wp:"
- Wp          [2019/01/28] Now -wp-dynamic is set by default (annotation @calls)
- Wp          [2019/01/28] New floating-point model
- Wp          [2018/01/18] Auto-Search mode, see -wp-auto
- TIP         [2018/01/18] Auto-Search mode from the GUI
- TIP         [2018/01/18] New Strategies for bitwise and congruence operations
- TIP         [2017/12/17] Fix bug that makes the TIP wrongly reuse previous results
- Wp          [2017/12/17] Option -wp-print-separation changed into -wp-warn-separation
- Wp          [2017/12/17] Option -wp-unfold-assigns for proving assigns of aggregates field by field
- TIP         [2017/04/25] New tactical Congruence (divisions and products)
- Qed         [2017/10/30] Extends simplifications for lsl,lsr and div
- Wp          [2017/10/27] Fix soundness bug when assigning non-valid ranges
- Qed         [2017/10/27] New simplifications for validity and ranges
- TIP         [2017/10/27] New tacticals for validity and ranges

######################
Plugin WP 18.0 (Argon)
######################

-  Wp         [2018/10/25] Added support for ACSL \offset construct
-  Wp         [2018/09/04] Option -wp-warn-separation changed into -wp-warn-memory-model
                           Adding memory model hypotheses related to pointer validity
-  Wp         [2018/06/28] Use functional havoc instead of a predicate in Typed model
-  Qed        [2018/06/28] Added builtin simplification on array operations
-  Wp         [2018/06/20] Added more simplifications on list operations
-  Qed        [2018/06/20] Added more simplifications for invertible functions
-  TIP        [2018/06/07] Extends tactical 'Split' to distribution of qualitifiers

#########################
Plugin WP Sulfur-20171101
#########################

- Wp         [2017/10/18] Support for LoopCurrent and LoopEntry
- TIP        [2017/04/25] Options -wp-time-{extra|margin} for more stability
-* Gui       [2017/04/25] Fixed bug when running prover from the TIP
- Wp         [2017/04/25] Improved model and simplifications of logical shifts
- Wp         [2017/04/25] New simplification logic functions (-wp-reduce)
- Wp         [2017/04/25] New simplification of unused variables (-wp-parasite)
- Wp         [2017/04/25] New simplification for ground terms (-wp-ground)
- Wp         [2017/04/25] Option -wp-prenex to normalize nested binders
- Wp         [2017/04/25] Option -wp-overflows to add explicit assumptions
- TIP        [2017/04/25] New tactical Overflow (to cope with modulus)
- TIP        [2017/04/25] New tactical Ratio (divisions and products)
- TIP        [2017/04/25] New tactical Bitwised, BitRange and Shift
- TIP        [2017/04/25] New tactical Rewrite (two apply equalities)
- Wp         [2017/03/12] Reduction of equalities with logic functions
- Wp         [2017/03/12] More simplifications wrt integer domains

###########################
Plugin WP Chlorine-20180501
###########################

-  WP         [2018/03/08] Add the missing ACSL math builtins (see manual)
-  WP         [2018/02/12] Experimental support for _Bool range (-wp-bool-range)
-  WP         [2018/03/12] Better handling of \null and (void *)0L
-  WP         [2018/02/16] Allow backtracking when using strategies (-wp-auto-backtrack)
-  WP         [2018/02/16] Filter out some variables from separation
-  TIP        [2018/02/15] Extend bitwise-eq auto-strategy on hypotheses
-  TIP        [2018/02/15] Fix wrong reconciliation of sub-scripts during replay
-  WP         [2018/01/15] Upgrade to Alt-Ergo 2.0.0
-  WP         [2018/01/15] Upgrade to Coq 8.7.1
-  WP         [2018/01/15] Upgrade to Why-3 0.88.3
-  Qed        [2017/12/13] Transforms some quantifications into let constructs
-  WP         [2018/01/18] Auto-Search mode, see -wp-auto
-  TIP        [2018/01/18] Auto-Search mode from the GUI
-  TIP        [2018/01/18] New Strategies for bitwise and congruence operations
-  TIP        [2017/12/17] Fix bug that makes the TIP wrongly reuse previous results
-  WP         [2017/12/17] Option -wp-print-separation changed into -wp-warn-separation
-  WP         [2017/12/17] Option -wp-unfold-assigns for proving assigns of aggregates field by field
-  TIP        [2017/04/25] New tactical Congruence (divisions and products)
-  Qed        [2017/10/30] Extends simplifications for lsl,lsr and div
-  WP         [2017/10/27] Fix soundness bug when assigning non-valid ranges
-  Qed        [2017/10/27] New simplifications for validirt and ranges
-  TIP        [2017/10/27] New tacticals for validity and ranges

#########################
Plugin WP Sulfur-20171101
#########################

- WP          [2017/10/18] Support for LoopCurrent and LoopEntry
- TIP         [2017/04/25] Options -wp-time-{extra|margin} for more stability
-* Gui        [2017/04/25] Fixed bug when running prover from the TIP
- WP          [2017/04/25] Improved model and simplifications of logical shifts
- WP          [2017/04/25] New simplification logic functions (-wp-reduce)
- WP          [2017/04/25] New simplification of unused variables (-wp-parasite)
- WP          [2017/04/25] New simplification for ground terms (-wp-ground)
- WP          [2017/04/25] Option -wp-prenex to normalize nested binders
- WP          [2017/04/25] Option -wp-overflows to add explicit assumptions
- TIP         [2017/04/25] New tactical Overflow (to cope with modulus)
- TIP         [2017/04/25] New tactical Ratio (divisions and products)
- TIP         [2017/04/25] New tactical Bitwised, BitRange and Shift
- TIP         [2017/04/25] New tactical Rewrite (two apply equalities)
- WP          [2017/03/12] Reduction of equalities with logic functions
- WP          [2017/03/12] More simplifications wrt integer domains

#############################
Plugin WP Phosphorus-20170501
#############################

- Qed         [2017/12/13] Transforms some quantifications into let constructs
-  WP         [2017/05/15] Extract inductive predicates as Inductive in Coq
-! WP         [2017/03/24] Remove support for generalized invariants (-wp-invariants)
-o Ergo       [2017/01/12] Update qualif tests to Alt-Ergo 1.30
-  Qed        [2016/12/09] Add E_fun constructor for neutral and absorbent
-  WP         [2016/12/07] Trivial simplification for truncate
-  WP         [2016/12/07] Fix bug on negative 0x float constants
-  WP         [2016/11/04] Improved comparison of logic compounds
-  WP         [2016/11/04] Improved filtering (prevents loss of init clauses)
-  WP         [2016/10/26] Generated HTML API (make wp-doc-api)
-  WP         [2016/10/26] Extensible Proof Engine
-! WP         [2016/10/11] Deprecated Dynamic API
-  WP         [2016/09/20] Improved sequent simplifier
-  Qed        [2016/09/02] Negation of forall/exists qualitifers
-  GUI        [2016/08/26] Pretty-print of memory side effects
-  WP         [2016/08/23] Fixed bug #2246 (unsound switch)
-  Gui        [2016/07/23] Interactive Proof Engine
-  WP         [2016/07/21] Improved Sequent API (Conditions)
-  WP         [2016/05/26] Simplification of ACSL sequences
-  Qed        [2016/05/17] Mutualized type inference in Term
-  Qed        [2016/04/12] Improved simplifiers
-  WP         [2016/11/17] Warn against access to volatile l-values
-  WP         [2016/11/17] Fix volatile access (see -wp-no-volatile)

##########################
Plugin WP Silicon-20161101
##########################

-  WP         [2016/04/08] Unified variable usage for all models
-  WP         [2016/10/06] Simplification of arithmetics models
-  WP         [2016/10/06] Use kernel options -warn-xxx in cint model
-  WP         [2016/10/06] Use cint and cfloat models by default
-  WP         [2016/10/06] Fix -wp-rte with respect to models and kernel options

################################
Plugin WP 1.0 Aluminium_20160502
################################

- Coq         [2016/03/30] Fixed bug #2214 (coq realbase)
- WP	      [2016/03/29] Support for why3 0.87 (and ide)
- WP	      [2016/03/25] Support for Why3 0.86
- WP	      [2016/03/25] Support for Coq 8.5
- WP	      [2016/02/24] Support for Alt-Ergo 1.01
- WP	      [2016/02/18] Fix behavior on ASM code
- WP	      [2016/02/15] Now follows '-safe-arrays' when refining 'p+(..)'
- WP          [2016/02/02] Added support for ACSL let-predicate
-! WP         [2016/01/15] Removed alias '-wp-log' (use '-wp-msg-key' instead)
- WP          [2015/12/16] Strict parsing of -wp-model (stop on error)
- Caveat      [2015/12/02] Separation Hypotheses with -wp-print-separation
- WP          [2015/11/13] Exported OCaml API via Wp.mli
- WP          [2015/11/24] Added support for built-in ACSL lists
- WP	      [2015/11/19] New options to set prover commands
- Coq	      [2015/11/19] Support for Proof General 4.3

################################
Plugin WP 0.9 Magnesium_20151002
################################

- WP	      [2015/09/02] Added support for float-classification.
              (\is_NaN, \is_finite, \is_infinite, \is_plus_infinity, \is_minus_infinity).
-* WP         [2015/09/02] Fixed bug #2082 (crash with \is_infinite).
-* WP         [2015/08/19] Fixed bug #2040 (wrong label Here in assumes).
-* WP         [2015/08/18] Fixed bug #2110 (wrong premisses for structs assigns).
-* WP         [2015/08/18] Fixed bug #2141 (incorrect simplification of 'x%1').
-* WP         [2015/08/18] Fixed bug #2144 (lost \result after explicit assignment).
-* WP         [2015/06/29] Fixed bug #2078 (ill typed PO with void*).
-* WP         [2015/06/29] Fixed bug #2127 (unsigned inequality).
-* WP         [2015/06/29] Fixed bug #2126 (0-shift rewriting).
-* WP         [2015/05/20] Fixed bug #1683 (multiply reported Qed proofs).
-* WP         [2015/03/20] Fixed bug #2079 (incorrect pointer arithmetics).
- WP	      [2015/02/28] Handle global constants (-wp-init-const).
- WP	      [2015/02/28] Quiet output on TTY (see -tty kernel option).
- WP	      [2015/02/28] Added solver mean time to console output.
-* Hoare      [2015/02/28] Fixed incorrect partial assignments in compound objects.
- WP	      [2015/02/28] Refactoring of compound objects modeling.
- Qed	      [2015/02/28] Fold constant expressions in goals.
- Qed	      [2015/02/28] More simplifications on strict inequalities.
- Qed	      [2015/02/28] More aggressive filtering and pruning (-wp-filter).
- Qed	      [2015/02/28] Aggressive ite-lifting.
- Qed	      [2015/02/28] Automatic introduction of existentials.
-! Coq	      [2015/02/28] Inductive if-then-else construct.
- WP	      [2015/02/28] -wp-simplify-type remove some most type constraints (sound, incomplete).
- WP	      [2015/02/28] -wp-simplify-forall of quantifier guards (unsound).
- Qed	      [2015/02/28] Factorization of core equalities (-wp-core).
- WP	      [2015/02/28] Improved -wp-check mode.
-* WP	      [2015/02/28] Fixed bool-prop conversions.
- WP	      [2015/02/28] Summarize initializers (-wp-init-summarize-array).
- WP	      [2015/02/28] Simplifications of 'is_cint' with quantifiers.
- Caveat      [2015/02/28] New 'Caveat' memory model.
- Typed	      [2015/02/28] Named shift operators (better triggers).
- WP          [2015/02/28] New integer model '+rg'.
-* WP	      [2015/02/28] Fixed bug #1683 (duplicate Qed results).
-* WP	      [2015/02/28] Improved typing for alt-ergo let-bindings.
-* WP	      [2015/02/28] Fix sharing bug in proof obligation output.
- Report      [2015/02/28] Support for CVC4 reporting.
-* WP	      [2015/02/28] Fix bugs with -wp-extern-arrays.
- WP 	      [2015/02/28] More lemmas for bitwise operations.
- WP	      [2015/02/28] Options -wp-*-vars to tune memory model detection.
-* WP         [2015/02/18] Fixed bug #1785 (fixed pre-condition with Clang).
- WP	      [2015/01/27] Support for \subset.
- WP	      [2014/09/24] Now accept patterns in drivers.
-* WP	      [2014/09/15] Fixed bug #1828 (separation of locals/formals/heap).

#############################
Plugin WP 0.8 Sodium_20150201
#############################

- WP          [2014/09/05] Drivers for min/max.
- Typed       [2014/09/04] Simplification of assigns and separated.
-* Gui	      [2014/09/04] Fixed bug #1688 (recover results from cmdline).
-! WP         [2014/07/09] Next to the new way the kernel handles command line
	      options, -wp-include +dir has to be replaced by -wp-include ++dir.
	      Forward and backward compatibilities are broken.
- WP          [2014/06/11] Some improvements on bitwise operators.
- Cmd         [2014/05/22] Added option -wp-filename-truncation to truncate
	                   proof obligation filenames.

###########################
Plugin WP 0.8 Neon_20140301
###########################

- Gui	      [2014/01/30] Edition of current proof script (right-click).
- Gui	      [2014/01/30] Consistent icons with status.
- Driver      [2014/01/30] Refactoring of prover external libraries.
	                   (consult driver section in manual).
-* WP         [2014/01/16] Important bug-fix in CFG (missing hyps in goals).
-* WP         [2013/12/11] Major speed-up for huge functions.
- WP          [2014/01/30] Many improvements on reals and floats.
- WP          [2014/01/30] Many improvements on bitwise operators.
- WP          [2014/01/30] Better integration with Why-3 and Coq.
- WP          [2013/12/09] Clever assigns everything with formals and locals.
- WP	      [2013/11/26] More type constraints in typed memory model.

###############################
Plugin WP 0.7 Fluorine_20130501
###############################

-* Typed      [2013/05/23] Better trigger generation for arrays with Alt-Ergo.
-* Provers    [2013/05/23] Fixed various bugs with drivers and provers.
-* WP         [2013/05/23] Fixed various bugs on floats.
-* Typed      [2013/05/23] Fixed bug on address differences and offsets.

###############################
Plugin WP 0.7 Fluorine_20130401
###############################

-* Makefile   [2013/04/17] Fixed bug #1385 about ocamllex.opt.
-! Cmd        [2013/04/15] Removed now useless options -wp-huge, -wp-dot,
	      -wp-trace.
-  Cmd        [2013/04/15] Added option -wp-skip-fct to exclude functions.
-  Cmd        [2013/04/15] Using -wp-prover instead of -wp-proof
	      (kept for compatibility).
-  Gui        [2013/04/15] New Why3 provers selection, added -wp-detect to
	      force detection.
-  WP         [2013/02/29] Added support for string literals (-wp-literals).
-  WP         [2013/02/01] New simplification engine (specific options).
-  WP         [2013/02/01] New interface to model selection (unique
	      -wp-model option).
-  WP         [2013/02/01] Experimental float and machine-integer models.
-  WP         [2013/02/01] 'Store' and 'Runtime' models abandoned.
-  WP         [2013/01/09] 'Typed' becomes the default model.
-  Why3       [2012/12/18] Why3 output (-wp-proof why3:xxx).
-  Typed      [2012/10/23] Extensions of Typed model (unsafe-casts).
-  WP         [2012/10/09] Drivers for linking ACSL symbols to external
	      libs (-wp-driver).

#############################
Plugin WP 0.6 Oxygen_20120901
#############################

-  WP	      [2012/09/14] Experimental simplifier with new 'Typed' model
	      (see manual).
o! WP	      [2012/09/05] Enhanced Ocaml API (see manual). Old bindings
	      are preserved, but now emit a deprecated warning.
-* WP         [2012/07/31] Fixed issue about -ulevel option (bug #1244).
-  WP         [2012/06/30] Truncating too long log filenames.
-  WP         [2012/06/20] Enhanced statistics for -wp-report (see manual).
-* Coq        [2012/05/22] Better translation in Coq for floats and reals
	      (fixed bugs #1174 and #1176).
-  Gui        [2012/05/15] Graphical version of Alt-Ergo (altgr-ergo) can be
	      launched from the 'Proof Obligation Panel'.
-  Cmd	      [2012/03/15] Extended selection language: -wp-prop [+|-][@]id
	      to add or remove property category or name.
-  WP	      [2012/03/06] Better elimination of let constructs for -wp-norm Eqs
	      option.
-  WP         [2012/02/08] Limited support for triggers in axioms and lemmas.
-  Cmd	      [2012/02/03] Extended support for external libraries:
	      Options -wp-coq-lib, -wp-why-lib and now -wp-alt-ergo-lib.

###############################
Plugin WP 0.5 Nitrogen_20111001
###############################

+* Store      [2012/01/03] Adding guard for 'fresh' axiomatization in Store.
+  WP	      [2011/12/23] Timing.
-  Gui	      [2011/12/19] Changes into Gui panel.
-  Cmd	      [2011/12/16] Adding support for reporting with option: -wp-report.
+* WP         [2011/11/25] Fixed bug #!1020 on arbitrary invariants.
-  Cmd        [2011/11/22] Adding support for external proof libraries.
	      See options -wp-include, -wp-tactic, -wp-coq-lib and -wp-why-lib.
-  Cmd	      [2011/11/21] Adding support for multi-provers in command line.

###############################
Plugin WP 0.4 Nitrogen_20111001
###############################

-  WP         [2011/10/24] Further improvement for proof of assigns clauses.
-  WP         [2011/10/14] A warning is now emitted for missing assigns clauses.
+* WP         [2011/09/30] Fixed bug #!572 for logic declaration without
	      'reads' clause.
+* WP         [2011/09/22] Fixed bug #!970 for labels that may escape the
	      control flow.
+* WP         [2011/09/07] Fixed bug #!943 on translation of reals and floats
-  Cmd	      [2011/08/25] Optimization of arguments passing by reference
              with option: -wp-byreference.
-  WP         [2011/09/15] Improvements of conversion between C-integers
	      and Z-integers.
-  WP         [2011/07/22] Optimization of arguments passing by reference.
-  WP         [2011/07/22] Print of formula change.
-  Gui        [2011/06/29] Feedback for proof of preconditions at call sites.
-  Gui        [2011/06/29] New menu options to prove preconditions at one
	      or all call sites.
-  Cmd        [2011/06/17] Added option -wp-proof-trace to obtain more
	      informations from provers when available (option 'Trace' in GUI).
-! Ergo       [2011/06/17] Alt-Ergo is always used with builtin arrays.
	      Removed option -wp-arrays.
-  Vampire    [2011/06/10] Support for Vampire as back-end prover.
-* WP         [2011/06/10] In some cases, a proof attempt could silently
	      failed. It is now properly reported.
-  Gui        [2011/06/07] Default output directory is set to
	      <home>/.frama-c-wp in Gui.
-  Gui        [2011/06/07] Enhancement of Proof-Obligation panel.
-! WP         [2011/05/20] Translation of axioms with labels
	      (removed option -wp-axioms).
+  Caveat     [2011/05/19] Suppression of legacy Caveat model.
-  Hoare      [2011/05/19] New Hoare model
	      (now implemented on top of logic variables).
-  WP         [2011/05/19] Handling partial initializers in C global variables.
-  Cmd        [2011/05/17] New engine to compute proof obligations for
	      arbitrary invariants. See option -wp-invariants.
-! Ergo       [2011/05/17] Alt-Ergo 0.93 now required.
-! Gui	      [2011/05/17] Removed 'Refresh' button from WP panel.
+* Gui 	      [2011/05/17] Fixed bug #!706 : property status not refreshed.
+* Gui	      [2011/05/17] Fixed bug #!707 : unexpected run of wp provers
	      after -then.
+* WP         [2011/05/02] Fixed bug #!708 (missing definitions in
	      environments).
-  WP         [2011/04/29] Alt-Ergo is now selected (and run) by default.
-* WP         [2011/04/29] Fixed problems with -wp-out <dir>.
-  WP         [2011/04/21] Better representation of records and unions in logic.
-  WP         [2011/04/21] No more logic generic pointers. Pointer arithmetics
	      moved to memory models.
-* Store      [2011/04/21] Better representation of pointers (issue #796).
-* Gui        [2011/04/15] Fixed bug on PO status (wrong PO identification).
-* Gui        [2011/04/13] Fixed bug #711 (cyclic dependencies).

#############################
Plugin WP 0.3 Carbon_20110201
#############################

-* Coq        [2011/04/08] Fixed bug #740 for Coq on Windows.
	      WP now uses directly coqtop -compile instead of coqc.
-  Runtime    [2011/04/01] Optimization of effect-assigns.
-* Store      [2011/03/30] Fixed bug #766 about offsets in assigns.
-  Cmd        [2011/03/23] Adding version in -wp-help.
+* WP         [2011/03/10] Proof of requires of the main entry point (bug #675).
-  Cmd        [2011/01/31] Option -wp-warnings to display additional
	      informations for 'Stronger' and 'Degenerated' goals.
-  WP         [2011/01/24] New spliting algorithm. See option -wp-split.
	      Option -wp-split-dim <n> to limit spliting up to 2**n sub-goals.
-  WP         [2011/01/24] When -rte-precond is not used,
	      wp generates a separate proof obligation for each call site.
-  Cmd	      [2011/01/20] Options -wp-status-xxx to refine goal selection
-  Cmd        [2011/01/19] Clarification of -save/-then effect on WP
-* Gui        [2011/01/10] Fixed incorrect property status refresh in the GUI.
-* Coq        [2011/01/04] Fixed bug #702 on Coq output with large integers.
-* WP         [2011/03/10] Proof of requires of the main entry point (bug #675).

#############################
Plugin WP 0.2 Carbon_20101202
#############################

-* Coq        [2010/12/16] Fixed bug #639: no more compilation to shared
	      directory.
-  Gui        [2010/12/16] Accessibility of all provers from gui.

#############################
Plugin WP 0.1 Carbon_20101201
#############################

-  WP         [2010/12/06] New WP plugin.

#############################
