aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_types.ml20
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/funind/glob_termops.ml6
-rw-r--r--plugins/funind/indfun.ml6
-rw-r--r--plugins/funind/indfun_common.ml31
-rw-r--r--plugins/funind/invfun.ml2
6 files changed, 16 insertions, 53 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index b2a528a1fd..f7094ebe51 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -322,7 +322,8 @@ let generate_functional_principle (evd: Evd.evar_map ref)
try
let f = funs.(i) in
- let type_sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd InType in
+ let sigma, type_sort = Evd.fresh_sort_in_family !evd InType in
+ evd := sigma;
let new_sorts =
match sorts with
| None -> Array.make (Array.length funs) (type_sort)
@@ -394,7 +395,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
exception Not_Rec
-let get_funs_constant mp dp =
+let get_funs_constant mp =
let get_funs_constant const e : (Names.Constant.t*int) array =
match Constr.kind ((strip_lam e)) with
| Fix((_,(na,_,_))) ->
@@ -402,7 +403,7 @@ let get_funs_constant mp dp =
(fun i na ->
match na with
| Name id ->
- let const = Constant.make3 mp dp (Label.of_id id) in
+ let const = Constant.make2 mp (Label.of_id id) in
const,i
| Anonymous ->
anomaly (Pp.str "Anonymous fix.")
@@ -474,13 +475,13 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
let env = Global.env () in
let funs = List.map fst fas in
let first_fun = List.hd funs in
- let funs_mp,funs_dp,_ = KerName.repr (Constant.canonical (fst first_fun)) in
+ let funs_mp = KerName.modpath (Constant.canonical (fst first_fun)) in
let first_fun_kn =
try
fst (find_Function_infos (fst first_fun)).graph_ind
with Not_found -> raise No_graph_found
in
- let this_block_funs_indexes = get_funs_constant funs_mp funs_dp (fst first_fun) in
+ let this_block_funs_indexes = get_funs_constant funs_mp (fst first_fun) in
let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in
let prop_sort = InProp in
let funs_indexes =
@@ -507,8 +508,9 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
let i = ref (-1) in
let sorts =
List.rev_map (fun (_,x) ->
- Evarutil.evd_comb1 Evd.fresh_sort_in_family evd x
- )
+ let sigma, fs = Evd.fresh_sort_in_family !evd x in
+ evd := sigma; fs
+ )
fas
in
(* We create the first priciple by tactic *)
@@ -669,9 +671,9 @@ let build_case_scheme fa =
user_err ~hdr:"FunInd.build_case_scheme"
(str "Cannot find " ++ Libnames.pr_qualid f) in
let first_fun,u = destConst funs in
- let funs_mp,funs_dp,_ = Constant.repr3 first_fun in
+ let funs_mp = Constant.modpath first_fun in
let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in
- let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
+ let this_block_funs_indexes = get_funs_constant funs_mp first_fun in
let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
let prop_sort = InProp in
let funs_indexes =
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..9a6169d42a 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
@@ -900,11 +898,11 @@ let make_graph (f_ref : GlobRef.t) =
let id = Label.to_id (Constant.label c) in
[((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
in
- let mp,dp,_ = Constant.repr3 c in
+ let mp = Constant.modpath c in
do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list;
(* We register the infos *)
List.iter
- (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
+ (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id)))
expr_list)
let do_generate_principle = do_generate_principle [] warning_error true
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 4eee2c7a45..6ed382ca1c 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -297,36 +297,7 @@ let subst_Function (subst,finfos) =
let classify_Function infos = Libobject.Substitute infos
-let discharge_Function (_,finfos) =
- let function_constant' = Lib.discharge_con finfos.function_constant
- and graph_ind' = Lib.discharge_inductive finfos.graph_ind
- and equation_lemma' = Option.Smart.map Lib.discharge_con finfos.equation_lemma
- and correctness_lemma' = Option.Smart.map Lib.discharge_con finfos.correctness_lemma
- and completeness_lemma' = Option.Smart.map Lib.discharge_con finfos.completeness_lemma
- and rect_lemma' = Option.Smart.map Lib.discharge_con finfos.rect_lemma
- and rec_lemma' = Option.Smart.map Lib.discharge_con finfos.rec_lemma
- and prop_lemma' = Option.Smart.map Lib.discharge_con finfos.prop_lemma
- in
- if function_constant' == finfos.function_constant &&
- graph_ind' == finfos.graph_ind &&
- equation_lemma' == finfos.equation_lemma &&
- correctness_lemma' == finfos.correctness_lemma &&
- completeness_lemma' == finfos.completeness_lemma &&
- rect_lemma' == finfos.rect_lemma &&
- rec_lemma' == finfos.rec_lemma &&
- prop_lemma' == finfos.prop_lemma
- then Some finfos
- else
- Some { function_constant = function_constant' ;
- graph_ind = graph_ind' ;
- equation_lemma = equation_lemma' ;
- correctness_lemma = correctness_lemma' ;
- completeness_lemma = completeness_lemma';
- rect_lemma = rect_lemma';
- rec_lemma = rec_lemma';
- prop_lemma = prop_lemma' ;
- is_general = finfos.is_general
- }
+let discharge_Function (_,finfos) = Some finfos
let pr_ocst c =
let sigma, env = Pfedit.get_current_context () in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ad11f853ca..56fe430077 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -450,7 +450,7 @@ let generalize_dependent_of x hyp g =
let tauto =
let dp = List.map Id.of_string ["Tauto" ; "Init"; "Coq"] in
let mp = ModPath.MPfile (DirPath.make dp) in
- let kn = KerName.make2 mp (Label.make "tauto") in
+ let kn = KerName.make mp (Label.make "tauto") in
Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
let body = Tacenv.interp_ltac kn in
Tacinterp.eval_tactic body
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 05:40:42 +0000