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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/btauto/refl_btauto.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/mlutil.ml | 2 | ||||
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 6 |
3 files changed, 5 insertions, 5 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 23f8fe04a3..ac2058ba1b 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -115,7 +115,7 @@ module Bool = struct | Case (info, r, _iv, arg, pats) -> let is_bool = let i = info.ci_ind in - Names.eq_ind i (Lazy.force ind) + Names.Ind.CanOrd.equal i (Lazy.force ind) in if is_bool then Ifb ((aux arg), (aux pats.(0)), (aux pats.(1))) diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index b1ce10985a..21ec80abbc 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -685,7 +685,7 @@ let is_regular_match br = | _ -> raise Impossible in let is_ref i tr = match get_r tr with - | GlobRef.ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1) + | GlobRef.ConstructRef (ind', j) -> Ind.CanOrd.equal ind ind' && Int.equal j (i + 1) | _ -> false in Array.for_all_i is_ref 0 br diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index d464ec4c06..61f90608b1 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -100,7 +100,7 @@ let rec make_form env sigma atom_env term = | Cast(a,_,_) -> make_form env sigma atom_env a | Ind (ind, _) -> - if Names.eq_ind ind (fst (Lazy.force li_False)) then + if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_False)) then Bot else make_atom atom_env (normalize term) @@ -108,11 +108,11 @@ let rec make_form env sigma atom_env term = begin try let ind, _ = destInd sigma hd in - if Names.eq_ind ind (fst (Lazy.force li_and)) then + if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_and)) then let fa = make_form env sigma atom_env argv.(0) in let fb = make_form env sigma atom_env argv.(1) in Conjunct (fa,fb) - else if Names.eq_ind ind (fst (Lazy.force li_or)) then + else if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_or)) then let fa = make_form env sigma atom_env argv.(0) in let fb = make_form env sigma atom_env argv.(1) in Disjunct (fa,fb) |