aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml3
-rw-r--r--pretyping/detyping.ml3
-rw-r--r--pretyping/evarsolve.ml2
-rw-r--r--pretyping/glob_ops.ml43
-rw-r--r--pretyping/glob_ops.mli9
-rw-r--r--pretyping/glob_term.ml11
-rw-r--r--pretyping/locus.ml5
-rw-r--r--pretyping/locusops.ml4
-rw-r--r--pretyping/miscops.ml55
-rw-r--r--pretyping/miscops.mli30
-rw-r--r--pretyping/pattern.ml6
-rw-r--r--pretyping/patternops.ml5
-rw-r--r--pretyping/patternops.mli1
-rw-r--r--pretyping/pretyping.ml1
-rw-r--r--pretyping/typeclasses.ml2
-rw-r--r--pretyping/typeclasses.mli2
-rw-r--r--pretyping/typeclasses_errors.ml2
-rw-r--r--pretyping/typeclasses_errors.mli4
-rw-r--r--pretyping/typing.ml7
19 files changed, 76 insertions, 119 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1edce17bd..0dd3c5944 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1427,6 +1427,7 @@ and match_current pb (initial,tomatch) =
let case =
make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
in
+ let _ = Evarutil.evd_comb1 (Typing.type_of pb.env) pb.evdref pred in
Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
{ uj_val = applist (case, inst);
uj_type = prod_applist !(pb.evdref) typ inst }
@@ -2103,7 +2104,7 @@ let mk_JMeq_refl evdref typ x =
let hole na = DAst.make @@
GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na),
- Misctypes.IntroAnonymous, None)
+ IntroAnonymous, None)
let constr_of_pat env evdref arsign pat avoid =
let rec typ env (ty, realargs) pat avoid =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index e6cfe1f76..df89d9eac 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -27,7 +27,6 @@ open Libnames
open Globnames
open Nametab
open Mod_subst
-open Misctypes
open Decl_kinds
open Context.Named.Declaration
open Ltac_pretype
@@ -1027,7 +1026,7 @@ let rec subst_glob_constr subst = DAst.map (function
| GCast (r1,k) as raw ->
let r1' = subst_glob_constr subst r1 in
- let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in
+ let k' = smartmap_cast_type (subst_glob_constr subst) k in
if r1' == r1 && k' == k then raw else GCast (r1',k')
| GProj (p,c) as raw ->
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index aefae1ecc..8afb9b942 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -929,7 +929,7 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_
with Not_found ->
match expand_alias_once evd aliases t with
| None -> raise Not_found
- | Some c -> aux k c in
+ | Some c -> aux k (lift k c) in
try
let c = aux 0 c_in_env_extended_with_k_binders in
Invertible (UniqueProjection (c,!effects))
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 63618c918..8ecec30cf 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -11,10 +11,8 @@
open Util
open CAst
open Names
-open Constr
open Nameops
open Globnames
-open Misctypes
open Glob_term
open Evar_kinds
open Ltac_pretype
@@ -48,12 +46,20 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
let comp2 = f ty in
(na,k,comp1,comp2)
+
+let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
+| GProp, GProp -> true
+| GSet, GSet -> true
+| GType l1, GType l2 ->
+ List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2
+| _ -> false
+
let binding_kind_eq bk1 bk2 = match bk1, bk2 with
| Decl_kinds.Explicit, Decl_kinds.Explicit -> true
| Decl_kinds.Implicit, Decl_kinds.Implicit -> true
| (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false
-let case_style_eq s1 s2 = match s1, s2 with
+let case_style_eq s1 s2 = let open Constr in match s1, s2 with
| LetStyle, LetStyle -> true
| IfStyle, IfStyle -> true
| LetPatternStyle, LetPatternStyle -> true
@@ -141,10 +147,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 &&
Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 &&
Array.equal f c1 c2 && Array.equal f t1 t2
- | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2
+ | GSort s1, GSort s2 -> glob_sort_eq s1 s2
| GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) ->
Option.equal (==) gn1 gn2 (** Only thing sensible *) &&
- Miscops.intro_pattern_naming_eq nam1 nam2
+ Namegen.intro_pattern_naming_eq nam1 nam2
| GCast (c1, t1), GCast (c2, t2) ->
f c1 c2 && cast_type_eq f t1 t2
| GProj (p1, t1), GProj (p2, t2) ->
@@ -154,6 +160,21 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
+(** Mapping [cast_type] *)
+
+let map_cast_type f = function
+ | CastConv a -> CastConv (f a)
+ | CastVM a -> CastVM (f a)
+ | CastCoerce -> CastCoerce
+ | CastNative a -> CastNative (f a)
+
+let smartmap_cast_type f c =
+ match c with
+ | CastConv a -> let a' = f a in if a' == a then c else CastConv a'
+ | CastVM a -> let a' = f a in if a' == a then c else CastVM a'
+ | CastCoerce -> CastCoerce
+ | CastNative a -> let a' = f a in if a' == a then c else CastNative a'
+
let map_glob_constr_left_to_right f = DAst.map (function
| GApp (g,args) ->
let comp1 = f g in
@@ -194,7 +215,7 @@ let map_glob_constr_left_to_right f = DAst.map (function
GRec (fk,idl,comp1,comp2,comp3)
| GCast (c,k) ->
let comp1 = f c in
- let comp2 = Miscops.map_cast_type f k in
+ let comp2 = map_cast_type f k in
GCast (comp1,comp2)
| GProj (p,c) ->
GProj (p, f c)
@@ -248,8 +269,9 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
| GCases (_,rtntypopt,tml,pl) ->
let fold_pattern acc {v=(idl,p,c)} = f (List.fold_right g idl v) acc c in
let fold_tomatch (v',acc) (tm,(na,onal)) =
- (Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'')
- (Name.fold_right g na v') onal,
+ ((if rtntypopt = None then v' else
+ Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'')
+ (Name.fold_right g na v') onal),
f v acc tm) in
let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in
let acc = Option.fold_left (f v') acc rtntypopt in
@@ -260,6 +282,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
| GIf (c,rtntyp,b1,b2) ->
f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2
| GRec (_,idl,bll,tyl,bv) ->
+ let v' = Array.fold_right g idl v in
let f' i acc fid =
let v,acc =
List.fold_left
@@ -267,7 +290,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
(Name.fold_right g na v, f v (Option.fold_left (f v) acc bbd) bty))
(v,acc)
bll.(i) in
- f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in
+ f v' (f v acc tyl.(i)) (bv.(i)) in
Array.fold_left_i f' acc idl
| GCast (c,k) ->
let acc = match k with
@@ -539,7 +562,7 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo
| PatVar (Name id) when not isclosed ->
GVar id
| PatVar Anonymous when not isclosed ->
- GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Misctypes.IntroAnonymous,None)
+ GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Namegen.IntroAnonymous,None)
| _ -> raise Not_found
) x
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 124440f5d..c967f4e88 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -13,6 +13,8 @@ open Glob_term
(** Equalities *)
+val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
+
val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
val alias_of_pat : 'a cases_pattern_g -> Name.t
@@ -20,10 +22,15 @@ val alias_of_pat : 'a cases_pattern_g -> Name.t
val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g
val cast_type_eq : ('a -> 'a -> bool) ->
- 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
+ 'a cast_type -> 'a cast_type -> bool
val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool
+(** Mapping [cast_type] *)
+
+val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
+val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
+
(** Operations on [glob_constr] *)
val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 6ecb479e6..54fa5328f 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -18,7 +18,6 @@
open Names
open Decl_kinds
-open Misctypes
type existential_name = Id.t
@@ -41,6 +40,14 @@ type glob_constraint = glob_level * Univ.constraint_type * glob_level
type sort_info = (Libnames.reference * int) option list
type glob_sort = sort_info glob_sort_gen
+(** Casts *)
+
+type 'a cast_type =
+ | CastConv of 'a
+ | CastVM of 'a
+ | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
+ | CastNative of 'a
+
(** The kind of patterns that occurs in "match ... with ... end"
locs here refers to the ident's location, not whole pat *)
@@ -73,7 +80,7 @@ type 'a glob_constr_r =
| GRec of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array *
'a glob_constr_g array * 'a glob_constr_g array
| GSort of glob_sort
- | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option
+ | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
| GCast of 'a glob_constr_g * 'a glob_constr_g cast_type
| GProj of Projection.t * 'a glob_constr_g
and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
diff --git a/pretyping/locus.ml b/pretyping/locus.ml
index 95a2e495b..37dd120c1 100644
--- a/pretyping/locus.ml
+++ b/pretyping/locus.ml
@@ -9,10 +9,13 @@
(************************************************************************)
open Names
-open Misctypes
(** Locus : positions in hypotheses and goals *)
+type 'a or_var =
+ | ArgArg of 'a
+ | ArgVar of lident
+
(** {6 Occurrences} *)
type 'a occurrences_gen =
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 1664e68f2..6b6a3f8a9 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -86,8 +86,8 @@ let concrete_clause_of enum_hyps cl =
(** Miscellaneous functions *)
let out_arg = function
- | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.")
- | Misctypes.ArgArg x -> x
+ | ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.")
+ | ArgArg x -> x
let occurrences_of_hyp id cls =
let rec hyp_occ = function
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
deleted file mode 100644
index 1697e54ab..000000000
--- a/pretyping/miscops.ml
+++ /dev/null
@@ -1,55 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Util
-open Misctypes
-
-(** Mapping [cast_type] *)
-
-let map_cast_type f = function
- | CastConv a -> CastConv (f a)
- | CastVM a -> CastVM (f a)
- | CastCoerce -> CastCoerce
- | CastNative a -> CastNative (f a)
-
-let smartmap_cast_type f c =
- match c with
- | CastConv a -> let a' = f a in if a' == a then c else CastConv a'
- | CastVM a -> let a' = f a in if a' == a then c else CastVM a'
- | CastCoerce -> CastCoerce
- | CastNative a -> let a' = f a in if a' == a then c else CastNative a'
-
-(** Equalities on [glob_sort] *)
-
-let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
-| GProp, GProp -> true
-| GSet, GSet -> true
-| GType l1, GType l2 ->
- List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2
-| _ -> false
-
-let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
-| IntroAnonymous, IntroAnonymous -> true
-| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2
-| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
-| _ -> false
-
-(** Mapping bindings *)
-
-let map_explicit_bindings f l =
- let map = CAst.map (fun (hyp, x) -> (hyp, f x)) in
- List.map map l
-
-let map_bindings f = function
-| ImplicitBindings l -> ImplicitBindings (List.map f l)
-| ExplicitBindings expl -> ExplicitBindings (map_explicit_bindings f expl)
-| NoBindings -> NoBindings
-
-let map_with_bindings f (x, bl) = (f x, map_bindings f bl)
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
deleted file mode 100644
index 6a84fb9eb..000000000
--- a/pretyping/miscops.mli
+++ /dev/null
@@ -1,30 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Misctypes
-
-(** Mapping [cast_type] *)
-
-val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
-val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
-
-(** Equalities on [glob_sort] *)
-
-val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
-
-(** Equalities on [intro_pattern_naming] *)
-
-val intro_pattern_naming_eq :
- intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool
-
-(** Mapping bindings *)
-
-val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings
-val map_with_bindings : ('a -> 'b) -> 'a with_bindings -> 'b with_bindings
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 996a2dc36..be7ebe49c 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -9,10 +9,12 @@
(************************************************************************)
open Names
-open Misctypes
(** {5 Patterns} *)
+(** Cases pattern variables *)
+type patvar = Id.t
+
type case_info_pattern =
{ cip_style : Constr.case_style;
cip_ind : inductive option;
@@ -22,7 +24,7 @@ type case_info_pattern =
type constr_pattern =
| PRef of GlobRef.t
| PVar of Id.t
- | PEvar of existential_key * constr_pattern array
+ | PEvar of Evar.t * constr_pattern array
| PRel of int
| PApp of constr_pattern * constr_pattern array
| PSoApp of patvar * constr_pattern list
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 9342b4cc7..622a8e982 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -18,7 +18,6 @@ open Constr
open Glob_term
open Pp
open Mod_subst
-open Misctypes
open Decl_kinds
open Pattern
open Environ
@@ -47,7 +46,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
| PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) ->
Name.equal v1 v2 && constr_pattern_eq b1 b2 &&
Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2
-| PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2
+| PSort s1, PSort s2 -> Glob_ops.glob_sort_eq s1 s2
| PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2
| PIf (t1, l1, r1), PIf (t2, l2, r2) ->
constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2
@@ -418,7 +417,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
pat_of_raw metas vars b1,pat_of_raw metas vars b2)
| GLetTuple (nal,(_,None),b,c) ->
let mkGLambda na c = DAst.make ?loc @@
- GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in
+ GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None),c) in
let c = List.fold_right mkGLambda nal c in
let cip =
{ cip_style = LetStyle;
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index dfbfb147f..36317b3ac 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -10,7 +10,6 @@
open Names
open Mod_subst
-open Misctypes
open Glob_term
open Pattern
open EConstr
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b2507b5f2..9e024b1c2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -45,7 +45,6 @@ open Pretype_errors
open Glob_term
open Glob_ops
open Evarconv
-open Misctypes
open Ltac_pretype
module NamedDecl = Context.Named.Declaration
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 70588b6ad..d3aa7ac64 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -30,7 +30,7 @@ type 'a hint_info_gen =
{ hint_priority : int option;
hint_pattern : 'a option }
-type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
+type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
let typeclasses_unique_solutions = ref false
let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c78382c82..e4a56960c 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -21,7 +21,7 @@ type 'a hint_info_gen =
{ hint_priority : int option;
hint_pattern : 'a option }
-type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
+type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
(** This module defines type-classes *)
type typeclass = {
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index a1ac53c73..2720a3e4d 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -18,7 +18,7 @@ type contexts = Parameters | Properties
type typeclass_error =
| NotAClass of constr
- | UnboundMethod of GlobRef.t * Misctypes.lident (* Class name, method *)
+ | UnboundMethod of GlobRef.t * lident (* Class name, method *)
exception TypeClassError of env * typeclass_error
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 1003f2ae1..9831627a9 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -16,11 +16,11 @@ type contexts = Parameters | Properties
type typeclass_error =
| NotAClass of constr
- | UnboundMethod of GlobRef.t * Misctypes.lident (** Class name, method *)
+ | UnboundMethod of GlobRef.t * lident (** Class name, method *)
exception TypeClassError of env * typeclass_error
val not_a_class : env -> constr -> 'a
-val unbound_method : env -> GlobRef.t -> Misctypes.lident -> 'a
+val unbound_method : env -> GlobRef.t -> lident -> 'a
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index bffe36eea..cf34ac016 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -197,10 +197,13 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj =
(* FIXME: might depend on the level of actual parameters!*)
let check_allowed_sort env sigma ind c p =
- let pj = Retyping.get_judgment_of env sigma p in
- let ksort = Sorts.family (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in
let specif = Global.lookup_inductive (fst ind) in
let sorts = elim_sorts specif in
+ let pj = Retyping.get_judgment_of env sigma p in
+ let _, s = splay_prod env sigma pj.uj_type in
+ let ksort = match EConstr.kind sigma s with
+ | Sort s -> Sorts.family (ESorts.kind sigma s)
+ | _ -> error_elim_arity env sigma ind sorts c pj None in
if not (List.exists ((==) ksort) sorts) then
let s = inductive_sort_family (snd specif) in
error_elim_arity env sigma ind sorts c pj
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-20 01:23:36 +0000