diff options
Diffstat (limited to 'src/SMT_terms.v')
| -rw-r--r-- | src/SMT_terms.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/SMT_terms.v b/src/SMT_terms.v index 169c761..a85804c 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -489,8 +489,8 @@ Module Typ. | Cast (k: forall P, P A -> P B) | NoCast. - Implicit Arguments Cast [A B]. - Implicit Arguments NoCast [A B]. + Arguments Cast {A B} k. + Arguments NoCast {A B}. Notation idcast := (Cast (fun P x => x)). (* La fonction cast calcule cast_result *) |