diff options
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 84cb233402..a1db3b78a1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1475,7 +1475,7 @@ let _ = | [VARG_CONSTR c] -> (fun () -> (* by (tactic_com exact c) *) (* on experimente la synthese d'ise dans exact *) - by (dyn_exact [Command c]); + by (dyn_exact_check [Command c]); save_named true) | _ -> assert false) |