diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b1e12bd66e..38f9b57e45 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2339,7 +2339,7 @@ let extract_ids env = let scope_of_type_kind sigma = function | IsType -> Notation.current_type_scope_name () | OfType typ -> compute_type_scope sigma typ - | WithoutTypeConstraint -> None + | WithoutTypeConstraint | UnknownIfTermOrType -> None let empty_ltac_sign = { ltac_vars = Id.Set.empty; |