aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacinterp.ml')
-rw-r--r--tactics/tacinterp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2055bd7ea..d05f5f8ad 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -681,7 +681,7 @@ let interp_may_eval f ist env sigma = function
| ConstrEval (r,c) ->
let (sigma,redexp) = interp_red_expr ist env sigma r in
let (sigma,c_interp) = f ist env sigma c in
- sigma , (fst (Redexpr.reduction_of_red_expr env redexp) env sigma c_interp)
+ (fst (Redexpr.reduction_of_red_expr env redexp) env sigma c_interp)
| ConstrContext ((loc,s),c) ->
(try
let (sigma,ic) = f ist env sigma c in