MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

Commit 5fa2b7df by Guillaume Melquiond

Break lines after arrows for the Coq printer.

parent 981a9347
 ... ... @@ -7,8 +7,8 @@ Require list.List. Require option.Option. (* Why3 goal *) Definition nth: forall {a:Type} {a_WT:WhyType a}, Z -> (list a) -> (option a). Definition nth: forall {a:Type} {a_WT:WhyType a}, Z -> (list a) -> (option a). intros a a_WT. exact (fix nth n l := match l with nil => None | cons h t => if Zeq_bool n Z0 then Some h else nth (n - 1)%Z t end). Defined. ... ...
 ... ... @@ -32,8 +32,8 @@ now rewrite 2!Map.Select_neq by now apply sym_not_eq. Qed. (* Why3 assumption *) Inductive permut_sub {a:Type} {a_WT:WhyType a} : (@map.Map.map Z _ a a_WT) -> (@map.Map.map Z _ a a_WT) -> Z -> Z -> Prop := Inductive permut_sub {a:Type} {a_WT:WhyType a} : (@map.Map.map Z _ a a_WT) -> (@map.Map.map Z _ a a_WT) -> Z -> Z -> Prop := | permut_refl : forall (a1:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z), ((@permut_sub _ _) a1 a1 l u) | permut_sym : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ ... ...
 ... ... @@ -107,8 +107,8 @@ unfold add, mem; intuition. Qed. (* Why3 goal *) Definition remove: forall {a:Type} {a_WT:WhyType a}, a -> (@set a a_WT) -> (@set a a_WT). Definition remove: forall {a:Type} {a_WT:WhyType a}, a -> (@set a a_WT) -> (@set a a_WT). intros a a_WT x s. exact (fun y => x <> y /\ s y). Defined. ... ...
 ... ... @@ -230,7 +230,7 @@ let print_paren_l fmt x = let print_paren_r fmt x = print_list_delim ~start:lparen_r ~stop:rparen ~sep:comma fmt x let arrow fmt () = fprintf fmt "@ -> " let arrow fmt () = fprintf fmt " ->@ " let print_arrow_list fmt x = print_list_suf arrow fmt x let rec print_pat info fmt p = match p.pat_node with ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!