aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/glob_term_to_relation.ml20
-rw-r--r--plugins/funind/glob_termops.ml7
-rw-r--r--plugins/funind/indfun.ml1
-rw-r--r--plugins/funind/merge.ml4
4 files changed, 11 insertions, 21 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 6d22743652..4f308af5eb 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -405,7 +405,7 @@ let rec pattern_to_term_and_type env typ = function
Array.to_list
(Array.init
(cst_narg - List.length patternl)
- (fun i -> Detyping.detype false [] (Termops.names_of_rel_context env) Evd.empty csta.(i))
+ (fun i -> Detyping.detype false [] env Evd.empty csta.(i))
)
in
let patl_as_term =
@@ -488,7 +488,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
*)
let rt_as_constr,ctx = Pretyping.understand env Evd.empty rt in
let rt_typ = Typing.type_of env Evd.empty rt_as_constr in
- let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) Evd.empty rt_typ in
+ let res_raw_type = Detyping.detype false [] env Evd.empty rt_typ in
let res = fresh_id args_res.to_avoid "_res" in
let new_avoid = res::args_res.to_avoid in
let res_rt = mkGVar res in
@@ -559,7 +559,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 _ -> error "Not handled GRec"
- | GProj _ -> error "Not handled GProj"
| GProd _ -> error "Cannot apply a type"
end (* end of the application treatement *)
@@ -662,7 +661,6 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
end
| GRec _ -> error "Not handled GRec"
- | GProj _ -> error "Not handled GProj"
| GCast(_,b,_) ->
build_entry_lc env funnames avoid b
and build_entry_lc_from_case env funname make_discr
@@ -743,7 +741,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
in
let raw_typ_of_id =
Detyping.detype false []
- (Termops.names_of_rel_context env_with_pat_ids) Evd.empty typ_of_id
+ env_with_pat_ids Evd.empty typ_of_id
in
mkGProd (Name id,raw_typ_of_id,acc))
pat_ids
@@ -787,7 +785,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
List.map3
(fun pat e typ_as_constr ->
let this_pat_ids = ids_of_pat pat in
- let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) Evd.empty typ_as_constr in
+ let typ = Detyping.detype false [] new_env Evd.empty typ_as_constr in
let pat_as_term = pattern_to_term pat in
List.fold_right
(fun id acc ->
@@ -795,7 +793,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
then (Prod (Name id),
let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in
let raw_typ_of_id =
- Detyping.detype false [] (Termops.names_of_rel_context new_env) Evd.empty typ_of_id
+ Detyping.detype false [] new_env Evd.empty typ_of_id
in
raw_typ_of_id
)::acc
@@ -951,7 +949,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
GRef (Loc.ghost,Globnames.IndRef (fst ind),None),
(List.map
(fun p -> Detyping.detype false []
- (Termops.names_of_rel_context env) Evd.empty
+ env Evd.empty
p) params)@(Array.to_list
(Array.make
(List.length args' - nparam)
@@ -979,12 +977,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| Anonymous -> acc
| Name id' ->
(id',Detyping.detype false []
- (Termops.names_of_rel_context env)
+ env
Evd.empty
arg)::acc
else if isVar var_as_constr
then (destVar var_as_constr,Detyping.detype false []
- (Termops.names_of_rel_context env)
+ env
Evd.empty
arg)::acc
else acc
@@ -1183,7 +1181,7 @@ let rec compute_cst_params relnames params = function
discriminitation ones *)
| GSort _ -> params
| GHole _ -> params
- | GIf _ | GRec _ | GCast _ | GProj _->
+ | GIf _ | GRec _ | GCast _ ->
raise (UserError("compute_cst_params", str "Not handled case"))
and compute_cst_params_from_app acc (params,rtl) =
match params,rtl with
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 4cdea414eb..e55ede968a 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -180,7 +180,6 @@ let change_vars =
| GRec _ -> error "Local (co)fixes are not supported"
| GSort _ -> rt
| GHole _ -> rt
- | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GCast(loc,b,c) ->
GCast(loc,change_vars mapping b,
Miscops.map_cast_type (change_vars mapping) c)
@@ -358,7 +357,6 @@ let rec alpha_rt excluded rt =
alpha_rt excluded rhs
)
| GRec _ -> error "Not handled GRec"
- | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GSort _ -> rt
| GHole _ -> rt
| GCast (loc,b,c) ->
@@ -409,7 +407,6 @@ let is_free_in id =
| GIf(_,cond,_,br1,br2) ->
is_free_in cond || is_free_in br1 || is_free_in br2
| GRec _ -> raise (UserError("",str "Not handled GRec"))
- | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GSort _ -> false
| GHole _ -> false
| GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
@@ -506,7 +503,6 @@ let replace_var_by_term x_id term =
replace_var_by_pattern rhs
)
| GRec _ -> raise (UserError("",str "Not handled GRec"))
- | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GSort _ -> rt
| GHole _ -> rt
| GCast(loc,b,c) ->
@@ -602,7 +598,6 @@ let ids_of_glob_constr c =
| GCases (loc,sty,rtntypopt,tml,brchl) ->
List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl)
| GRec _ -> failwith "Fix inside a constructor branch"
- | GProj _ -> error "Native projections are not supported" (** FIXME *)
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> []
in
(* build the set *)
@@ -661,7 +656,6 @@ let zeta_normalize =
zeta_normalize_term rhs
)
| GRec _ -> raise (UserError("",str "Not handled GRec"))
- | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GSort _ -> rt
| GHole _ -> rt
| GCast(loc,b,c) ->
@@ -704,7 +698,6 @@ let expand_as =
GIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
expand_as map br1, expand_as map br2)
| GRec _ -> error "Not handled GRec"
- | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GCast(loc,b,c) ->
GCast(loc,expand_as map b,
Miscops.map_cast_type (expand_as map) c)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index cd35a09a1d..be84f2ed44 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -181,7 +181,6 @@ let is_rec names =
let rec lookup names = function
| GVar(_,id) -> check_id id names
| GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false
- | GProj (loc, p, c) -> lookup names c
| GCast(_,b,_) -> lookup names b
| GRec _ -> error "GRec not handled"
| GIf(_,b,_,lhs,rhs) ->
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 669b77e038..8e3c0ba9c2 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -773,7 +773,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
let mkrawcor nme avoid typ =
(* first replace rel 1 by a varname *)
let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
- Detyping.detype false (Id.Set.elements avoid) [] Evd.empty substindtyp in
+ Detyping.detype false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in
let lcstr1: glob_constr list =
Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
(* add to avoid all indentifiers of lcstr1 *)
@@ -854,7 +854,7 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
match rdecl with
| (nme,None,t) ->
- let traw = Detyping.detype false [] [] Evd.empty t in
+ let traw = Detyping.detype false [] (Global.env()) Evd.empty t in
GProd (Loc.ghost,nme,Explicit,traw,t2)
| (_,Some _,_) -> assert false
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:18:57 +0000