lp:~jgross-h/coq/v8.4

Branch merges

This import branch has no branches proposed for merge into it.

No branches dependent on this one.

Related source package recipes

No recipes using this branch. (?)

Create packaging recipe

Related snap packages

Related bugs

Related blueprints

13165. By Hugo Herbelin <email address hidden> on 2017-12-08

Adding support for OCaml 4.06.0 (option -unsafe-string needed).

And other minor changes.

13164. By Hugo Herbelin <email address hidden> on 2017-05-04

Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in batch mode.

13163. By Hugo Herbelin <email address hidden> on 2017-05-04

Adding an option "Set Debug Cbv" for printing visited constants during cbv.

13162. By Pierre-Marie Pédrot <email address hidden> on 2017-04-27

Protecting the '-time' flag from changes in the summary.

This fixes #5478: Module Types break -time in Coq 8.4.

13161. By Hugo Herbelin <email address hidden> on 2017-03-12

Updating a misleading comment in Logic library.

It was implicitly assuming that impredicative Set is the default
option, while it is not the case anymore since Coq 8.0.

Thanks to A.M. for noticing.

13160. By Hugo Herbelin <email address hidden> on 2017-02-25

Fixing a little ennoying approximation in configure when detecting camlp5.

Note: not to be merged beyond 8.4.

13159. By Pierre Letouzey on 2017-02-08

Extraction: adapt the test-suite after 4b1429d (was a fix for #2842)

13158. By Pierre Letouzey on 2017-02-07

Extraction: an extra space forgotten in previous commit

13157. By Pierre Letouzey on 2017-02-04

Extraction: fix complexity issue #5310

  A double call to pp_module_type inside Ocaml.pp_specif was
  causing an complexity blowup when pretty-printing heavily modular
  extracted code.

  I wasn't able to figure out why this double call is there. It could
  be the leftover of some intermediate work in 2007 before commit 350398eae
  (which introduced global printing phases Pre/Impl/Intf).

  Anyway I'm reasonably sure that today these two pp_module_type calls produce
  the exact same pretty-printed signature (even if there's a large bunch of
  imperative states around). Moreover, this duplicated signature is actually
  slightly wrong: when we alias a module M with a unambiguous name like Coq__123,
  the type of Coq__123 should not be an exact copy of the type of M, but rather
  a "strengthened" version of it (with equality between inductive types).
  So the best solution is now to use this funny feature of OCaml introduced in 3.12 :

  module Coq__123 : module type of struct include M end

  This "module type of struct include" is slightly awkward, but short, correct,
  and trivial to produce :-). And I doubt anybody will object to the (rare) use
  of some 3.12 features in extracted code of 2017...

13156. By Nickolai Zeldovich <email address hidden> on 2016-05-04

Fix Haskell extraction for terms over 45 characters long

The Haskell extraction code would allow line-wrapping of the Haskell
type definition, which would lead to unparseable Haskell code when the
linebreak occured just before the type name. In particular, with a term
name of 46 characters or more, the following Coq code:

  Definition xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx := tt.
  Extraction Language Haskell.
  Extraction xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx.

would produce:

  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx ::
  Unit
  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx =
    Tt

which failed to compile with GHC (according to Haskell's indentation
rules, the "Unit" line must be indented to be treated as a continuation
of the previous line).

This patch always forces the type onto a separate line, and ensures that
it is always indented by 2 spaces (just like the body of each definition).