diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-11 18:48:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-11 18:48:01 +0200 |
| commit | f8658b06b98e59e7f6397c6082e4b9b399499948 (patch) | |
| tree | 61e1d3203c80619d8282551b39aebbedad675939 /tactics | |
| parent | cd9a2e9e59d87801790859ddd26d225d71be7f7c (diff) | |
Fixing bug #4366: Conversion tactics recheck uselessly convertibility.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b113ed31e..0d6a26a11 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -726,12 +726,11 @@ let reduction_clause redexp cl = let reduce redexp cl goal = let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in let redexps = reduction_clause redexp cl in + let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in let tac = tclMAP (fun (where,redexp) -> - e_reduct_option ~check:true + e_reduct_option ~check (Redexpr.reduction_of_red_expr (pf_env goal) redexp) where) redexps in - match redexp with - | Fold _ | Pattern _ -> with_check tac goal - | _ -> tac goal + if check then with_check tac goal else tac goal (* Unfolding occurrences of a constant *) |