Generalize now works on a list of convertible terms, generalizing all of

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 293bed93c0c75da83e18e8f06770ff0b344753d3..27c6ca17b8ec1915f410256dea436d50c662ddd7 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2292,7 +2292,7 @@ let split = call_tactic ProofEngine.split;;
 let left = call_tactic ProofEngine.left;;
 let right = call_tactic ProofEngine.right;;
 let assumption = call_tactic ProofEngine.assumption;;
-let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
+let generalize = call_tactic_with_goal_inputs ProofEngine.generalize;;
 let absurd = call_tactic_with_input ProofEngine.absurd;;
 let contradiction = call_tactic ProofEngine.contradiction;;
 let decompose =