diff options
| -rw-r--r-- | tactics/eqschemes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 0553a14989..51dbd7ecdd 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -60,7 +60,7 @@ open Indrec let hid = id_of_string "H" let xid = id_of_string "X" -let default_id_of_sort = function InProp _ | InSet -> hid | InType _ -> xid +let default_id_of_sort = function InProp | InSet -> hid | InType -> xid let fresh env id = next_global_ident_away id [] let build_dependent_inductive ind (mib,mip) = |