diff options
| author | Maxime Dénès | 2018-09-11 10:23:02 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-02 16:33:58 +0200 |
| commit | ba63f39be8e26e04e94d1db7fcc534ad5f732871 (patch) | |
| tree | e2ba13e46bed7fd6377c39d6e67a3baa140e177a /plugins/funind/glob_termops.ml | |
| parent | 7803262696980e6f2cb1fd4397b91f1098712647 (diff) | |
Revert #6651: Use r.(p) syntax to print primitive projections
Fixes #6764: Printing Notation regressed compared to 8.7
Diffstat (limited to 'plugins/funind/glob_termops.ml')
| -rw-r--r-- | plugins/funind/glob_termops.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 954fc3bab4..f81de82d5e 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -109,7 +109,6 @@ let change_vars = | GCast(b,c) -> GCast(change_vars mapping b, Glob_ops.map_cast_type (change_vars mapping) c) - | GProj(p,c) -> GProj(p, change_vars mapping c) ) rt and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) = let new_mapping = List.fold_right Id.Map.remove idl mapping in @@ -294,7 +293,6 @@ let rec alpha_rt excluded rt = GApp(alpha_rt excluded f, List.map (alpha_rt excluded) args ) - | GProj(p,c) -> GProj(p, alpha_rt excluded c) in new_rt @@ -346,7 +344,6 @@ let is_free_in id = | GHole _ -> false | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t | GCast (b,CastCoerce) -> is_free_in b - | GProj (_,c) -> is_free_in c ) x and is_free_in_br {CAst.v=(ids,_,rt)} = (not (Id.List.mem id ids)) && is_free_in rt @@ -440,8 +437,6 @@ let replace_var_by_term x_id term = | GCast(b,c) -> GCast(replace_var_by_pattern b, Glob_ops.map_cast_type replace_var_by_pattern c) - | GProj(p,c) -> - GProj(p,replace_var_by_pattern c) ) x and replace_var_by_pattern_br ({CAst.loc;v=(idl,patl,res)} as br) = if List.exists (fun id -> Id.compare id x_id == 0) idl @@ -545,7 +540,6 @@ let expand_as = | GCases(sty,po,el,brl) -> GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) - | GProj(p,c) -> GProj(p, expand_as map c) ) and expand_as_br map {CAst.loc; v=(idl,cpl,rt)} = CAst.make ?loc (idl,cpl, expand_as (List.fold_left add_as map cpl) rt) |