diff options
35 files changed, 74 insertions, 64 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index ef606c9a75..7bb714aa17 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -104,7 +104,7 @@ let check_kelim k1 k2 = Sorts.family_leq k1 k2 let eq_nested_types ty1 ty2 = match ty1, ty2 with | NestedInd ind1, NestedInd ind2 -> eq_ind_chk ind1 ind2 | NestedInd _, _ -> false -| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.equal c1 c2 +| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.CanOrd.equal c1 c2 | NestedPrimitive _, _ -> false let eq_recarg a1 a2 = match a1, a2 with diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 36297fe243..28d23cc67e 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -127,7 +127,7 @@ let isRef sigma c = match kind sigma c with let isRefX sigma x c = let open GlobRef in match x, kind sigma c with - | ConstRef c, Const (c', _) -> Constant.equal c c' + | ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c' | IndRef i, Ind (i', _) -> eq_ind i i' | ConstructRef i, Construct (i', _) -> eq_constructor i i' | VarRef id, Var id' -> Id.equal id id' @@ -514,7 +514,7 @@ let compare_head_gen_proj env sigma equ eqs eqc' nargs m n = | Proj (p, c), App (f, args) | App (f, args), Proj (p, c) -> (match kind f with - | Const (p', u) when Constant.equal (Projection.constant p) p' -> + | Const (p', u) when Environ.QConstant.equal env (Projection.constant p) p' -> let npars = Projection.npars p in if Array.length args == npars + 1 then eqc' 0 c args.(npars) diff --git a/engine/termops.ml b/engine/termops.ml index 467b269e37..3116b03c4f 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1145,7 +1145,7 @@ let compare_constr_univ sigma f cv_pb t1 t2 = Sort s1, Sort s2 -> base_sort_cmp cv_pb (ESorts.kind sigma s1) (ESorts.kind sigma s2) | Prod (_,t1,c1), Prod (_,t2,c2) -> f Reduction.CONV t1 t2 && f cv_pb c1 c2 - | Const (c, u), Const (c', u') -> Constant.equal c c' + | Const (c, u), Const (c', u') -> Constant.CanOrd.equal c c' | Ind (i, _), Ind (i', _) -> eq_ind i i' | Construct (i, _), Construct (i', _) -> eq_constructor i i' | _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2 diff --git a/kernel/constr.ml b/kernel/constr.ml index 1837a39764..fb1e4d12da 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -353,7 +353,7 @@ let isRef c = match kind c with let isRefX x c = let open GlobRef in match x, kind c with - | ConstRef c, Const (c', _) -> Constant.equal c c' + | ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c' | IndRef i, Ind (i', _) -> eq_ind i i' | ConstructRef i, Construct (i', _) -> eq_constructor i i' | VarRef id, Var id' -> Id.equal id id' @@ -954,7 +954,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && List.equal (eq 0) l1 l2 | Const (c1,u1), Const (c2,u2) -> (* The args length currently isn't used but may as well pass it. *) - Constant.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2 + Constant.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2 | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2 | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2 @@ -1442,7 +1442,7 @@ let rec hash t = | Evar (e,l) -> combinesmall 8 (combine (Evar.hash e) (hash_term_list l)) | Const (c,u) -> - combinesmall 9 (combine (Constant.hash c) (Instance.hash u)) + combinesmall 9 (combine (Constant.CanOrd.hash c) (Instance.hash u)) | Ind (ind,u) -> combinesmall 10 (combine (ind_hash ind) (Instance.hash u)) | Construct (c,u) -> diff --git a/kernel/declareops.ml b/kernel/declareops.ml index b9f434f179..ee90ad382b 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -159,7 +159,7 @@ let hcons_const_body cb = let eq_nested_type t1 t2 = match t1, t2 with | NestedInd ind1, NestedInd ind2 -> Names.eq_ind ind1 ind2 | NestedInd _, _ -> false -| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.equal c1 c2 +| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.CanOrd.equal c1 c2 | NestedPrimitive _, _ -> false let eq_recarg r1 r2 = match r1, r2 with diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d751d9875a..2b1a295620 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -472,7 +472,7 @@ let inter_recarg r1 r2 = match r1, r2 with | Nested (NestedInd i1), Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None | Nested (NestedInd _), _ -> None | Nested (NestedPrimitive c1), Nested (NestedPrimitive c2) -> - if Names.Constant.equal c1 c2 then Some r1 else None + if Names.Constant.CanOrd.equal c1 c2 then Some r1 else None | Nested (NestedPrimitive _), _ -> None let inter_wf_paths = Rtree.inter Declareops.eq_recarg inter_recarg Norec @@ -644,7 +644,7 @@ let abstract_mind_lc ntyps npars lc = let is_primitive_positive_container env c = match env.retroknowledge.Retroknowledge.retro_array with - | Some c' when Constant.equal c c' -> true + | Some c' when QConstant.equal env c c' -> true | _ -> false (* [get_recargs_approx env tree ind args] builds an approximation of the recargs @@ -673,7 +673,7 @@ let get_recargs_approx env tree ind args = end | Const (c,_) when is_primitive_positive_container env c -> begin match dest_recarg tree with - | Nested (NestedPrimitive c') when Constant.equal c c' -> + | Nested (NestedPrimitive c') when QConstant.equal env c c' -> build_recargs_nested_primitive ienv tree (c, largs) | _ -> mk_norec end diff --git a/kernel/names.ml b/kernel/names.ml index 592b5e65f7..f987b1d92e 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -529,6 +529,7 @@ module KerPair = struct end module SyntacticOrd = struct + type t = kernel_pair let compare x y = match x, y with | Same knx, Same kny -> KerName.compare knx kny | Dual (knux,kncx), Dual (knuy,kncy) -> diff --git a/kernel/names.mli b/kernel/names.mli index ea137ad1f4..9a01ea2b43 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -341,27 +341,30 @@ sig (** Comparisons *) module CanOrd : sig + type nonrec t = t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int end module UserOrd : sig + type nonrec t = t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int end module SyntacticOrd : sig + type nonrec t = t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int end - val equal : t -> t -> bool + val equal : t -> t -> bool [@@ocaml.deprecated "Use QConstant.equal"] (** Default comparison, alias for [CanOrd.equal] *) - val hash : t -> int + val hash : t -> int [@@ocaml.deprecated "Use QConstant.hash"] (** Hashing function *) val change_label : t -> Label.t -> t @@ -431,27 +434,30 @@ sig (** Comparisons *) module CanOrd : sig + type nonrec t = t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int end module UserOrd : sig + type nonrec t = t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int end module SyntacticOrd : sig + type nonrec t = t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int end - val equal : t -> t -> bool - (** Default comparison, alias for [CanOrd.equal] *) + val equal : t -> t -> bool [@@ocaml.deprecated "Use QMutInd.equal"] + (** Default comparison, alias for [CanOrd.equal] *) - val hash : t -> int + val hash : t -> int [@@ocaml.deprecated "Use QMutInd.hash"] (** Displaying *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index ae070e6f8e..9314203e04 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -67,7 +67,7 @@ let eq_gname gn1 gn2 = | Gind (s1, ind1), Gind (s2, ind2) -> String.equal s1 s2 && eq_ind ind1 ind2 | Gconstant (s1, c1), Gconstant (s2, c2) -> - String.equal s1 s2 && Constant.equal c1 c2 + String.equal s1 s2 && Constant.CanOrd.equal c1 c2 | Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) -> String.equal s1 s2 && eq_ind ind1 ind2 && Int.equal i1 i2 | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2 @@ -98,7 +98,7 @@ let gname_hash gn = match gn with | Gind (s, ind) -> combinesmall 1 (combine (String.hash s) (ind_hash ind)) | Gconstant (s, c) -> - combinesmall 2 (combine (String.hash s) (Constant.hash c)) + combinesmall 2 (combine (String.hash s) (Constant.CanOrd.hash c)) | Gcase (l, i) -> combinesmall 3 (combine (Option.hash Label.hash l) (Int.hash i)) | Gpred (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i)) | Gfixtype (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i)) @@ -148,7 +148,7 @@ let eq_symbol sy1 sy2 = | SymbValue v1, SymbValue v2 -> (=) v1 v2 (** FIXME: how is this even valid? *) | SymbSort s1, SymbSort s2 -> Sorts.equal s1 s2 | SymbName n1, SymbName n2 -> Name.equal n1 n2 - | SymbConst kn1, SymbConst kn2 -> Constant.equal kn1 kn2 + | SymbConst kn1, SymbConst kn2 -> Constant.CanOrd.equal kn1 kn2 | SymbMatch sw1, SymbMatch sw2 -> eq_annot_sw sw1 sw2 | SymbInd ind1, SymbInd ind2 -> eq_ind ind1 ind2 | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2 @@ -162,7 +162,7 @@ let hash_symbol symb = | SymbValue v -> combinesmall 1 (Hashtbl.hash v) (** FIXME *) | SymbSort s -> combinesmall 2 (Sorts.hash s) | SymbName name -> combinesmall 3 (Name.hash name) - | SymbConst c -> combinesmall 4 (Constant.hash c) + | SymbConst c -> combinesmall 4 (Constant.CanOrd.hash c) | SymbMatch sw -> combinesmall 5 (hash_annot_sw sw) | SymbInd ind -> combinesmall 6 (ind_hash ind) | SymbMeta m -> combinesmall 7 m diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index fc6afb79d4..00418009c7 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -83,7 +83,7 @@ and conv_atom env pb lvl a1 a2 cu = if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu else raise NotConvertible | Aconstant (c1,u1), Aconstant (c2,u2) -> - if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 cu + if Constant.CanOrd.equal c1 c2 then convert_instances ~flex:true u1 u2 cu else raise NotConvertible | Asort s1, Asort s2 -> sort_cmp_universes env pb s1 s2 cu diff --git a/kernel/primred.ml b/kernel/primred.ml index f158cfacea..17e5a89b74 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -12,7 +12,7 @@ type _ action_kind = type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn let check_same_types typ c1 c2 = - if not (Constant.equal c1 c2) + if not (Constant.CanOrd.equal c1 c2) then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2)) let check_same_inds ind i1 i2 = diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 96bf370342..f295b36b60 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -283,7 +283,7 @@ let convert_constructors ctor nargs u1 u2 (s, check) = let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else match k1, k2 with - | ConstKey (cst, u), ConstKey (cst', u') when Constant.equal cst cst' -> + | ConstKey (cst, u), ConstKey (cst', u') when Constant.CanOrd.equal cst cst' -> if Univ.Instance.equal u u' then cuniv else let flex = evaluable_constant cst (info_env infos) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 76a1c190be..1a4c786e43 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -182,7 +182,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 begin let kn2' = kn_of_delta reso2 kn2 in if KerName.equal kn2 kn2' || - MutInd.equal (mind_of_delta_kn reso1 kn1) + MutInd.CanOrd.equal (mind_of_delta_kn reso1 kn1) (subst_mind subst2 (MutInd.make kn2 kn2')) then () else error NotEqualInductiveAliases diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index ec8601edc9..42908a7363 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -36,7 +36,7 @@ let eq_reloc_info r1 r2 = match r1, r2 with | Reloc_annot _, _ -> false | Reloc_const c1, Reloc_const c2 -> eq_structured_constant c1 c2 | Reloc_const _, _ -> false -| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2 +| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.CanOrd.equal c1 c2 | Reloc_getglobal _, _ -> false | Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2 | Reloc_proj_name _, _ -> false @@ -48,7 +48,7 @@ let hash_reloc_info r = match r with | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw) | Reloc_const c -> combinesmall 2 (hash_structured_constant c) - | Reloc_getglobal c -> combinesmall 3 (Constant.hash c) + | Reloc_getglobal c -> combinesmall 3 (Constant.CanOrd.hash c) | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p) | Reloc_caml_prim p -> combinesmall 5 (CPrimitives.hash p) diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 2068133b10..28a7abc7c6 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -250,7 +250,7 @@ type id_key = | EvarKey of Evar.t let eq_id_key (k1 : id_key) (k2 : id_key) = match k1, k2 with -| ConstKey c1, ConstKey c2 -> Constant.equal c1 c2 +| ConstKey c1, ConstKey c2 -> Constant.CanOrd.equal c1 c2 | VarKey id1, VarKey id2 -> Id.equal id1 id2 | RelKey n1, RelKey n2 -> Int.equal n1 n2 | EvarKey evk1, EvarKey evk2 -> Evar.equal evk1 evk2 @@ -469,7 +469,7 @@ struct let equal = eq_id_key open Hashset.Combine let hash : t -> tag = function - | ConstKey c -> combinesmall 1 (Constant.hash c) + | ConstKey c -> combinesmall 1 (Constant.CanOrd.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) | EvarKey evk -> combinesmall 4 (Evar.hash evk) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 2dca1d5e49..6869f9c47e 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -741,7 +741,7 @@ and extract_cst_app env sg mle mlt kn args = (* Can we instantiate types variables for this constant ? *) (* In Ocaml, inside the definition of this constant, the answer is no. *) let instantiated = - if lang () == Ocaml && List.mem_f Constant.equal kn !current_fixpoints + if lang () == Ocaml && List.mem_f Constant.CanOrd.equal kn !current_fixpoints then var2var' (snd schema) else instantiation schema in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index f8449bcda1..e56d66ca2d 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -32,7 +32,7 @@ module Refset' = GlobRef.Set_env let occur_kn_in_ref kn = let open GlobRef in function | IndRef (kn',_) - | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' + | ConstructRef ((kn',_),_) -> MutInd.CanOrd.equal kn kn' | ConstRef _ | VarRef _ -> false let repr_of_r = let open GlobRef in function diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index e50c6087bb..73eb943418 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -674,7 +674,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos |Prod _ -> let new_infos = {dyn_infos with info = (f, args)} in build_proof_args env sigma do_finalize new_infos - | Const (c, _) when not (List.mem_f Constant.equal c fnames) -> + | Const (c, _) when not (List.mem_f Constant.CanOrd.equal c fnames) -> let new_infos = {dyn_infos with info = (f, args)} in (* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *) build_proof_args env sigma do_finalize new_infos diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 1ab747ca09..0ab9ac65d7 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -100,8 +100,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in let is_dom c = match Constr.kind c with - | Ind ((u, _), _) -> MutInd.equal u rel_as_kn - | Construct (((u, _), _), _) -> MutInd.equal u rel_as_kn + | Ind ((u, _), _) -> Environ.QMutInd.equal env u rel_as_kn + | Construct (((u, _), _), _) -> Environ.QMutInd.equal env u rel_as_kn | _ -> false in let get_fun_num c = diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 012fcee486..314c8abcaf 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1316,9 +1316,9 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list = let prop_sort = Sorts.InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in + let eq c1 c2 = Environ.QConstant.equal env c1 c2 in List.map - (function - | cst -> List.assoc_f Constant.equal (fst cst) this_block_funs_indexes) + (function cst -> List.assoc_f eq (fst cst) this_block_funs_indexes) funs in let ind_list = @@ -2228,7 +2228,8 @@ let build_case_scheme fa = let prop_sort = Sorts.InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in - List.assoc_f Constant.equal funs this_block_funs_indexes + let eq c1 c2 = Environ.QConstant.equal env c1 c2 in + List.assoc_f eq funs this_block_funs_indexes in let ind, sf = let ind = (first_fun_kn, funs_indexes) in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 5d631aac84..118a917381 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -27,12 +27,13 @@ open Indfun_common *) let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl -> + let env = Proofview.Goal.env gl in let sigma = project gl in let typ = pf_get_hyp_typ hid gl in match EConstr.kind sigma typ with | App (i, args) when isInd sigma i -> let ((kn', num) as ind'), u = destInd sigma i in - if MutInd.equal kn kn' then + if Environ.QMutInd.equal env kn kn' then (* We have generated a graph hypothesis so that we must change it if we can *) let info = match find_Function_of_graph ind' with diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 5ef76dbdc1..3e4a96b10d 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -968,7 +968,7 @@ let fold_match ?(force=false) env sigma c = let unfold_match env sigma sk app = match EConstr.kind sigma app with - | App (f', args) when Constant.equal (fst (destConst sigma f')) sk -> + | App (f', args) when QConstant.equal env (fst (destConst sigma f')) sk -> let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in let v = EConstr.of_constr v in Reductionops.whd_beta env sigma (mkApp (v, args)) diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index cdd15acb0d..bd514f15d5 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -463,8 +463,8 @@ let nb_cs_proj_args pc f u = try match kind f with | Prod _ -> na Prod_cs | Sort s -> na (Sort_cs (Sorts.family s)) - | Const (c',_) when Constant.equal c' pc -> nargs_of_proj u.up_f - | Proj (c',_) when Constant.equal (Projection.constant c') pc -> nargs_of_proj u.up_f + | Const (c',_) when Constant.CanOrd.equal c' pc -> nargs_of_proj u.up_f + | Proj (c',_) when Constant.CanOrd.equal (Projection.constant c') pc -> nargs_of_proj u.up_f | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (fst @@ destRef f)) | _ -> -1 with Not_found -> -1 @@ -508,7 +508,7 @@ let filter_upat i0 f n u fpats = let () = if !i0 < np then i0 := n in (u, np) :: fpats let eq_prim_proj c t = match kind t with - | Proj(p,_) -> Constant.equal (Projection.constant p) c + | Proj(p,_) -> Constant.CanOrd.equal (Projection.constant p) c | _ -> false let filter_upat_FO i0 f n u fpats = diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 419eeaa92a..71ef166ff0 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -244,7 +244,7 @@ let matches_core env sigma allow_bound_rels let open GlobRef in match ref, EConstr.kind sigma c with | VarRef id, Var id' -> Names.Id.equal id id' - | ConstRef c, Const (c',_) -> Constant.equal c c' + | ConstRef c, Const (c',_) -> Environ.QConstant.equal env c c' | IndRef i, Ind (i', _) -> Names.eq_ind i i' | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' | _, _ -> false @@ -307,7 +307,7 @@ let matches_core env sigma allow_bound_rels | PApp (c1,arg1), App (c2,arg2) -> (match c1, EConstr.kind sigma c2 with - | PRef (GlobRef.ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr)) + | PRef (GlobRef.ConstRef r), Proj (pr,c) when not (Environ.QConstant.equal env r (Projection.constant pr)) || Projection.unfolded pr -> raise PatternMatchingFailure | PProj (pr1,c1), Proj (pr,c) -> @@ -324,7 +324,7 @@ let matches_core env sigma allow_bound_rels with Invalid_argument _ -> raise PatternMatchingFailure) | PApp (PRef (GlobRef.ConstRef c1), _), Proj (pr, c2) - when Projection.unfolded pr || not (Constant.equal c1 (Projection.constant pr)) -> + when Projection.unfolded pr || not (Environ.QConstant.equal env c1 (Projection.constant pr)) -> raise PatternMatchingFailure | PApp (c, args), Proj (pr, c2) -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a5311e162d..6a668e79e8 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -566,7 +566,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty in let compare_heads evd = match EConstr.kind evd term, EConstr.kind evd term' with - | Const (c, u), Const (c', u') when Constant.equal c c' -> + | Const (c, u), Const (c', u') when QConstant.equal env c c' -> let u = EInstance.kind evd u and u' = EInstance.kind evd u' in check_strict evd u u' | Const _, Const _ -> UnifFailure (evd, NotSameHead) @@ -844,7 +844,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty ise_try evd [f1; f2] (* Catch the p.c ~= p c' cases *) - | Proj (p,c), Const (p',u) when Constant.equal (Projection.constant p) p' -> + | Proj (p,c), Const (p',u) when QConstant.equal env (Projection.constant p) p' -> let res = try Some (destApp evd (Retyping.expand_projection env evd p c [])) with Retyping.RetypeError _ -> None @@ -855,7 +855,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty appr2 | None -> UnifFailure (evd,NotSameHead)) - | Const (p,u), Proj (p',c') when Constant.equal p (Projection.constant p') -> + | Const (p,u), Proj (p',c') when QConstant.equal env p (Projection.constant p') -> let res = try Some (destApp evd (Retyping.expand_projection env evd p' c' [])) with Retyping.RetypeError _ -> None diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index eaf8c65811..13abf47413 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -206,7 +206,7 @@ let is_array_const env sigma c = | Const (cst,_) -> (match env.Environ.retroknowledge.Retroknowledge.retro_array with | None -> false - | Some cst' -> Constant.equal cst cst') + | Some cst' -> Environ.QConstant.equal env cst cst') | _ -> false let split_as_array env sigma0 = function diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 5be8f9f83c..5ffd919312 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -584,7 +584,7 @@ let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function (List.map (function ((mind',u'),dep',s') -> let (sp',_) = mind' in - if MutInd.equal sp sp' then + if QMutInd.equal env sp sp' then let (mibi',mipi') = lookup_mind_specif env mind' in ((mind',u'),mibi',mipi',dep',s') else diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 9d15e98373..d94cae75bd 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -82,7 +82,7 @@ type evaluable_reference = | EvalEvar of EConstr.existential let evaluable_reference_eq sigma r1 r2 = match r1, r2 with -| EvalConst c1, EvalConst c2 -> Constant.equal c1 c2 +| EvalConst c1, EvalConst c2 -> Constant.CanOrd.equal c1 c2 | EvalVar id1, EvalVar id2 -> Id.equal id1 id2 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) -> @@ -995,7 +995,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c = | CoFix _ | Fix _ -> s' | Proj (p,t) when (match EConstr.kind sigma constr with - | Const (c', _) -> Constant.equal (Projection.constant p) c' + | Const (c', _) -> Constant.CanOrd.equal (Projection.constant p) c' | _ -> false) -> let npars = Projection.npars p in if List.length stack <= npars then @@ -1101,7 +1101,7 @@ let contextually byhead occs f env sigma t = let match_constr_evaluable_ref sigma c evref = match EConstr.kind sigma c, evref with - | Const (c,u), EvalConstRef c' when Constant.equal c c' -> Some u + | Const (c,u), EvalConstRef c' when Constant.CanOrd.equal c c' -> Some u | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty | _, _ -> None diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ccfb508964..08303c80d6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -547,10 +547,10 @@ let oracle_order env cf1 cf2 = | Some k2 -> match k1, k2 with | IsProj (p, _), IsKey (ConstKey (p',_)) - when Constant.equal (Projection.constant p) p' -> + when Environ.QConstant.equal env (Projection.constant p) p' -> Some (not (Projection.unfolded p)) | IsKey (ConstKey (p,_)), IsProj (p', _) - when Constant.equal p (Projection.constant p') -> + when Environ.QConstant.equal env p (Projection.constant p') -> Some (Projection.unfolded p') | _ -> Some (Conv_oracle.oracle_order (fun x -> x) @@ -796,7 +796,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c) (* Fast path for projections. *) - | Proj (p1,c1), Proj (p2,c2) when Constant.equal + | Proj (p1,c1), Proj (p2,c2) when Environ.QConstant.equal env (Projection.constant p1) (Projection.constant p2) -> (try unify_same_proj curenvnb cv_pb {opt with at_top = true} substn c1 c2 @@ -914,7 +914,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e match EConstr.kind sigma c' with | Meta _ -> true | Evar _ -> true - | Const (c, u) -> Constant.equal c (Projection.constant p) + | Const (c, u) -> Environ.QConstant.equal env c (Projection.constant p) | _ -> false in let expand_proj c c' l = diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 0b13f4763a..bec9ede6f1 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -225,7 +225,7 @@ struct let equal_cst_member x y = match x, y with | Cst_const (c1,u1), Cst_const (c2, u2) -> - Constant.equal c1 c2 && Univ.Instance.equal u1 u2 + Constant.CanOrd.equal c1 c2 && Univ.Instance.equal u1 u2 | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2 | _, _ -> false in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a607c09010..f3ecc2a9f0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -540,7 +540,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl -> | (f, n, ar) :: oth -> let open Context.Named.Declaration in let (sp', u') = check_mutind env sigma n ar in - if not (MutInd.equal sp sp') then + if not (QMutInd.equal env sp sp') then error "Fixpoints should be on the same mutual inductive declaration."; if mem_named_context_val f sign then user_err ~hdr:"Logic.prim_refiner" diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 7a7e7d6e35..475d4e9af9 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -145,7 +145,7 @@ let build_beq_scheme_deps kn = | Cast (x,_,_) -> aux accu (Term.applist (x,a)) | App _ -> assert false | Ind ((kn', _), _) -> - if MutInd.equal kn kn' then accu + if Environ.QMutInd.equal env kn kn' then accu else let eff = SchemeMutualDep (kn', !beq_scheme_kind_aux ()) in List.fold_left aux (eff :: accu) a @@ -253,7 +253,7 @@ let build_beq_scheme mode kn = | Cast (x,_,_) -> aux (Term.applist (x,a)) | App _ -> assert false | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> - if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1) + if Environ.QMutInd.equal env kn kn' then mkRel(eqA-nlist-i+nb_ind-1) else begin try let eq = match lookup_scheme (!beq_scheme_kind_aux()) ind' with @@ -539,7 +539,8 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.") end end >>= fun (sp2,i2) -> - if not (MutInd.equal sp1 sp2) || not (Int.equal i1 i2) + Proofview.tclENV >>= fun env -> + if not (Environ.QMutInd.equal env sp1 sp2) || not (Int.equal i1 i2) then Tacticals.New.tclZEROMSG (str "Eq should be on the same type") else aux (Array.to_list ca1) (Array.to_list ca2) diff --git a/vernac/declare.ml b/vernac/declare.ml index 5274a6da3b..7d0c5ee48f 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -162,7 +162,7 @@ let cache_constant ((sp,kn), obj) = then Constant.make1 kn else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(Libnames.basename sp) ++ str".") in - assert (Constant.equal kn' (Constant.make1 kn)); + assert (Environ.QConstant.equal (Global.env ()) kn' (Constant.make1 kn)); Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn)); Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 356ccef06b..de72a30f18 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -405,7 +405,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = let get_common_underlying_mutual_inductive env = function | [] -> assert false | (id,(mind,i as ind))::l as all -> - match List.filter (fun (_,(mind',_)) -> not (MutInd.equal mind mind')) l with + match List.filter (fun (_,(mind',_)) -> not (Environ.QMutInd.equal env mind mind')) l with | (_,ind')::_ -> raise (RecursionSchemeError (env, NotMutualInScheme (ind,ind'))) | [] -> diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml index 534c358a3f..79468627de 100644 --- a/vernac/recLemmas.ml +++ b/vernac/recLemmas.ml @@ -44,7 +44,7 @@ let find_mutually_recursive_statements sigma thms = [] in ind_hyps,ind_ccl) thms in let inds_hyps,ind_ccls = List.split inds in - let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> Names.MutInd.equal kn kn' in + let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> Environ.QMutInd.equal (Global.env ()) kn kn' in (* Check if all conclusions are coinductive in the same type *) (* (degenerated cartesian product since there is at most one coind ccl) *) let same_indccl = |