aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrexpr.ml1
-rw-r--r--interp/constrexpr_ops.ml8
-rw-r--r--interp/constrextern.ml3
-rw-r--r--interp/constrintern.ml7
-rw-r--r--interp/notation_ops.ml17
-rw-r--r--interp/notation_term.ml1
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/funind/glob_termops.ml6
-rw-r--r--plugins/funind/indfun.ml2
-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.ml5
-rw-r--r--printing/ppconstr.ml3
-rw-r--r--printing/proof_diffs.ml2
-rw-r--r--test-suite/output/UnivBinders.out2
17 files changed, 12 insertions, 75 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index d8dd4ef6dd..77d612cfd9 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -114,7 +114,6 @@ and constr_expr_r =
| CGeneralization of binding_kind * abstraction_kind option * constr_expr
| CPrim of prim_token
| CDelimiters of string * constr_expr
- | CProj of qualid * constr_expr
and constr_expr = constr_expr_r CAst.t
and case_expr = constr_expr (* expression that is being matched *)
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 011c4a6e4e..23d0536df8 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -177,12 +177,10 @@ let rec constr_expr_eq e1 e2 =
| CDelimiters(s1,e1), CDelimiters(s2,e2) ->
String.equal s1 s2 &&
constr_expr_eq e1 e2
- | CProj(p1,c1), CProj(p2,c2) ->
- qualid_eq p1 p2 && constr_expr_eq c1 c2
| (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
| CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
| CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
- | CGeneralization _ | CDelimiters _ | CProj _), _ -> false
+ | CGeneralization _ | CDelimiters _ ), _ -> false
and args_eq (a1,e1) (a2,e2) =
Option.equal (eq_ast explicitation_eq) e1 e2 &&
@@ -359,8 +357,6 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
(fold_local_binders g f n acc t lb) c lb) l acc
| CCoFix (_,_) ->
Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc
- | CProj (_,c) ->
- f n acc c
)
let free_vars_of_constr_expr c =
@@ -439,8 +435,6 @@ let map_constr_expr_with_binders g f e = CAst.map (function
let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in
let d' = f e'' d in
(id,bl',t',d')) dl)
- | CProj (p,c) ->
- CProj (p, f e c)
)
(* Used in constrintern *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3996a1756c..98e1f6dd36 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -958,9 +958,6 @@ let rec extern inctx scopes vars r =
| GCast (c, c') ->
CCast (sub_extern true scopes vars c,
map_cast_type (extern_typ scopes vars) c')
- | GProj (p, c) ->
- let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in
- CProj (pr, sub_extern inctx scopes vars c)
in insert_coercion coercion (CAst.make ?loc c)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1c8d957014..d02f59414e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2062,13 +2062,6 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| CCast (c1, c2) ->
DAst.make ?loc @@
GCast (intern env c1, map_cast_type (intern_type env) c2)
- | CProj (pr, c) ->
- match intern_reference pr with
- | ConstRef p ->
- let p = Option.get @@ Recordops.find_primitive_projection p in
- DAst.make ?loc @@ GProj (Projection.make p false, intern env c)
- | _ ->
- raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *)
)
and intern_type env = intern (set_type_scope env)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 06943ce7b9..ff5e2bb5f3 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -89,11 +89,9 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
glob_sort_eq s1 s2
| NCast (t1, c1), NCast (t2, c2) ->
(eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
-| NProj (p1, c1), NProj (p2, c2) ->
- Projection.equal p1 p2 && eq_notation_constr vars c1 c2
| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
| NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
- | NRec _ | NSort _ | NCast _ | NProj _), _ -> false
+ | NRec _ | NSort _ | NCast _ ), _ -> false
(**********************************************************************)
(* Re-interpret a notation as a glob_constr, taking care of binders *)
@@ -220,7 +218,6 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
| NSort x -> GSort x
| NHole (x, naming, arg) -> GHole (x, naming, arg)
| NRef x -> GRef (x,None)
- | NProj (p,c) -> GProj (p, f e c)
let glob_constr_of_notation_constr ?loc x =
let rec aux () x =
@@ -440,7 +437,6 @@ let notation_constr_and_vars_of_glob_constr recvars a =
if arg != None then has_ltac := true;
NHole (w, naming, arg)
| GRef (r,_) -> NRef r
- | GProj (p, c) -> NProj (p, aux c)
| GEvar _ | GPatVar _ ->
user_err Pp.(str "Existential variables not allowed in notations.")
) x
@@ -640,12 +636,6 @@ let rec subst_notation_constr subst bound raw =
let k' = smartmap_cast_type (subst_notation_constr subst bound) k in
if r1' == r1 && k' == k then raw else NCast(r1',k')
- | NProj (p, c) ->
- let p' = subst_proj subst p in
- let c' = subst_notation_constr subst bound c in
- if p' == p && c' == c then raw else NProj(p', c')
-
-
let subst_interpretation subst (metas,pat) =
let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in
(metas,subst_notation_constr subst bound pat)
@@ -1218,12 +1208,9 @@ let rec match_ inner u alp metas sigma a1 a2 =
match_names metas (alp,sigma) (Name id') na in
match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2
- | GProj(p1, t1), NProj(p2, t2) when Projection.equal p1 p2 ->
- match_in u alp metas sigma t1 t2
-
| (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
| GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
- | GCast _ | GProj _ ), _ -> raise No_match
+ | GCast _ ), _ -> raise No_match
and match_in u = match_ true u
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 942ea5ff3f..5fb0ca1b43 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -43,7 +43,6 @@ type notation_constr =
notation_constr array * notation_constr array
| NSort of glob_sort
| NCast of notation_constr * notation_constr cast_type
- | NProj of Projection.t * notation_constr
(** Note concerning NList: first constr is iterator, second is terminator;
first id is where each argument of the list has to be substituted
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index fd2d90e9cf..0c45de4dc4 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -590,7 +590,6 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
*)
build_entry_lc env funnames avoid (mkGApp(b,args))
| GRec _ -> user_err Pp.(str "Not handled GRec")
- | GProj _ -> user_err Pp.(str "Funind does not support primitive projections")
| GProd _ -> user_err Pp.(str "Cannot apply a type")
end (* end of the application treatement *)
@@ -696,7 +695,6 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GCast(b,_) ->
build_entry_lc env funnames avoid b
- | GProj(_,_) -> user_err Pp.(str "Funind does not support primitive projections")
and build_entry_lc_from_case env funname make_discr
(el:tomatch_tuples)
(brl:Glob_term.cases_clauses) avoid :
@@ -1246,7 +1244,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function
discrimination ones *)
| GSort _ -> params
| GHole _ -> params
- | GIf _ | GRec _ | GCast _ | GProj _ ->
+ | GIf _ | GRec _ | GCast _ ->
raise (UserError(Some "compute_cst_params", str "Not handled case"))
) gt
and compute_cst_params_from_app acc (params,rtl) =
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 954fc3bab4..f81de82d5e 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -109,7 +109,6 @@ let change_vars =
| GCast(b,c) ->
GCast(change_vars mapping b,
Glob_ops.map_cast_type (change_vars mapping) c)
- | GProj(p,c) -> GProj(p, change_vars mapping c)
) rt
and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) =
let new_mapping = List.fold_right Id.Map.remove idl mapping in
@@ -294,7 +293,6 @@ let rec alpha_rt excluded rt =
GApp(alpha_rt excluded f,
List.map (alpha_rt excluded) args
)
- | GProj(p,c) -> GProj(p, alpha_rt excluded c)
in
new_rt
@@ -346,7 +344,6 @@ let is_free_in id =
| GHole _ -> false
| GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
| GCast (b,CastCoerce) -> is_free_in b
- | GProj (_,c) -> is_free_in c
) x
and is_free_in_br {CAst.v=(ids,_,rt)} =
(not (Id.List.mem id ids)) && is_free_in rt
@@ -440,8 +437,6 @@ let replace_var_by_term x_id term =
| GCast(b,c) ->
GCast(replace_var_by_pattern b,
Glob_ops.map_cast_type replace_var_by_pattern c)
- | GProj(p,c) ->
- GProj(p,replace_var_by_pattern c)
) x
and replace_var_by_pattern_br ({CAst.loc;v=(idl,patl,res)} as br) =
if List.exists (fun id -> Id.compare id x_id == 0) idl
@@ -545,7 +540,6 @@ let expand_as =
| GCases(sty,po,el,brl) ->
GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
List.map (expand_as_br map) brl)
- | GProj(p,c) -> GProj(p, expand_as map c)
)
and expand_as_br map {CAst.loc; v=(idl,cpl,rt)} =
CAst.make ?loc (idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e114a0119e..9eda19a86b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -222,7 +222,6 @@ let is_rec names =
| GCases(_,_,el,brl) ->
List.exists (fun (e,_) -> lookup names e) el ||
List.exists (lookup_br names) brl
- | GProj(_,c) -> lookup names c
and lookup_br names {CAst.v=(idl,_,rt)} =
let new_names = List.fold_right Id.Set.remove idl names in
lookup new_names rt
@@ -783,7 +782,6 @@ let rec add_args id new_args = CAst.map (function
| CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
| CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.")
| CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.")
- | CProj _ -> user_err Pp.(str "Funind does not support primitive projections")
)
exception Stop of Constrexpr.constr_expr
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..a40c0d2375 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
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 418e13759b..90d2b7abaf 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -675,9 +675,6 @@ let tag_var = tag Tag.variable
return (pr_prim_token p, prec_of_prim_token p)
| CDelimiters (sc,a) ->
return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim)
- | CProj (p,c) ->
- let p = pr_proj (pr mt) pr_app c (CAst.make (CRef (p,None))) [] in
- return (p, lproj)
in
let loc = constr_loc a in
pr_with_comments ?loc
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 5bb1053645..0b630b39b5 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -523,8 +523,6 @@ let match_goals ot nt =
| CPrim p, CPrim p2 -> ()
| CDelimiters (key,e), CDelimiters (key2,e2) ->
constr_expr ogname e e2
- | CProj (pr,c), CProj (pr2,c2) ->
- constr_expr ogname c c2
| _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (5)")
end
in
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index f8f11d7cf6..1e50ba511a 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -5,7 +5,7 @@ PWrap has primitive projections with eta conversion.
For PWrap: Argument scope is [type_scope]
For pwrap: Argument scopes are [type_scope _]
punwrap@{u} =
-fun (A : Type@{u}) (p : PWrap@{u} A) => p.(punwrap)
+fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
: forall A : Type@{u}, PWrap@{u} A -> A
(* u |= *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:15:39 +0000