diff options
| -rw-r--r-- | contrib/field/field.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 5727f1fd7e..10e22b86c8 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -122,7 +122,7 @@ let field g = <:tactic< Match Context With | [|- (eq ?1 ?2 ?3)] -> - Let t = (eqT ?1 ?2 ?3) In + Let t = '(eqT ?1 ?2 ?3) In Cut t;[Intro; (Match Context With | [id:t |- ?] -> Rewrite id;Reflexivity)|Field_Gen FT] |