From 5f2b3fd5c17c29ffc734eef05bdb22b44d015edf Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 11 Jul 2007 21:48:04 +0000
Subject: Slight cleanup of refl_omega.ml : in particular it uses now list
 utilities from Util. Some additions in Util, and simplifications in various
 files.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9969 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2e5ec38c8b..74ea5aef6a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -789,8 +789,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let lf = List.map (fun (id,_,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
-	  try
-	    (list_index iddef lf) -1
+	  try list_index0 iddef lf
           with Not_found ->
 	    raise (InternalisationError (locid,UnboundFixName (false,iddef)))
 	in
@@ -827,8 +826,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let lf = List.map (fun (id,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
-          try 
-	    (list_index iddef lf) -1
+          try list_index0 iddef lf
           with Not_found ->
 	    raise (InternalisationError (locid,UnboundFixName (true,iddef)))
 	in
-- 
cgit v1.2.3