diff options
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 85d4ac06e..d8c933912 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1780,7 +1780,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,sigma'),EConstr.of_constr c) clp eqpat) sigma') end } (* Derived basic tactics *) |