diff options
Diffstat (limited to 'pretyping/glob_term.ml')
| -rw-r--r-- | pretyping/glob_term.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 10e9d60fd5..44323441b6 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -91,6 +91,7 @@ type 'a glob_constr_r = | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type | GInt of Uint63.t + | GFloat of Float64.t and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g |