aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/field/field.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/field/field.ml4')
-rw-r--r--contrib/field/field.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 5727f1fd7..10e22b86c 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]