aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/detyping.ml12
-rw-r--r--pretyping/glob_ops.ml10
-rw-r--r--pretyping/glob_term.ml1
-rw-r--r--pretyping/patternops.ml3
-rw-r--r--pretyping/pretyping.ml14
-rw-r--r--pretyping/typeclasses.ml14
-rw-r--r--pretyping/typeclasses.mli3
-rw-r--r--pretyping/unification.ml5
8 files changed, 11 insertions, 51 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6a9a042f57..0dc5a9bad5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -675,8 +675,12 @@ and detype_r d flags avoid env sigma t =
(Array.map_to_list (detype d flags avoid env sigma) args)
| Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u)
| Proj (p,c) ->
- let noparams () =
- GProj (p, detype d flags avoid env sigma c)
+ let noparams () =
+ let pars = Projection.npars p in
+ let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Namegen.IntroAnonymous,None) in
+ let args = List.make pars hole in
+ GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None),
+ (args @ [detype d flags avoid env sigma c]))
in
if fst flags || !Flags.in_debugger || !Flags.in_toplevel then
try noparams ()
@@ -1030,10 +1034,6 @@ let rec subst_glob_constr subst = DAst.map (function
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 ->
- let p' = subst_proj subst p in
- let c' = subst_glob_constr subst c in
- if p' == p && c' == c then raw else GProj(p', c')
)
(* Utilities to transform kernel cases to simple pattern-matching problem *)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index bd13f1d00a..9b2da0b084 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -152,10 +152,8 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
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) ->
- Projection.equal p1 p2 && f t1 t2
| (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ |
- GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ | GProj _), _ -> false
+ GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ ), _ -> false
let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
@@ -216,8 +214,6 @@ let map_glob_constr_left_to_right f = DAst.map (function
let comp1 = f c in
let comp2 = map_cast_type f k in
GCast (comp1,comp2)
- | GProj (p,c) ->
- GProj (p, f c)
| (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x
)
@@ -250,8 +246,6 @@ let fold_glob_constr f acc = DAst.with_val (function
let acc = match k with
| CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in
f acc c
- | GProj(_,c) ->
- f acc c
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
)
@@ -295,8 +289,6 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
let acc = match k with
| CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in
f v acc c
- | GProj(_,c) ->
- f v acc c
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc))
let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 86245d4794..c6fdb0ec14 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -82,7 +82,6 @@ type 'a glob_constr_r =
| GSort of glob_sort
| 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
and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index f7fea22c0f..3c1c470053 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -464,9 +464,6 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
one non-trivial branch. These facts are used in [Constrextern]. *)
PCase (info, pred, pat_of_raw metas vars c, brs)
- | GProj(p,c) ->
- PProj(p, pat_of_raw metas vars c)
-
| GRec (GFix (ln,n), ids, decls, tl, cl) ->
if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then
err ?loc (Pp.str "\"struct\" annotation is expected.")
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 162adf0626..1b7f32bcae 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -613,11 +613,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
let j = pretype_sort ?loc evdref s in
inh_conv_coerce_to_tycon ?loc env evdref j tycon
- | GProj (p, c) ->
- (* TODO: once GProj is used as an input syntax, use bidirectional typing here *)
- let cj = pretype empty_tycon env evdref c in
- judge_of_projection !!env !evdref p cj
-
| GApp (f,args) ->
let fj = pretype empty_tycon env evdref f in
let floc = loc_of_glob_constr f in
@@ -795,9 +790,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
| [], [] -> []
| _ -> assert false
in aux 1 1 (List.rev nal) cs.cs_args, true in
- let fsign = if Flags.version_strictly_greater Flags.V8_6
- then Context.Rel.map (whd_betaiota !evdref) fsign
- else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in
+ let fsign = Context.Rel.map (whd_betaiota !evdref) fsign in
let fsign,env_f = push_rel_context !evdref fsign env in
let obj ind p v f =
if not record then
@@ -896,10 +889,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
let pi = lift n pred in (* liftn n 2 pred ? *)
let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in
- let cs_args =
- if Flags.version_strictly_greater Flags.V8_6
- then Context.Rel.map (whd_betaiota !evdref) cs_args
- else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in
+ let cs_args = Context.Rel.map (whd_betaiota !evdref) cs_args in
let csgn =
List.map (set_name Anonymous) cs_args
in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 55d9838bbb..67c5643459 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -11,7 +11,6 @@
(*i*)
open Names
open Globnames
-open Decl_kinds
open Term
open Constr
open Vars
@@ -482,19 +481,6 @@ let instances r =
let is_class gr =
GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
-let is_instance = function
- | ConstRef c ->
- (match Decls.constant_kind c with
- | IsDefinition Instance -> true
- | _ -> false)
- | VarRef v ->
- (match Decls.variable_kind v with
- | IsDefinition Instance -> true
- | _ -> false)
- | ConstructRef (ind,_) ->
- is_class (IndRef ind)
- | _ -> false
-
(* To embed a boolean for resolvability status.
This is essentially a hack to mark which evars correspond to
goals and do not need to be resolved when we have nested [resolve_all_evars]
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 80c6d82397..f0437be4ed 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -79,13 +79,12 @@ val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass
(** Just return None if not a class *)
val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option
-
+
val instance_impl : instance -> GlobRef.t
val hint_priority : instance -> int option
val is_class : GlobRef.t -> bool
-val is_instance : GlobRef.t -> bool
(** Returns the term and type for the given instance of the parameters and fields
of the type class. *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e223674579..4665486fc0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -193,10 +193,7 @@ let pose_all_metas_as_evars env evd t =
| None ->
let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
- let ty =
- if Flags.version_strictly_greater Flags.V8_6
- then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *)
- else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in
+ let ty = nf_betaiota env evd ty in
let src = Evd.evar_source_of_meta mv !evdref in
let evd, ev = Evarutil.new_evar env !evdref ~src ty in
evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) evd;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 07:05:22 +0000