Make sure "Print Module" write a dot at the end of inductive definitions.

8 files changed, 36 insertions, 19 deletions

diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index e46774f68a..9fd846ac16 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -11,7 +11,7 @@ eq_refl
      : ?y = ?y
 where
 ?y : [ |- nat]
-Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x.
 
 Arguments eq {A}%type_scope _ _
 Arguments eq_refl {B}%type_scope {y}, [_] _
@@ -22,7 +22,7 @@ eq_refl is not universe polymorphic
 Arguments eq_refl {B}%type_scope {y}, [_] _
   (where some original arguments have been renamed)
 Expands to: Constructor Coq.Init.Logic.eq_refl
-Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x
+Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x.
 
 Arguments myEq _%type_scope _ _
 Arguments myrefl {C}%type_scope x _
@@ -55,7 +55,7 @@ Expands to: Constant Arguments_renaming.Test1.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 Inductive myEq (A B : Type) (x : A) : A -> Prop :=
-    myrefl : B -> myEq A B x x
+    myrefl : B -> myEq A B x x.
 
 Arguments myEq (_ _)%type_scope _ _
 Arguments myrefl A%type_scope {C}%type_scope x _
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index 8e10107673..fc3b6fbd99 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -5,7 +5,7 @@ A : Set
 a : A
 l : list' A
 Unable to unify "list' (A * A)%type" with "list' A".
-Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
+Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x.
 
 Arguments foo _%type_scope _
 Arguments Foo _%type_scope _
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index 02e58775b5..fdd609f5b2 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,5 +1,5 @@
 Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
-    exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}
+    exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}.
 
 Arguments sig2 [A]%type_scope (_ _)%type_scope
 Arguments exist2 [A]%type_scope (_ _)%function_scope _ _ _
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index fe16dba496..03b9e3b527 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -4,14 +4,14 @@ existT is template universe polymorphic on sigT.u0 sigT.u1
 Arguments existT [A]%type_scope _%function_scope _ _
 Expands to: Constructor Coq.Init.Specif.existT
 Inductive sigT (A : Type) (P : A -> Type) : Type :=
-    existT : forall x : A, P x -> {x : A & P x}
+    existT : forall x : A, P x -> {x : A & P x}.
 
 Arguments sigT [A]%type_scope _%type_scope
 Arguments existT [A]%type_scope _%function_scope _ _
 existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 Argument A is implicit
-Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x.
 
 Arguments eq {A}%type_scope _ _
 Arguments eq_refl {A}%type_scope {x}, [_] _
@@ -50,7 +50,7 @@ Arguments plus_n_O _%nat_scope
 plus_n_O is opaque
 Expands to: Constant Coq.Init.Peano.plus_n_O
 Inductive le (n : nat) : nat -> Prop :=
-    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
+    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m.
 
 Arguments le (_ _)%nat_scope
 Arguments le_n _%nat_scope
@@ -60,7 +60,7 @@ comparison : Set
 comparison is not universe polymorphic
 Expands to: Inductive Coq.Init.Datatypes.comparison
 Inductive comparison : Set :=
-    Eq : comparison | Lt : comparison | Gt : comparison
+    Eq : comparison | Lt : comparison | Gt : comparison.
 bar : foo
 
 bar is not universe polymorphic
@@ -78,7 +78,7 @@ Arguments bar {x}
 Module Coq.Init.Peano
 Notation sym_eq := eq_sym
 Expands to: Notation Coq.Init.Logic.sym_eq
-Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x.
 
 Arguments eq {A}%type_scope _ _
 Arguments eq_refl {A}%type_scope {x}, {_} _
diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
index 1a9bc068c5..7c7600b786 100644
--- a/test-suite/output/PrintModule.out
+++ b/test-suite/output/PrintModule.out
@@ -7,3 +7,11 @@ Module N : S with Module T := K := M
 Module N : S with Module T := M
 
 Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End
+Module
+A
+:= Struct
+     Variant I : Set :=  C : nat -> I.
+     Record R : Set := Build_R { n : nat }.
+     Definition n : R -> nat.
+   End
+
diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
index 54ef305be4..b4de03b556 100644
--- a/test-suite/output/PrintModule.v
+++ b/test-suite/output/PrintModule.v
@@ -60,3 +60,10 @@ Print Func.
 End Shortest_path.
 
 End QUX.
+
+Module A.
+Variant I := C : nat -> I.
+Record R := { n : nat }.
+End A.
+
+Print Module A.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 95b6c6ee95..4993b747fa 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -1,6 +1,7 @@
-Inductive Empty@{uu} : Type@{uu} :=  
+Inductive Empty@{uu} : Type@{uu} :=  .
 (* uu |=  *)
-Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap { punwrap : A }
+Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap
+  { punwrap : A }.
 (* uu |=  *)
 
 PWrap has primitive projections with eta conversion.
@@ -12,7 +13,8 @@ fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p
 (* uu |=  *)
 
 Arguments punwrap _%type_scope _
-Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap { runwrap : A }
+Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap
+  { runwrap : A }.
 (* uu |=  *)
 
 Arguments RWrap _%type_scope
@@ -80,9 +82,9 @@ foo@{uu u v} =
 Type@{u} -> Type@{v} -> Type@{uu}
      : Type@{max(uu+1,u+1,v+1)}
 (* uu u v |=  *)
-Inductive Empty@{E} : Type@{E} :=  
+Inductive Empty@{E} : Type@{E} :=  .
 (* E |=  *)
-Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
+Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }.
 (* E |=  *)
 
 PWrap has primitive projections with eta conversion.
@@ -107,7 +109,7 @@ insec@{v} = Type@{uu} -> Type@{v}
      : Type@{max(uu+1,v+1)}
 (* v |=  *)
 Inductive insecind@{k} : Type@{k+1} :=
-    inseccstr : Type@{k} -> insecind@{k}
+    inseccstr : Type@{k} -> insecind@{k}.
 (* k |=  *)
 
 Arguments inseccstr _%type_scope
@@ -115,7 +117,7 @@ insec@{uu v} = Type@{uu} -> Type@{v}
      : Type@{max(uu+1,v+1)}
 (* uu v |=  *)
 Inductive insecind@{uu k} : Type@{k+1} :=
-    inseccstr : Type@{k} -> insecind@{uu k}
+    inseccstr : Type@{k} -> insecind@{uu k}.
 (* uu k |=  *)
 
 Arguments inseccstr _%type_scope
diff --git a/vernac/printmod.ml b/vernac/printmod.ml
index fdf7f6c74a..ba4a7857e7 100644
--- a/vernac/printmod.ml
+++ b/vernac/printmod.ml
@@ -124,7 +124,7 @@ let print_mutual_inductive env mind mib udecl =
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   hov 0 (def keyword ++ spc () ++
          prlist_with_sep (fun () -> fnl () ++ str"  with ")
-           (print_one_inductive env sigma mib) inds ++
+           (print_one_inductive env sigma mib) inds ++ str "." ++
          Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes)
 
 let get_fields =
@@ -173,7 +173,7 @@ let print_record env mind mib udecl =
       prlist_with_sep (fun () -> str ";" ++ brk(2,0))
         (fun (id,b,c) ->
           Id.print id ++ str (if b then " : " else " := ") ++
-          Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
+          Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }." ++
     Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes
   )