diff options
| author |  gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-02 10:01:15 +0000 |
|---|---|---|
| committer | gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-02 10:01:15 +0000 |
| commit | bf578ad5e2f63b7a36aeaef5e0597101db1bd24a (patch) | |
| tree | c0bc4e5f9ae67b8a03b28134dab3dcfe31d184dd /pretyping/rawterm.ml | |
| 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 'pretyping/rawterm.ml')
| -rw-r--r-- | pretyping/rawterm.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index b91531395..dde8490d0 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -70,7 +70,7 @@ type rawconstr = rawconstr array * rawconstr array | RSort of loc * rawsort | RHole of (loc * hole_kind) - | RCast of loc * rawconstr * rawconstr + | RCast of loc * rawconstr * cast_kind * rawconstr | RDynamic of loc * Dyn.t and rawdecl = name * rawconstr option * rawconstr @@ -110,7 +110,7 @@ let map_rawconstr f = function | RRec (loc,fk,idl,bl,tyl,bv) -> RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl, Array.map f tyl,Array.map f bv) - | RCast (loc,c,t) -> RCast (loc,f c,f t) + | RCast (loc,c,k,t) -> RCast (loc,f c,k,f t) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x @@ -184,7 +184,7 @@ let occur_rawconstr id = (na=Name id or not(occur_fix bl)) in occur_fix bl) idl bl tyl bv) - | RCast (loc,c,t) -> (occur c) or (occur t) + | RCast (loc,c,_,t) -> (occur c) or (occur t) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c) @@ -211,7 +211,7 @@ let loc_of_rawconstr = function | RRec (loc,_,_,_,_,_) -> loc | RSort (loc,_) -> loc | RHole (loc,_) -> loc - | RCast (loc,_,_) -> loc + | RCast (loc,_,_,_) -> loc | RDynamic (loc,_) -> loc type 'a raw_red_flag = { |