diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 00:03:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 00:10:03 +0200 |
| commit | c5ecebf6fefbaa673dda506175a2aa4a69d79807 (patch) | |
| tree | e364fd928f247c249767ffb679b0265857327a6a /plugins/funind/glob_termops.ml | |
| parent | 4dc8746cac24ba72a1ec4dfa764a1ae88ce79277 (diff) | |
Revert specific syntax for primitive projections, avoiding ugly
contortions in internalization/externalization. It uses a fully typed
version of detyping, requiring the environment, to move from
primitive projection applications to regular applications of
the eta-expanded version. The kernel is unchanged, and only
constrMatching needs compatibility code now.
Diffstat (limited to 'plugins/funind/glob_termops.ml')
| -rw-r--r-- | plugins/funind/glob_termops.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 4cdea414e..e55ede968 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -180,7 +180,6 @@ let change_vars = | GRec _ -> error "Local (co)fixes are not supported" | GSort _ -> rt | GHole _ -> rt - | GProj _ -> error "Native projections are not supported" (** FIXME *) | GCast(loc,b,c) -> GCast(loc,change_vars mapping b, Miscops.map_cast_type (change_vars mapping) c) @@ -358,7 +357,6 @@ let rec alpha_rt excluded rt = alpha_rt excluded rhs ) | GRec _ -> error "Not handled GRec" - | GProj _ -> error "Native projections are not supported" (** FIXME *) | GSort _ -> rt | GHole _ -> rt | GCast (loc,b,c) -> @@ -409,7 +407,6 @@ let is_free_in id = | GIf(_,cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 | GRec _ -> raise (UserError("",str "Not handled GRec")) - | GProj _ -> error "Native projections are not supported" (** FIXME *) | GSort _ -> false | GHole _ -> false | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t @@ -506,7 +503,6 @@ let replace_var_by_term x_id term = replace_var_by_pattern rhs ) | GRec _ -> raise (UserError("",str "Not handled GRec")) - | GProj _ -> error "Native projections are not supported" (** FIXME *) | GSort _ -> rt | GHole _ -> rt | GCast(loc,b,c) -> @@ -602,7 +598,6 @@ 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" - | GProj _ -> error "Native projections are not supported" (** FIXME *) | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> [] in (* build the set *) @@ -661,7 +656,6 @@ let zeta_normalize = zeta_normalize_term rhs ) | GRec _ -> raise (UserError("",str "Not handled GRec")) - | GProj _ -> error "Native projections are not supported" (** FIXME *) | GSort _ -> rt | GHole _ -> rt | GCast(loc,b,c) -> @@ -704,7 +698,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" - | GProj _ -> error "Native projections are not supported" (** FIXME *) | GCast(loc,b,c) -> GCast(loc,expand_as map b, Miscops.map_cast_type (expand_as map) c) |