Fixed bug 12934

CHANGES

 * marks an incompatible change
 
+  o [Coq output] fixed bug 12934: type def with several type params
   o [IDE] interactive detection of provers disabled because incompatible
     with session. Detection must be done with why3config --detect-provers
   o WhyML with mutable record fields and type models

ROADMAP

@@ -42,6 +42,9 @@
    * add "ctrl-S" to save the session explicitly
      (partially done, but no shortcut)
 
+* reload: improve matching of new and old goals by use a kind a distance
+  between some notion of shape of a goal
+
 * Add more examples in the regression tests and in the proval gallery
 
 * prover support
@@ -86,9 +89,6 @@
    - IDE: not necessary to exit to change the input file: just use "reload"
 ** as soon as possible: update why3 output of Why2, release Why 2.30
 
-* fix bug 12934 : Coq syntax
-  https://gforge.inria.fr/tracker/index.php?func=detail&aid=12934&group_id=2990&atid=10293
-
 * increment the magic number in config (A)
 
 * distribute bench files (A + F)
@@ -105,6 +105,9 @@
 * (partially done) update doc for why3replayer
   - not done: parler des examples distribues ci dessus
 
+* DONE fix bug 12934 : Coq syntax
+  https://gforge.inria.fr/tracker/index.php?func=detail&aid=12934&group_id=2990&atid=10293
+
 * DONE document new IDE features (C)
 
 * DONE doc: citer l'article Boogie 2011 quelque part

src/printer/coq.ml

@@ -411,7 +411,7 @@ let print_type_decl ~old info fmt (ts,def) =
               (realization ~old ~def:true) info.realization
         | Some ty ->
             fprintf fmt "@[<hov 2>Definition %a %a :=@ %a.@]@\n@\n"
-              print_ts ts (print_arrow_list print_tv_binder) ts.ts_args
+              print_ts ts (print_list space print_tv_binder) ts.ts_args
               (print_ty info) ty
       end
     | Talgebraic csl ->

tests/bts-12934.why

+
+theory BTS12934
+
+  type set 'a
+
+  type rel 'a 'b = set ('a,'b)
+
+  goal t: true
+
+end