From 217cdd9aefb0b2cb822d8be7ba8c85de39aef2dd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 10 Sep 2001 12:37:15 +0000
Subject: Utilisation d'un type spécifique (elimination_sorts) pour
 caractériser les éliminations, pour éviter les collisions avec les univers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1946 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'toplevel/command.ml')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index b3a34e2ce6..5620473fe5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -398,9 +398,10 @@ let build_scheme lnamedepindsort =
   and sigma = Evd.empty
   and env0 = Global.env() in
   let lrecspec =
-    List.map (fun (_,dep,indid,sort) -> 
-                let s = destSort (interp_constr sigma env0 sort) in
-                (inductive_of_ident indid,dep,s)) lnamedepindsort
+    List.map
+      (fun (_,dep,indid,sort) -> 
+         (inductive_of_ident indid,dep,interp_elimination_sort sort)) 
+      lnamedepindsort
   in
   let n = NeverDischarge in 
   let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in 
-- 
cgit v1.2.3