diff options
| author | gregoire | 2005-12-02 10:01:15 +0000 |
|---|---|---|
| committer | gregoire | 2005-12-02 10:01:15 +0000 |
| commit | bf578ad5e2f63b7a36aeaef5e0597101db1bd24a (patch) | |
| tree | c0bc4e5f9ae67b8a03b28134dab3dcfe31d184dd /kernel/term.mli | |
| parent | 825a338a1ddf1685d55bb5193aa5da078a534e1c (diff) | |
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
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 13 |
1 files changed, 9 insertions, 4 deletions
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 |