From c1cab3ba606f7034f2785f06c0d3892bca3976cf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 18 Aug 2017 11:36:05 +0200
Subject: Removing cumbersome location in multiple patterns.

This is to have a better symmetry between CCases and GCases.
---
 pretyping/cases.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4f3669a2b9..1207c967b5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1566,11 +1566,9 @@ substituer après par les initiaux *)
 
 (* builds the matrix of equations testing that each eqn has n patterns
  * and linearizing the _ patterns.
- * Syntactic correctness has already been done in astterm *)
+ * Syntactic correctness has already been done in constrintern *)
 let matx_of_eqns env eqns =
-  let build_eqn (loc,(ids,lpat,rhs)) =
-    let initial_lpat,initial_rhs = lpat,rhs in
-    let initial_rhs = rhs in
+  let build_eqn (loc,(ids,initial_lpat,initial_rhs)) =
     let avoid = ids_of_named_context_val (named_context_val env) in
     let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in
     let rhs =
-- 
cgit v1.2.3