aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/tacinterp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 155cb31d85..6ed96c1fb7 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1787,7 +1787,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(TacLetTac(na,c,clp,b,eqpat))
(Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*)
(let_pat_tac b (interp_name ist env sigma na)
- ((sigma,sigma'),c) clp eqpat) sigma')
+ (sigma,c) clp eqpat) sigma')
end }
(* Derived basic tactics *)