diff options
| author | Pierre-Marie Pédrot | 2020-09-23 12:42:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-21 12:22:12 +0200 |
| commit | bc108fdf6cf42f3ce550f2f258adf7de5fa5bfdc (patch) | |
| tree | 6cf8e0f459ff3630ebd5115773c04bc0bcd70b6c /vernac/himsg.ml | |
| parent | 0a46af10ffc38726207bca952775102d48ad3b15 (diff) | |
Introduce an Ind module in the Names API.
This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.
Diffstat (limited to 'vernac/himsg.ml')
| -rw-r--r-- | vernac/himsg.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 5f7eb78a40..bef9e29ac2 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -656,7 +656,7 @@ let explain_evar_not_found env sigma id = let explain_wrong_case_info env (ind,u) ci = let pi = pr_inductive env ind in - if eq_ind ci.ci_ind ind then + if Ind.CanOrd.equal ci.ci_ind ind then str "Pattern-matching expression on an object of inductive type" ++ spc () ++ pi ++ spc () ++ str "has invalid information." else @@ -1232,7 +1232,7 @@ let error_not_allowed_dependent_analysis env isrec i = pr_inductive env i ++ str "." let error_not_mutual_in_scheme env ind ind' = - if eq_ind ind ind' then + if Ind.CanOrd.equal ind ind' then str "The inductive type " ++ pr_inductive env ind ++ str " occurs twice." else |