From 33d01606bf5b6e13e4e8fce548ec9935be65a329 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Tue, 16 Feb 2016 11:41:30 -0500
Subject: [PATCH] Harmonize inductive-definition convention

---
 TransitionSystems.v          | 12 ++++++------
 TransitionSystems_template.v | 12 ++++++------
 2 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/TransitionSystems.v b/TransitionSystems.v
index aec831f..4978d1e 100644
--- a/TransitionSystems.v
+++ b/TransitionSystems.v
@@ -301,12 +301,12 @@ Qed.
  * kinds of *local*state* in a thread:
  * - program counter
  * - values of local variables that may be ready eventually *)
-Inductive increment_program : Set :=
-| Lock : increment_program
-| Read : increment_program
-| Write : nat -> increment_program
-| Unlock : increment_program
-| Done : increment_program.
+Inductive increment_program :=
+| Lock
+| Read
+| Write (local : nat)
+| Unlock
+| Done.
 
 (* Next, a type for state shared between threads. *)
 Record inc_state := {
diff --git a/TransitionSystems_template.v b/TransitionSystems_template.v
index 016e79a..8caadd4 100644
--- a/TransitionSystems_template.v
+++ b/TransitionSystems_template.v
@@ -203,12 +203,12 @@ Qed.
  * kinds of *local*state* in a thread:
  * - program counter
  * - values of local variables that may be ready eventually *)
-Inductive increment_program : Set :=
-| Lock : increment_program
-| Read : increment_program
-| Write : nat -> increment_program
-| Unlock : increment_program
-| Done : increment_program.
+Inductive increment_program :=
+| Lock
+| Read
+| Write (local : nat)
+| Unlock
+| Done.
 
 (* Next, a type for state shared between threads. *)
 Record inc_state := {