diff options
Diffstat (limited to 'mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 index 6416f85..cc2643a 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 @@ -122,7 +122,7 @@ let prl_term (k, c) = pr_guarded (guard_term k) prl_glob_constr_and_expr c (** Adding a new uninterpreted generic argument type *) let add_genarg tag pr = - let wit = Genarg.make0 None tag in + let wit = Genarg.make0 tag in let glob ist x = (ist, x) in let subst _ x = x in let interp ist x = Ftactic.return x in |