diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/extratactics.ml4 | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index d0318fb5f6..e6498e02b2 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -370,6 +370,11 @@ TACTIC EXTEND simple_refine | [ "simple" "refine" uconstr(c) ] -> [ refine_tac ist true c ] END +(* Solve unification constraints using heuristics or fail if any remain *) +TACTIC EXTEND solve_constraints +[ "solve_constraints" ] -> [ Refine.solve_constraints ] +END + (**********************************************************************) (* Inversion lemmas (Leminv) *) |