diff options
| -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 = |