diff options
Diffstat (limited to 'pretyping/heads.ml')
| -rw-r--r-- | pretyping/heads.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/heads.ml b/pretyping/heads.ml index 870df62500..7740628c21 100644 --- a/pretyping/heads.ml +++ b/pretyping/heads.ml @@ -79,7 +79,7 @@ and kind_of_head env t = | Proj (p,c) -> RigidHead RigidOther | Case (_,_,c,_) -> aux k [] c true - | Int _ -> ConstructorHead + | Int _ | Float _ -> ConstructorHead | Fix ((i,j),_) -> let n = i.(j) in try aux k [] (List.nth l n) true |