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
---
 parsing/astterm.ml  | 6 ++++++
 parsing/astterm.mli | 2 ++
 toplevel/command.ml | 7 ++++---
 3 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index c2d867ec95..3017a6aee8 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -705,6 +705,12 @@ let interp_sort = function
   | Node(loc,"TYPE", _) -> new_Type_sort ()
   | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >])
 
+let interp_elimination_sort = function
+  | Node(loc,"PROP", []) -> Declarations.ElimOnProp
+  | Node(loc,"SET", [])  -> Declarations.ElimOnSet
+  | Node(loc,"TYPE", _) -> Declarations.ElimOnType
+  | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >])
+
 let judgment_of_rawconstr sigma env c =
   understand_judgment sigma env (interp_rawconstr sigma env c)
 
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 744e75fa56..4503f09a6a 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -26,6 +26,8 @@ val interp_casted_constr : 'a evar_map -> env -> Coqast.t -> constr -> constr
 val interp_type          : 'a evar_map -> env -> Coqast.t -> types
 val interp_sort          : Coqast.t -> sorts
 
+val interp_elimination_sort : Coqast.t -> Declarations.elimination_sorts
+
 val interp_openconstr    :
   'a evar_map -> env -> Coqast.t -> (existential * constr) list * constr
 val interp_casted_openconstr    :
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