summaryrefslogtreecommitdiff
path: root/pretyping/indrec.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/indrec.ml')
-rw-r--r--pretyping/indrec.ml281
1 files changed, 160 insertions, 121 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index c7cdb302..54d47fbe 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -11,66 +11,75 @@
(* This file builds various inductive schemes *)
open Pp
+open Errors
open Util
open Names
open Libnames
+open Globnames
open Nameops
open Term
+open Vars
+open Context
open Namegen
open Declarations
-open Entries
+open Declareops
open Inductive
open Inductiveops
open Environ
open Reductionops
-open Typeops
-open Type_errors
-open Safe_typing
open Nametab
-open Sign
type dep_flag = bool
(* Errors related to recursors building *)
type recursion_scheme_error =
- | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive
+ | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive
| NotMutualInScheme of inductive * inductive
exception RecursionSchemeError of recursion_scheme_error
let make_prod_dep dep env = if dep then mkProd_name env else mkProd
-let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
+let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c)
(*******************************************)
(* Building curryfied elimination *)
(*******************************************)
+let is_private mib =
+ match mib.mind_private with
+ | Some true -> true
+ | _ -> false
+
+let check_privacy_block mib =
+ if is_private mib then
+ errorlabstrm ""(str"case analysis on a private inductive type")
+
(**********************************************************************)
(* Building case analysis schemes *)
(* Christine Paulin, 1996 *)
-let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
- let lnamespar = List.map
- (fun (n, c, t) -> (n, c, Termops.refresh_universes t))
- mib.mind_params_ctxt
+let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
+ let lnamespar = Vars.subst_instance_context u mib.mind_params_ctxt in
+ let indf = make_ind_family(pind, Termops.extended_rel_list 0 lnamespar) in
+ let constrs = get_constructors env indf in
+ let projs = get_projections env indf in
+
+ let () = if Option.is_empty projs then check_privacy_block mib in
+ let () =
+ if not (Sorts.List.mem kind (elim_sorts specif)) then
+ raise
+ (RecursionSchemeError
+ (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind)))
in
+ let ndepar = mip.mind_nrealdecls + 1 in
- if not (List.mem kind (elim_sorts specif)) then
- raise
- (RecursionSchemeError
- (NotAllowedCaseAnalysis (false, Termops.new_sort_in_family kind, ind)));
-
- let ndepar = mip.mind_nrealargs_ctxt + 1 in
-
- (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
- (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
+ (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
+ (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
let env' = push_rel_context lnamespar env in
- let indf = make_ind_family(ind, Termops.extended_rel_list 0 lnamespar) in
- let constrs = get_constructors env indf in
let rec add_branch env k =
- if k = Array.length mip.mind_consnames then
+ if Int.equal k (Array.length mip.mind_consnames) then
let nbprod = k+1 in
let indf' = lift_inductive_family nbprod indf in
@@ -78,7 +87,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
let depind = build_dependent_inductive env indf' in
let deparsign = (Anonymous,None,depind)::arsign in
- let ci = make_case_info env ind RegularStyle in
+ let ci = make_case_info env (fst pind) RegularStyle in
let pbody =
appvect
(mkRel (ndepar + nbprod),
@@ -90,21 +99,34 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
(Anonymous,depind,pbody))
arsign
in
- it_mkLambda_or_LetIn_name env'
- (mkCase (ci, lift ndepar p,
- mkRel 1,
- Termops.rel_vect ndepar k))
- deparsign
+ let obj =
+ match projs with
+ | None -> mkCase (ci, lift ndepar p, mkRel 1,
+ Termops.rel_vect ndepar k)
+ | Some ps ->
+ let term =
+ mkApp (mkRel 2,
+ Array.map
+ (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in
+ if dep then
+ let ty = mkApp (mkRel 3, [| mkRel 1 |]) in
+ mkCast (term, DEFAULTcast, ty)
+ else term
+ in
+ it_mkLambda_or_LetIn_name env' obj deparsign
else
let cs = lift_constructor (k+1) constrs.(k) in
let t = build_branch_type env dep (mkRel (k+1)) cs in
mkLambda_string "f" t
(add_branch (push_rel (Anonymous, None, t) env) (k+1))
in
- let typP = make_arity env' dep indf (Termops.new_sort_in_family kind) in
- it_mkLambda_or_LetIn_name env
+ let sigma, s = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in
+ let typP = make_arity env' dep indf s in
+ let c =
+ it_mkLambda_or_LetIn_name env
(mkLambda_string "P" typP
- (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
+ (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
+ in sigma, c
(* check if the type depends recursively on one of the inductive scheme *)
@@ -137,7 +159,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
let d = (n,Some b,t) in
mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c)
| Ind (_,_) ->
- let realargs = list_skipn nparams largs in
+ let realargs = List.skipn nparams largs in
let base = applist (lift i pk,realargs) in
if depK then
Reduction.beta_appvect
@@ -158,7 +180,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
(match dest_recarg ra with
| Mrec (_,j) when is_rec -> (depPvect.(j),rest)
| Imbr _ ->
- Flags.if_warn msg_warning (str "Ignoring recursive call");
+ msg_warning (strbrk "Ignoring recursive call");
(None,rest)
| _ -> (None, rest))
in
@@ -172,7 +194,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
let nP = lift (i+1+decP) p in
let env' = push_rel (n,None,t) env in
let t_0 = process_pos env' dep' nP (lift 1 t) in
- make_prod_dep (dep or dep') env
+ make_prod_dep (dep || dep') env
(n,t,
mkArrow t_0
(process_constr
@@ -186,9 +208,9 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
| _ -> assert false
else
if dep then
- let realargs = List.map (fun k -> mkRel (i-k)) (List.rev li) in
+ let realargs = List.rev_map (fun k -> mkRel (i-k)) li in
let params = List.map (lift i) vargs in
- let co = applist (mkConstruct cs.cs_cstr,params@realargs) in
+ let co = applist (mkConstructU cs.cs_cstr,params@realargs) in
Reduction.beta_appvect c [|co|]
else c
in
@@ -212,14 +234,14 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
let d = (n,Some b,t) in
mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
| Ind _ ->
- let realargs = list_skipn nparrec largs
+ let realargs = List.skipn nparrec largs
and arg = appvect (mkRel (i+1), Termops.extended_rel_vect 0 hyps) in
applist(lift i fk,realargs@[arg])
| _ -> assert false
in
prec env 0 []
in
- (* ici, cstrprods est la liste des produits du constructeur instantié *)
+ (* ici, cstrprods est la liste des produits du constructeur instantié *)
let rec process_constr env i f = function
| (n,None,t as d)::cprest, recarg::rest ->
let optionpos =
@@ -248,7 +270,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
process_constr (push_rel d env) (i+1) (lift 1 f)
(cprest,rest))
| [],[] -> f
- | _,[] | [],_ -> anomaly "process_constr"
+ | _,[] | [],_ -> anomaly (Pp.str "process_constr")
in
process_constr env 0 f (List.rev cstr.cs_args, recargs)
@@ -264,21 +286,21 @@ let context_chop k ctx =
| (_, []) -> failwith "context_chop"
in chop_aux [] (k,ctx)
-
(* Main function *)
-let mis_make_indrec env sigma listdepkind mib =
+let mis_make_indrec env sigma listdepkind mib u =
let nparams = mib.mind_nparams in
- let nparrec = mib. mind_nparams_rec in
+ let nparrec = mib.mind_nparams_rec in
+ let evdref = ref sigma in
let lnonparrec,lnamesparrec =
- context_chop (nparams-nparrec) mib.mind_params_ctxt in
+ context_chop (nparams-nparrec) (Vars.subst_instance_context u mib.mind_params_ctxt) in
let nrec = List.length listdepkind in
let depPvec =
- Array.create mib.mind_ntypes (None : (bool * constr) option) in
+ Array.make mib.mind_ntypes (None : (bool * constr) option) in
let _ =
let rec
assign k = function
| [] -> ()
- | (indi,mibi,mipi,dep,_)::rest ->
+ | ((indi,u),mibi,mipi,dep,_)::rest ->
(Array.set depPvec (snd indi) (Some(dep,mkRel k));
assign (k-1) rest)
in
@@ -287,12 +309,12 @@ let mis_make_indrec env sigma listdepkind mib =
Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
(* recarg information for non recursive parameters *)
let rec recargparn l n =
- if n = 0 then l else recargparn (mk_norec::l) (n-1) in
+ if Int.equal n 0 then l else recargparn (mk_norec::l) (n-1) in
let recargpar = recargparn [] (nparams-nparrec) in
let make_one_rec p =
let makefix nbconstruct =
let rec mrec i ln ltyp ldef = function
- | (indi,mibi,mipi,dep,_)::rest ->
+ | ((indi,u),mibi,mipi,dep,_)::rest ->
let tyi = snd indi in
let nctyi =
Array.length mipi.mind_consnames in (* nb constructeurs du type*)
@@ -300,7 +322,7 @@ let mis_make_indrec env sigma listdepkind mib =
(* arity in the context of the fixpoint, i.e.
P1..P_nrec f1..f_nbconstruct *)
let args = Termops.extended_rel_list (nrec+nbconstruct) lnamesparrec in
- let indf = make_ind_family(indi,args) in
+ let indf = make_ind_family((indi,u),args) in
let arsign,_ = get_arity env indf in
let depind = build_dependent_inductive env indf in
@@ -315,7 +337,7 @@ let mis_make_indrec env sigma listdepkind mib =
P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
let args' = Termops.extended_rel_list (dect+nrec) lnamesparrec in
let args'' = Termops.extended_rel_list ndepar lnonparrec in
- let indf' = make_ind_family(indi,args'@args'') in
+ let indf' = make_ind_family((indi,u),args'@args'') in
let branches =
let constrs = get_constructors env indf' in
@@ -324,8 +346,8 @@ let mis_make_indrec env sigma listdepkind mib =
(fun f -> appvect (f, Termops.extended_rel_vect ndepar lnonparrec))
fi
in
- array_map3
- (make_rec_branch_arg env sigma
+ Array.map3
+ (make_rec_branch_arg env !evdref
(nparrec,depPvec,larsign))
vecfi constrs (dest_subterms recargsvec.(tyi))
in
@@ -359,10 +381,27 @@ let mis_make_indrec env sigma listdepkind mib =
(Anonymous,depind',concl))
arsign'
in
- it_mkLambda_or_LetIn_name env
- (mkCase (ci, pred,
- mkRel 1,
- branches))
+ let obj =
+ let projs = get_projections env indf in
+ match projs with
+ | None -> (mkCase (ci, pred,
+ mkRel 1,
+ branches))
+ | Some ps ->
+ let branch = branches.(0) in
+ let ctx, br = decompose_lam_assum branch in
+ let n, subst =
+ List.fold_right (fun (na,b,t) (i, subst) ->
+ if b == None then
+ let t = mkProj (Projection.make ps.(i) true, mkRel 1) in
+ (i + 1, t :: subst)
+ else (i, mkRel 0 :: subst))
+ ctx (0, [])
+ in
+ let term = substl subst br in
+ term
+ in
+ it_mkLambda_or_LetIn_name env obj
(Termops.lift_rel_context nrec deparsign)
in
@@ -383,26 +422,26 @@ let mis_make_indrec env sigma listdepkind mib =
let fixn = Array.of_list (List.rev ln) in
let fixtyi = Array.of_list (List.rev ltyp) in
let fixdef = Array.of_list (List.rev ldef) in
- let names = Array.create nrec (Name(id_of_string "F")) in
+ let names = Array.make nrec (Name(Id.of_string "F")) in
mkFix ((fixn,p),(names,fixtyi,fixdef))
in
mrec 0 [] [] []
in
let rec make_branch env i = function
- | (indi,mibi,mipi,dep,_)::rest ->
+ | ((indi,u),mibi,mipi,dep,_)::rest ->
let tyi = snd indi in
let nconstr = Array.length mipi.mind_consnames in
let rec onerec env j =
- if j = nconstr then
+ if Int.equal j nconstr then
make_branch env (i+j) rest
else
let recarg = (dest_subterms recargsvec.(tyi)).(j) in
let recarg = recargpar@recarg in
let vargs = Termops.extended_rel_list (nrec+i+j) lnamesparrec in
- let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in
+ let cs = get_constructor ((indi,u),mibi,mipi,vargs) (j+1) in
let p_0 =
type_rec_branch
- true dep env sigma (vargs,depPvec,i+j) tyi cs recarg
+ true dep env !evdref (vargs,depPvec,i+j) tyi cs recarg
in
mkLambda_string "f" p_0
(onerec (push_rel (Anonymous,None,p_0) env) (j+1))
@@ -411,9 +450,13 @@ let mis_make_indrec env sigma listdepkind mib =
makefix i listdepkind
in
let rec put_arity env i = function
- | (indi,_,_,dep,kinds)::rest ->
- let indf = make_ind_family (indi, Termops.extended_rel_list i lnamesparrec) in
- let typP = make_arity env dep indf (Termops.new_sort_in_family kinds) in
+ | ((indi,u),_,_,dep,kinds)::rest ->
+ let indf = make_ind_family ((indi,u), Termops.extended_rel_list i lnamesparrec) in
+ let s =
+ Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env)
+ evdref kinds
+ in
+ let typP = make_arity env dep indf s in
mkLambda_string "P" typP
(put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
| [] ->
@@ -421,33 +464,38 @@ let mis_make_indrec env sigma listdepkind mib =
in
(* Body on make_one_rec *)
- let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in
+ let ((indi,u),mibi,mipi,dep,kind) = List.nth listdepkind p in
if (mis_is_recursive_subset
- (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind)
+ (List.map (fun ((indi,u),_,_,_,_) -> snd indi) listdepkind)
mipi.mind_recargs)
then
let env' = push_rel_context lnamesparrec env in
it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind)
lnamesparrec
else
- mis_make_case_com dep env sigma indi (mibi,mipi) kind
+ let evd', c = mis_make_case_com dep env !evdref (indi,u) (mibi,mipi) kind in
+ evdref := evd'; c
in
(* Body of mis_make_indrec *)
- list_tabulate make_one_rec nrec
+ !evdref, List.init nrec make_one_rec
(**********************************************************************)
(* This builds elimination predicate for Case tactic *)
-let build_case_analysis_scheme env sigma ity dep kind =
- let (mib,mip) = lookup_mind_specif env ity in
- mis_make_case_com dep env sigma ity (mib,mip) kind
+let build_case_analysis_scheme env sigma pity dep kind =
+ let (mib,mip) = lookup_mind_specif env (fst pity) in
+ mis_make_case_com dep env sigma pity (mib,mip) kind
-let build_case_analysis_scheme_default env sigma ity kind =
- let (mib,mip) = lookup_mind_specif env ity in
- let dep = inductive_sort_family mip <> InProp in
- mis_make_case_com dep env sigma ity (mib,mip) kind
+let is_in_prop mip =
+ match inductive_sort_family mip with
+ | InProp -> true
+ | _ -> false
+let build_case_analysis_scheme_default env sigma pity kind =
+ let (mib,mip) = lookup_mind_specif env (fst pity) in
+ let dep = not (is_in_prop mip) in
+ mis_make_case_com dep env sigma pity (mib,mip) kind
(**********************************************************************)
(* [modify_sort_scheme s rec] replaces the sort of the scheme
@@ -456,87 +504,78 @@ let build_case_analysis_scheme_default env sigma ity kind =
let change_sort_arity sort =
let rec drec a = match kind_of_term a with
| Cast (c,_,_) -> drec c
- | Prod (n,t,c) -> mkProd (n, t, drec c)
- | LetIn (n,b,t,c) -> mkLetIn (n,b, t, drec c)
- | Sort _ -> mkSort sort
+ | Prod (n,t,c) -> let s, c' = drec c in s, mkProd (n, t, c')
+ | LetIn (n,b,t,c) -> let s, c' = drec c in s, mkLetIn (n,b,t,c')
+ | Sort s -> s, mkSort sort
| _ -> assert false
in
drec
-(* [npar] is the number of expected arguments (then excluding letin's) *)
-let modify_sort_scheme sort =
- let rec drec npar elim =
- match kind_of_term elim with
- | Lambda (n,t,c) ->
- if npar = 0 then
- mkLambda (n, change_sort_arity sort t, c)
- else
- mkLambda (n, t, drec (npar-1) c)
- | LetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c)
- | _ -> anomaly "modify_sort_scheme: wrong elimination type"
- in
- drec
-
(* Change the sort in the type of an inductive definition, builds the
corresponding eta-expanded term *)
-let weaken_sort_scheme sort npars term =
+let weaken_sort_scheme env evd set sort npars term ty =
+ let evdref = ref evd in
let rec drec np elim =
match kind_of_term elim with
| Prod (n,t,c) ->
- if np = 0 then
- let t' = change_sort_arity sort t in
- mkProd (n, t', c),
- mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1)))
+ if Int.equal np 0 then
+ let osort, t' = change_sort_arity sort t in
+ evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort) env !evdref sort osort;
+ mkProd (n, t', c),
+ mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1)))
else
let c',term' = drec (np-1) c in
mkProd (n, t, c'), mkLambda (n, t, term')
| LetIn (n,b,t,c) -> let c',term' = drec np c in
mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term')
- | _ -> anomaly "weaken_sort_scheme: wrong elimination type"
+ | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type")
in
- drec npars
+ let ty, term = drec npars ty in
+ !evdref, ty, term
(**********************************************************************)
(* Interface to build complex Scheme *)
(* Check inductive types only occurs once
(otherwise we obtain a meaning less scheme) *)
-let check_arities listdepkind =
+let check_arities env listdepkind =
let _ = List.fold_left
- (fun ln ((_,ni as mind),mibi,mipi,dep,kind) ->
+ (fun ln (((_,ni as mind),u),mibi,mipi,dep,kind) ->
let kelim = elim_sorts (mibi,mipi) in
- if not (List.exists ((=) kind) kelim) then raise
+ if not (Sorts.List.mem kind kelim) then raise
(RecursionSchemeError
- (NotAllowedCaseAnalysis (true, Termops.new_sort_in_family kind,mind)))
- else if List.mem ni ln then raise
+ (NotAllowedCaseAnalysis (true, fst (Universes.fresh_sort_in_family env
+ kind),(mind,u))))
+ else if Int.List.mem ni ln then raise
(RecursionSchemeError (NotMutualInScheme (mind,mind)))
else ni::ln)
[] listdepkind
in true
let build_mutual_induction_scheme env sigma = function
- | (mind,dep,s)::lrecspec ->
- let (mib,mip) = Global.lookup_inductive mind in
+ | ((mind,u),dep,s)::lrecspec ->
+ let (mib,mip) = lookup_mind_specif env mind in
let (sp,tyi) = mind in
let listdepkind =
- (mind,mib,mip,dep,s)::
+ ((mind,u),mib,mip,dep,s)::
(List.map
- (function (mind',dep',s') ->
+ (function ((mind',u'),dep',s') ->
let (sp',_) = mind' in
- if sp=sp' then
+ if eq_mind sp sp' then
let (mibi',mipi') = lookup_mind_specif env mind' in
- (mind',mibi',mipi',dep',s')
+ ((mind',u'),mibi',mipi',dep',s')
else
raise (RecursionSchemeError (NotMutualInScheme (mind,mind'))))
lrecspec)
in
- let _ = check_arities listdepkind in
- mis_make_indrec env sigma listdepkind mib
- | _ -> anomaly "build_induction_scheme expects a non empty list of inductive types"
+ let _ = check_arities env listdepkind in
+ mis_make_indrec env sigma listdepkind mib u
+ | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types")
-let build_induction_scheme env sigma ind dep kind =
- let (mib,mip) = lookup_mind_specif env ind in
- List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
+let build_induction_scheme env sigma pind dep kind =
+ let (mib,mip) = lookup_mind_specif env (fst pind) in
+ let sigma, l = mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib (snd pind) in
+ sigma, List.hd l
(*s Eliminations. *)
@@ -559,17 +598,17 @@ let lookup_eliminator ind_sp s =
(* Try first to get an eliminator defined in the same section as the *)
(* inductive type *)
try
- let cst =Global.constant_of_delta_kn (make_kn mp dp (label_of_id id)) in
+ let cst =Global.constant_of_delta_kn (make_kn mp dp (Label.of_id id)) in
let _ = Global.lookup_constant cst in
- mkConst cst
+ ConstRef cst
with Not_found ->
(* Then try to get a user-defined eliminator in some other places *)
(* using short name (e.g. for "eq_rec") *)
- try constr_of_global (Nametab.locate (qualid_of_ident id))
+ try Nametab.locate (qualid_of_ident id)
with Not_found ->
errorlabstrm "default_elim"
(strbrk "Cannot find the elimination combinator " ++
pr_id id ++ strbrk ", the elimination of the inductive definition " ++
- pr_global_env Idset.empty (IndRef ind_sp) ++
+ pr_global_env Id.Set.empty (IndRef ind_sp) ++
strbrk " on sort " ++ Termops.pr_sort_family s ++
strbrk " is probably not allowed.")
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 06:41:42 +0000