diff options
author | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-28 08:35:06 +0000 |
---|---|---|
committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-28 08:35:06 +0000 |
commit | 97da8221e0097ed365f0a99e4960148424a59734 (patch) | |
tree | 7a0d1b1bc8995dd456b38863674a65230ace957f /plugins/funind/glob_termops.ml | |
parent | 7a10a8a17928df1da29b4f69a2b54ac83a3e1fc3 (diff) |
Remove dynamic stuff from constr_expr and glob_constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/glob_termops.ml')
-rw-r--r-- | plugins/funind/glob_termops.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 0de1104e7..cdd0eaf71 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -183,7 +183,6 @@ let change_vars = GCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t)) | GCast(loc,b,CastCoerce) -> GCast(loc,change_vars mapping b,CastCoerce) - | GDynamic _ -> error "Not handled GDynamic" and change_vars_br mapping ((loc,idl,patl,res) as br) = let new_mapping = List.fold_right Idmap.remove idl mapping in if idmap_is_empty new_mapping @@ -364,7 +363,6 @@ let rec alpha_rt excluded rt = GCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) | GCast (loc,b,CastCoerce) -> GCast(loc,alpha_rt excluded b,CastCoerce) - | GDynamic _ -> error "Not handled GDynamic" | GApp(loc,f,args) -> GApp(loc, alpha_rt excluded f, @@ -414,7 +412,6 @@ let is_free_in id = | GHole _ -> false | GCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t | GCast (_,b,CastCoerce) -> is_free_in b - | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) and is_free_in_br (_,ids,_,rt) = (not (List.mem id ids)) && is_free_in rt in @@ -513,7 +510,6 @@ let replace_var_by_term x_id term = GCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) | GCast(loc,b,CastCoerce) -> GCast(loc,replace_var_by_pattern b,CastCoerce) - | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = if List.exists (fun id -> id_ord id x_id == 0) idl then br @@ -604,7 +600,7 @@ let ids_of_glob_constr c = | GCases (loc,sty,rtntypopt,tml,brchl) -> List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl) | GRec _ -> failwith "Fix inside a constructor branch" - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> [] + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> [] in (* build the set *) List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_glob_constr [] c) @@ -668,7 +664,6 @@ let zeta_normalize = GCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) | GCast(loc,b,CastCoerce) -> GCast(loc,zeta_normalize_term b,CastCoerce) - | GDynamic _ -> raise (UserError("",str "Not handled GDynamic")) and zeta_normalize_br (loc,idl,patl,res) = (loc,idl,patl,zeta_normalize_term res) in @@ -706,7 +701,6 @@ let expand_as = GIf(loc,expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) | GRec _ -> error "Not handled GRec" - | GDynamic _ -> error "Not handled GDynamic" | GCast(loc,b,CastConv(kind,t)) -> GCast(loc,expand_as map b,CastConv(kind,expand_as map t)) | GCast(loc,b,CastCoerce) -> GCast(loc,expand_as map b,CastCoerce) | GCases(loc,sty,po,el,brl) -> |