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
---
 parsing/g_constr.ml4 | 2 +-
 parsing/g_vernac.ml4 | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 11c9ff48a1..ecb2e132a8 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -44,7 +44,7 @@ let rec index_and_rec_order_of_annot loc bl ann =
     | [_], (None, r) -> Some 0, r
     | lids, (Some x, ro) ->
         let ids = List.map snd lids in
-        (try Some (list_index (snd x) ids - 1), ro
+        (try Some (list_index0 (snd x) ids), ro
         with Not_found ->
           user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable"))
     | _, (None, r) -> None, r
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f7078aa000..c128ff7af2 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -253,7 +253,7 @@ GEXTEND Gram
           let ni =
             match fst annot with
                 Some id ->
-                  (try Some (list_index (Name id) names - 1)
+                  (try Some (list_index0 (Name id) names)
                    with Not_found ->  Util.user_err_loc
                      (loc,"Fixpoint",
                       Pp.str "No argument named " ++ Nameops.pr_id id))
-- 
cgit v1.2.3