diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-05 20:16:13 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-05 20:16:13 +0000 |
| commit | 5438bfe94fd1cb0d22de54df53bd0e09328a90a4 (patch) | |
| tree | 2fa81444edfd27a19c24f177ff8797eaf719de98 /contrib/funind/rawtermops.ml | |
| parent | c7a38bc3775f6d29af4c2ea31fdec81725ff6ecc (diff) | |
Move Record desugaring to constrintern and add ability to use notations
for record fields (using "someproj : sometype where not := constr" syntax). Only one
notation allowed currently and no redeclaration after the record
declaration either (will be done for typeclasses).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11542 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind/rawtermops.ml')
| -rw-r--r-- | contrib/funind/rawtermops.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index ffd7cd007..92396af59 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -176,7 +176,6 @@ let change_vars = change_vars mapping lhs, change_vars mapping rhs ) - | RRecord _ -> error "Records are not supported" | RRec _ -> error "Local (co)fixes are not supported" | RSort _ -> rt | RHole _ -> rt @@ -359,7 +358,6 @@ let rec alpha_rt excluded rt = alpha_rt excluded rhs ) | RRec _ -> error "Not handled RRec" - | RRecord _ -> error "Not handled RRecord" | RSort _ -> rt | RHole _ -> rt | RCast (loc,b,CastConv (k,t)) -> @@ -411,7 +409,6 @@ let is_free_in id = | RIf(_,cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 - | RRecord _ -> raise (UserError ("", str "Not handled RRecord")) | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> false | RHole _ -> false @@ -510,7 +507,6 @@ let replace_var_by_term x_id term = replace_var_by_pattern rhs ) | RRec _ -> raise (UserError("",str "Not handled RRec")) - | RRecord _ -> raise (UserError("",str "Not handled RRecord")) | RSort _ -> rt | RHole _ -> rt | RCast(loc,b,CastConv(k,t)) -> @@ -608,8 +604,6 @@ let ids_of_rawterm c = | RCases (loc,sty,rtntypopt,tml,brchl) -> List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl) | RRec _ -> failwith "Fix inside a constructor branch" - | RRecord (loc,w,l) -> Option.cata (ids_of_rawterm []) [] w @ - List.flatten (List.map (fun ((_,id), x) -> id :: ids_of_rawterm [] x) l) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> [] in (* build the set *) @@ -667,7 +661,6 @@ let zeta_normalize = zeta_normalize_term lhs, zeta_normalize_term rhs ) - | RRecord _ -> raise (UserError("",str "Not handled RRecord")) | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> rt | RHole _ -> rt @@ -712,7 +705,6 @@ let expand_as = | RIf(loc,e,(na,po),br1,br2) -> RIf(loc,expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) - | RRecord _ -> error "Not handled RRecord" | RRec _ -> error "Not handled RRec" | RDynamic _ -> error "Not handled RDynamic" | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t)) |