diff options
| author | Pierre-Marie Pédrot | 2019-05-01 17:00:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-10 12:53:09 +0200 |
| commit | f7c55014aabb0d607449868e2522515db0b40568 (patch) | |
| tree | 16fc97ca5dcc475115b059a40425f10f0f53c5fa /user-contrib | |
| parent | a5a89e8b623cd5822f59b854a45efc8236ae0087 (diff) | |
Make the check flag of conversion functions mandatory.
The current situation is a mess, some functions set it by default, but other
no. Making it mandatory ensures that the expected value is the correct one.
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/tac2tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml index 603e00c815..a8c1a67f6f 100644 --- a/user-contrib/Ltac2/tac2tactics.ml +++ b/user-contrib/Ltac2/tac2tactics.ml @@ -167,7 +167,7 @@ let change pat c cl = delayed_of_tactic (Tac2ffi.app_fun1 c (array constr) constr subst) env sigma in let cl = mk_clause cl in - Tactics.change pat c cl + Tactics.change ~check:true pat c cl end let rewrite ev rw cl by = |