diff options
Diffstat (limited to 'contrib/first-order/ground.ml4')
| -rw-r--r-- | contrib/first-order/ground.ml4 | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml4 index 914b209f12..054b28a070 100644 --- a/contrib/first-order/ground.ml4 +++ b/contrib/first-order/ground.ml4 @@ -185,8 +185,10 @@ END TACTIC EXTEND GIntuition ["GIntuition" tactic(t)] -> - [ gen_ground_tac false (Some(snd t)) [] ] + [ gen_ground_tac false + (Some(tclTHEN normalize_evaluables (snd t))) [] ] | [ "GIntuition" ] -> - [ gen_ground_tac false None [] ] + [ gen_ground_tac false + (Some (tclTHEN normalize_evaluables default_solver)) [] ] END |