diff options
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index e63c22bf8..ff1dab46a 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -297,10 +297,10 @@ let build_beq_scheme kn = done; Array.init nb_ind (fun i -> let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in - if not (List.mem InSet kelim) then - raise (NonSingletonProp (kn,i)); - let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in - create_input fix), + if not (Sorts.List.mem InSet kelim) then + raise (NonSingletonProp (kn,i)); + let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in + create_input fix), !eff let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme |