diff options
| author | Gaëtan Gilbert | 2020-11-10 16:52:51 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-16 11:25:07 +0100 |
| commit | bffa084eec75371c7df991c7a88aca5fe65114da (patch) | |
| tree | 451956c20e8c2213039e41b81df9232b0a41ef02 /plugins/ltac | |
| parent | 779d2b915a970cdfc87d3d1b69e10bab04094f33 (diff) | |
Finish fixing setoid rewrite under anonymous lambdas (hopefully)
Fix #13246
Not sure if this is the right thing to do, but it seems to work.
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 26e2b18a02..76a2b6fade 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -13,7 +13,6 @@ open CErrors open Util open Names open Nameops -open Namegen open Constr open Context open EConstr @@ -485,7 +484,7 @@ let rec decompose_app_rel env evd t = let (f', argl, argr) = decompose_app_rel env evd arg in let ty = Retyping.get_type_of env evd argl in let r = Retyping.relevance_of_type env evd ty in - let f'' = mkLambda (make_annot (Name default_dependent_ident) r, ty, + let f'' = mkLambda (make_annot (Name Namegen.default_dependent_ident) r, ty, mkLambda (make_annot (Name (Id.of_string "y")) r, lift 1 ty, mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |]))) in (f'', argl, argr) @@ -1119,7 +1118,14 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = *) | Lambda (n, t, b) when flags.under_lambdas -> - let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in + let unfresh, n' = + let id = match n.binder_name with + | Anonymous -> Namegen.default_dependent_ident + | Name id -> id + in + let id = Tactics.fresh_id_in_env unfresh id env in + Id.Set.add id unfresh, {n with binder_name = Name id} + in let unfresh = match n'.binder_name with | Anonymous -> unfresh | Name id -> Id.Set.add id unfresh |