diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 9 | ||||
| -rw-r--r-- | vernac/declare.ml | 2 | ||||
| -rw-r--r-- | vernac/himsg.ml | 4 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 2 | ||||
| -rw-r--r-- | vernac/recLemmas.ml | 4 |
5 files changed, 11 insertions, 10 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 7a7e7d6e35..f715459616 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 @@ -496,7 +496,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let u,v = try destruct_ind env sigma tt1 (* trick so that the good sequence is returned*) with e when CErrors.noncritical e -> indu,[||] - in if eq_ind (fst u) ind + in if Ind.CanOrd.equal (fst u) ind then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ] else ( find_scheme bl_scheme_key (fst u) (*FIXME*) >>= fun c -> @@ -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 bc38ba3f6d..3a8ceb0e0f 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/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 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..af72c01758 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 = @@ -70,7 +70,7 @@ let find_mutually_recursive_statements sigma thms = | [], _::_ -> let () = match same_indccl with | ind :: _ -> - if List.distinct_f Names.ind_ord (List.map pi1 ind) + if List.distinct_f Names.Ind.CanOrd.compare (List.map pi1 ind) then Flags.if_verbose Feedback.msg_info (Pp.strbrk |