diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0fbb511a7..2db58978d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -435,7 +435,8 @@ let id_of_name_with_default id = function let hid = Id.of_string "H" let xid = Id.of_string "X" -let default_id_of_sort = function Prop _ -> hid | Type _ -> xid +let default_id_of_sort s = + if Sorts.is_small s then hid else xid let default_id env sigma = function | (name,None,t) -> |