1 files changed, 41 insertions, 42 deletions

diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v
index e2bd0c5378..d50df9776f 100644
--- a/contrib/ring/Quote.v
+++ b/contrib/ring/Quote.v
@@ -32,54 +32,53 @@ Section variables_map.
 Variable A : Type.
 
 Inductive varmap : Type :=
-  Empty_vm : varmap
-| Node_vm : A->varmap->varmap->varmap.
-
-Inductive index : Set := 
-| Left_idx : index -> index
-| Right_idx : index -> index
-| End_idx : index
-.
-
-Fixpoint varmap_find [default_value:A; i:index; v:varmap] : A :=
-  Cases i v of
-    End_idx (Node_vm x _ _) => x
-  | (Right_idx i1) (Node_vm x v1 v2) => (varmap_find default_value i1 v2)
-  | (Left_idx i1) (Node_vm x v1 v2) => (varmap_find default_value i1 v1)
-  | _ _ => default_value
+  | Empty_vm : varmap
+  | Node_vm : A -> varmap -> varmap -> varmap.
+
+Inductive index : Set :=
+  | Left_idx : index -> index
+  | Right_idx : index -> index
+  | End_idx : index.
+
+Fixpoint varmap_find (default_value:A) (i:index) (v:varmap) {struct v} : A :=
+  match i, v with
+  | End_idx, Node_vm x _ _ => x
+  | Right_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v2
+  | Left_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v1
+  | _, _ => default_value
   end.
 
-Fixpoint index_eq [n,m:index] : bool :=
-  Cases n m of
-  | End_idx End_idx => true
-  | (Left_idx n') (Left_idx m') => (index_eq n' m')
-  | (Right_idx n') (Right_idx m') => (index_eq n' m')
-  | _ _ => false
+Fixpoint index_eq (n m:index) {struct m} : bool :=
+  match n, m with
+  | End_idx, End_idx => true
+  | Left_idx n', Left_idx m' => index_eq n' m'
+  | Right_idx n', Right_idx m' => index_eq n' m'
+  | _, _ => false
   end.
 
-Fixpoint index_lt[n,m:index] : bool :=
-  Cases n m of
-  | End_idx (Left_idx _) => true
-  | End_idx (Right_idx _) => true
-  | (Left_idx n') (Right_idx m') => true
-  | (Right_idx n') (Right_idx m') => (index_lt n' m') 
-  | (Left_idx n') (Left_idx m') => (index_lt n' m') 
-  | _ _ => false
+Fixpoint index_lt (n m:index) {struct m} : bool :=
+  match n, m with
+  | End_idx, Left_idx _ => true
+  | End_idx, Right_idx _ => true
+  | Left_idx n', Right_idx m' => true
+  | Right_idx n', Right_idx m' => index_lt n' m'
+  | Left_idx n', Left_idx m' => index_lt n' m'
+  | _, _ => false
   end.
 
-Lemma index_eq_prop : (n,m:index)(index_eq n m)=true -> n=m.
-  Induction n; Induction m; Simpl; Intros.
-  Rewrite (H i0 H1); Reflexivity.
-  Discriminate.
-  Discriminate.
-  Discriminate.
-  Rewrite (H i0 H1); Reflexivity.
-  Discriminate.
-  Discriminate.
-  Discriminate.
-  Reflexivity.
-Save.
+Lemma index_eq_prop : forall n m:index, index_eq n m = true -> n = m.
+  simple induction n; simple induction m; simpl in |- *; intros.
+  rewrite (H i0 H1); reflexivity.
+  discriminate.
+  discriminate.
+  discriminate.
+  rewrite (H i0 H1); reflexivity.
+  discriminate.
+  discriminate.
+  discriminate.
+  reflexivity.
+Qed.
 
 End variables_map.
 
-Unset Implicit Arguments.
+Unset Implicit Arguments.
\ No newline at end of file