diff options
| author | Hugo Herbelin | 2018-09-04 00:03:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-04 00:03:51 +0200 |
| commit | b40d68fa4fc07a9b585dbd602e94224d6b3f2a7a (patch) | |
| tree | c475991d3bec678e31b95f5b0f791e2aec6535c0 | |
| parent | 8a59612e3043e8b9daa8d3723299e3d721cb492e (diff) | |
| parent | 60f396b240ce1e1a3622ecc512be62a168494efe (diff) | |
Merge PR #8263: Do not abstract over the named variable in unsafe introduction tactic.
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2d02c3ca6e..d536204ec3 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -125,7 +125,7 @@ let unsafe_intro env store decl b = let ninst = mkRel 1 :: inst in let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in - (sigma, mkNamedLambda_or_LetIn decl ev) + (sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) ev) end let introduction id = |