aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/base_include6
-rw-r--r--dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh9
-rw-r--r--dev/top_printers.ml2
-rw-r--r--dev/top_printers.mli2
-rw-r--r--interp/constrextern.ml2
-rw-r--r--interp/notation.ml2
-rw-r--r--interp/notation.mli2
-rw-r--r--plugins/firstorder/ground.ml4
-rw-r--r--plugins/ssr/ssrvernac.mlg6
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/coercionops.ml (renamed from pretyping/classops.ml)0
-rw-r--r--pretyping/coercionops.mli (renamed from pretyping/classops.mli)0
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--pretyping/pretyping.mllib2
-rw-r--r--vernac/comAssumption.ml4
-rw-r--r--vernac/comCoercion.ml (renamed from vernac/class.ml)4
-rw-r--r--vernac/comCoercion.mli (renamed from vernac/class.mli)2
-rw-r--r--vernac/comInductive.ml2
-rw-r--r--vernac/prettyp.ml6
-rw-r--r--vernac/prettyp.mli2
-rw-r--r--vernac/record.ml6
-rw-r--r--vernac/vernac.mllib2
-rw-r--r--vernac/vernacentries.ml14
23 files changed, 47 insertions, 38 deletions
diff --git a/dev/base_include b/dev/base_include
index 4841db8953..96a867475d 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -60,11 +60,11 @@ open Cases
open Pattern
open Patternops
open Cbv
-open Classops
+open Coercionops
open Arguments_renaming
open Pretyping
open Cbv
-open Classops
+open Coercionops
open Clenv
open Clenvtac
open Constr_matching
@@ -134,7 +134,7 @@ open Tacticals
open Tactics
open Eqschemes
-open Class
+open ComCoercion
open ComDefinition
open Indschemes
open Ind_tables
diff --git a/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh
new file mode 100644
index 0000000000..a95170a455
--- /dev/null
+++ b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11293" ] || [ "$CI_BRANCH" = "rename-class-files" ]; then
+
+ elpi_CI_REF=rename-class-files
+ elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+ mtac2_CI_REF=rename-class-files
+ mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f7f2bcdcff..835c20a4f7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -47,7 +47,7 @@ let ppmind kn = pp(MutInd.debug_print kn)
let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i)
let ppsp sp = pp(pr_path sp)
let ppqualid qid = pp(pr_qualid qid)
-let ppclindex cl = pp(Classops.pr_cl_index cl)
+let ppclindex cl = pp(Coercionops.pr_cl_index cl)
let ppscheme k = pp (Ind_tables.pr_scheme_kind k)
let prrecarg = function
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 5a2144f996..133326523b 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -29,7 +29,7 @@ val ppind : Names.inductive -> unit
val ppsp : Libnames.full_path -> unit
val ppqualid : Libnames.qualid -> unit
-val ppclindex : Classops.cl_index -> unit
+val ppclindex : Coercionops.cl_index -> unit
val ppscheme : 'a Ind_tables.scheme_kind -> unit
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 28f4f5aed6..cc0c1e4602 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -678,7 +678,7 @@ let remove_one_coercion inctx c =
try match match_coercion_app c with
| Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) ->
let nargs = List.length args in
- (match Classops.hide_coercion r with
+ (match Coercionops.hide_coercion r with
| Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) ->
(* We skip the coercion *)
let l = List.skipn (n - pars) args in
diff --git a/interp/notation.ml b/interp/notation.ml
index 5dc1658824..93969f3718 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1430,7 +1430,7 @@ let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
(**********************************************************************)
(* Mapping classes to scopes *)
-open Classops
+open Coercionops
type scope_class = cl_typ
diff --git a/interp/notation.mli b/interp/notation.mli
index 864e500d56..ea5125f7ec 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -271,7 +271,7 @@ val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option
(** Get the current scope bound to Sortclass, if it exists *)
val current_type_scope_name : unit -> scope_name option
-val scope_class_of_class : Classops.cl_typ -> scope_class
+val scope_class_of_class : Coercionops.cl_typ -> scope_class
(** Building notation key *)
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 2f26226f4e..4e7482d4af 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -18,11 +18,11 @@ open Tacticals.New
let update_flags ()=
let open TransparentState in
- let f accu coe = match coe.Classops.coe_value with
+ let f accu coe = match coe.Coercionops.coe_value with
| Names.GlobRef.ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
| _ -> accu
in
- let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in
+ let flags = List.fold_left f TransparentState.full (Coercionops.coercions ()) in
red_flags:=
CClosure.RedFlags.red_add_transparent
CClosure.betaiotazeta
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 9f6fe0e651..d8dbf2f3dc 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -370,14 +370,14 @@ let coerce_search_pattern_to_sort hpat =
let filter_head, coe_path =
try
let _, cp =
- Classops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in
+ Coercionops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in
warn ();
true, cp
with _ -> false, [] in
let coerce hp coe_index =
- let coe_ref = coe_index.Classops.coe_value in
+ let coe_ref = coe_index.Coercionops.coe_value in
try
- let n_imps = Option.get (Classops.hide_coercion coe_ref) in
+ let n_imps = Option.get (Coercionops.hide_coercion coe_ref) in
mkPApp (Pattern.PRef coe_ref) n_imps [|hp|]
with Not_found | Option.IsNone ->
errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc ()
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index f0e73bdb29..c980d204ca 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -27,7 +27,7 @@ open EConstr
open Vars
open Reductionops
open Pretype_errors
-open Classops
+open Coercionops
open Evarutil
open Evarconv
open Evd
diff --git a/pretyping/classops.ml b/pretyping/coercionops.ml
index 16021b66f8..16021b66f8 100644
--- a/pretyping/classops.ml
+++ b/pretyping/coercionops.ml
diff --git a/pretyping/classops.mli b/pretyping/coercionops.mli
index 9f633843eb..9f633843eb 100644
--- a/pretyping/classops.mli
+++ b/pretyping/coercionops.mli
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0364e1b61f..bfdb471c46 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1326,7 +1326,7 @@ let understand_ltac flags env sigma lvar kind c =
(sigma, c)
let path_convertible env sigma i p q =
- let open Classops in
+ let open Coercionops in
let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in
let mkGVar id = DAst.make @@ Glob_term.GVar(id) in
let mkGApp(rt,rtl) = DAst.make @@ Glob_term.GApp(rt,rtl) in
@@ -1379,4 +1379,4 @@ let path_convertible env sigma i p q =
let _ = Evarconv.unify_delay env sigma tp tq in true
with Evarconv.UnableToUnify _ | PretypeError _ -> false
-let _ = Classops.install_path_comparator path_convertible
+let _ = Coercionops.install_path_comparator path_convertible
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 7e140f4399..07154d4e03 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -26,7 +26,7 @@ Constr_matching
Tacred
Typeclasses_errors
Typeclasses
-Classops
+Coercionops
Program
Coercion
Detyping
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 8a403e5a03..625ffb5a06 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -32,7 +32,7 @@ let declare_variable is_coe ~kind typ imps impl {CAst.v=name} =
let env = Global.env () in
let sigma = Evd.from_env env in
let () = Classes.declare_instance env sigma None true r in
- let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in
+ let () = if is_coe then ComCoercion.try_add_new_coercion r ~local:true ~poly:false in
()
let instance_of_univ_entry = function
@@ -65,7 +65,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name
| Declare.ImportNeedQualified -> true
| Declare.ImportDefaultBehavior -> false
in
- let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in
+ let () = if is_coe then ComCoercion.try_add_new_coercion gr ~local ~poly in
let inst = instance_of_univ_entry univs in
(gr,inst)
diff --git a/vernac/class.ml b/vernac/comCoercion.ml
index 3c43b125d1..56ab6f289d 100644
--- a/vernac/class.ml
+++ b/vernac/comCoercion.ml
@@ -18,7 +18,7 @@ open Context
open Vars
open Termops
open Environ
-open Classops
+open Coercionops
open Declare
open Libobject
@@ -231,7 +231,7 @@ let check_source = function
let cache_coercion (_,c) =
let env = Global.env () in
let sigma = Evd.from_env env in
- Classops.declare_coercion env sigma c
+ Coercionops.declare_coercion env sigma c
let open_coercion i o =
if Int.equal i 1 then
diff --git a/vernac/class.mli b/vernac/comCoercion.mli
index 3254d5d981..f98ef4fdd6 100644
--- a/vernac/class.mli
+++ b/vernac/comCoercion.mli
@@ -9,7 +9,7 @@
(************************************************************************)
open Names
-open Classops
+open Coercionops
(** Classes and coercions. *)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index b603c54026..8de1c69424 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -553,7 +553,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni
(* Declare the possible notations of inductive types *)
List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
(* Declare the coercions *)
- List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes
+ List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index eb7b28f15b..d04a02febc 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -199,7 +199,7 @@ let print_opacity ref =
(*******************)
let print_if_is_coercion ref =
- if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else []
+ if Coercionops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else []
(*******************)
(* *)
@@ -951,7 +951,7 @@ let inspect env sigma depth =
(*************************************************************************)
(* Pretty-printing functions coming from classops.ml *)
-open Classops
+open Coercionops
let print_coercion_value v = Printer.pr_global v.coe_value
@@ -965,7 +965,7 @@ let print_path ((i,j),p) =
str"] : ") ++
print_class i ++ str" >-> " ++ print_class j
-let _ = Classops.install_path_printer print_path
+let _ = Coercionops.install_path_printer print_path
let print_graph () =
prlist_with_sep fnl print_path (inheritance_graph())
diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli
index dc4280f286..2ee9c4ed33 100644
--- a/vernac/prettyp.mli
+++ b/vernac/prettyp.mli
@@ -52,7 +52,7 @@ val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t
val print_graph : unit -> Pp.t
val print_classes : unit -> Pp.t
val print_coercions : unit -> Pp.t
-val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t
+val print_path_between : Coercionops.cl_typ -> Coercionops.cl_typ -> Pp.t
val print_canonical_projections : env -> Evd.evar_map -> Pp.t
(** Pretty-printing functions for type classes and instances *)
diff --git a/vernac/record.ml b/vernac/record.ml
index ea10e06d02..df9b4a0914 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -366,8 +366,8 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
let refi = GlobRef.ConstRef kn in
Impargs.maybe_declare_manual_implicits false refi impls;
if flags.pf_subclass then begin
- let cl = Class.class_of_global (GlobRef.IndRef indsp) in
- Class.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
+ let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in
+ ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
end;
let i = if is_local_assum decl then i+1 else i in
(Some kn::sp_projs, i, Projection term::subst)
@@ -489,7 +489,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
let cstr = (rsp, 1) in
let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
let build = GlobRef.ConstructRef cstr in
- let () = if is_coe then Class.try_add_new_coercion build ~local:false ~poly in
+ let () = if is_coe then ComCoercion.try_add_new_coercion build ~local:false ~poly in
let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in
rsp
in
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 5226c2ba65..7b4924eaed 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -21,7 +21,7 @@ RecLemmas
Library
Prettyp
Lemmas
-Class
+ComCoercion
Auto_ind_decl
Search
Indschemes
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 439ec61d38..604d1b28ff 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -49,9 +49,9 @@ let get_goal_or_global_context ~pstate glnum =
| Some p -> Pfedit.get_goal_context p glnum
let cl_of_qualid = function
- | FunClass -> Classops.CL_FUN
- | SortClass -> Classops.CL_SORT
- | RefClass r -> Class.class_of_global (Smartlocate.smart_global ~head:true r)
+ | FunClass -> Coercionops.CL_FUN
+ | SortClass -> Coercionops.CL_SORT
+ | RefClass r -> ComCoercion.class_of_global (Smartlocate.smart_global ~head:true r)
let scope_class_of_qualid qid =
Notation.scope_class_of_class (cl_of_qualid qid)
@@ -524,11 +524,11 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
let vernac_definition_hook ~local ~poly = let open Decls in function
| Coercion ->
- Some (Class.add_coercion_hook ~poly)
+ Some (ComCoercion.add_coercion_hook ~poly)
| CanonicalStructure ->
Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
| SubClass ->
- Some (Class.add_subclass_hook ~poly)
+ Some (ComCoercion.add_subclass_hook ~poly)
| _ -> None
let fresh_name_for_anonymous_theorem () =
@@ -1034,7 +1034,7 @@ let vernac_coercion ~atts ref qids qidt =
let target = cl_of_qualid qidt in
let source = cl_of_qualid qids in
let ref' = smart_global ref in
- Class.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target;
+ ComCoercion.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target;
Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
let vernac_identity_coercion ~atts id qids qidt =
@@ -1042,7 +1042,7 @@ let vernac_identity_coercion ~atts id qids qidt =
let local = enforce_locality local in
let target = cl_of_qualid qidt in
let source = cl_of_qualid qids in
- Class.try_add_new_identity_coercion id ~local ~poly ~source ~target
+ ComCoercion.try_add_new_identity_coercion id ~local ~poly ~source ~target
(* Type classes *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:50:06 +0000