From 73e027a781c1025914749975d341dbab21e2bc45 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 21 Mar 2000 00:03:37 +0000
Subject: Prise en compte nouveau case_info

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@334 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/rawterm.ml  | 4 +---
 pretyping/rawterm.mli | 4 +---
 2 files changed, 2 insertions(+), 6 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index c3f7d8822c..ec43265658 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -30,13 +30,11 @@ type reference =
   | REVar of int * identifier list
   | RMeta of int
 
-type cases_style = PrintLet | PrintIf | PrintCases
-
 type rawconstr = 
   | RRef of loc * reference
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr
-  | RCases of loc * cases_style * rawconstr option * rawconstr list * 
+  | RCases of loc * Term.case_style * rawconstr option * rawconstr list * 
       (identifier list * pattern list * rawconstr) list
   | ROldCase of loc * bool * rawconstr option * rawconstr * 
       rawconstr array
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 8c93eecd9f..c31691046d 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -30,13 +30,11 @@ type reference =
   | REVar of int * identifier list
   | RMeta of int
 
-type cases_style = PrintLet | PrintIf | PrintCases
-
 type rawconstr = 
   | RRef of loc * reference
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr
-  | RCases of loc * cases_style * rawconstr option * rawconstr list * 
+  | RCases of loc * Term.case_style * rawconstr option * rawconstr list * 
       (identifier list * pattern list * rawconstr) list
   | ROldCase of loc * bool * rawconstr option * rawconstr * 
       rawconstr array
-- 
cgit v1.2.3