From bf578ad5e2f63b7a36aeaef5e0597101db1bd24a Mon Sep 17 00:00:00 2001
From: gregoire
Date: Fri, 2 Dec 2005 10:01:15 +0000
Subject: Changement des named_context Ajout de cast indiquant au kernel la
 strategie a suivre Resolution du bug sur les coinductifs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.mli | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index 9c8f2fa101..70388808ad 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -12,6 +12,7 @@
 open Names
 (*i*)
 
+
 (*s The sorts of CCI. *)
 
 type contents = Pos | Null
@@ -99,9 +100,13 @@ val mkProp : types
 val mkSet  : types
 val mkType : Univ.universe -> types
 
+
+(* This defines the strategy to use for verifiying a Cast *)
+type cast_kind = VMcast | DEFAULTcast 
+
 (* Constructs the term [t1::t2], i.e. the term $t_1$ casted with the 
    type $t_2$ (that means t2 is declared as the type of t1). *)
-val mkCast : constr * types -> constr
+val mkCast : constr * cast_kind * constr -> constr
 
 (* Constructs the product [(x:t1)t2] *)
 val mkProd : name * types * types -> types
@@ -192,7 +197,7 @@ type ('constr, 'types) kind_of_term =
   | Meta      of metavariable
   | Evar      of 'constr pexistential
   | Sort      of sorts
-  | Cast      of 'constr * 'types
+  | Cast      of 'constr * cast_kind * 'types
   | Prod      of name * 'types * 'types
   | Lambda    of name * 'types * 'constr
   | LetIn     of name * 'constr * 'types * 'constr
@@ -213,7 +218,7 @@ val kind_of_term : constr -> (constr, types) kind_of_term
 (* Experimental *)
 type ('constr, 'types) kind_of_type =
   | SortType   of sorts
-  | CastType   of 'types * 'types
+  | CastType   of 'types * 'types 
   | ProdType   of name * 'types * 'types
   | LetInType  of name * 'constr * 'types * 'types
   | AtomicType of 'constr * 'constr array
@@ -258,7 +263,7 @@ val destVar : constr -> identifier
 val destSort : constr -> sorts
 
 (* Destructs a casted term *)
-val destCast : constr -> constr * types
+val destCast : constr -> constr * cast_kind * constr
 
 (* Destructs the product $(x:t_1)t_2$ *)
 val destProd : types -> name * types * types
-- 
cgit v1.2.3