aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_types.ml4
-rw-r--r--plugins/funind/functional_principles_types.mli4
-rw-r--r--plugins/funind/g_indfun.ml46
-rw-r--r--plugins/funind/indfun.ml43
-rw-r--r--plugins/funind/indfun_common.ml4
-rw-r--r--plugins/funind/indfun_common.mli8
-rw-r--r--plugins/funind/recdef.ml4
7 files changed, 33 insertions, 40 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index a158fc8ff..31496513a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -627,7 +627,7 @@ let build_scheme fas =
Smartlocate.global_with_alias f
with Not_found ->
user_err ~hdr:"FunInd.build_scheme"
- (str "Cannot find " ++ Libnames.pr_reference f)
+ (str "Cannot find " ++ Libnames.pr_qualid f)
in
let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
let _ = evd := evd' in
@@ -668,7 +668,7 @@ let build_case_scheme fa =
try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f))
with Not_found ->
user_err ~hdr:"FunInd.build_case_scheme"
- (str "Cannot find " ++ Libnames.pr_reference f) in
+ (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 first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 33aeafef8..97f9acdb3 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -36,5 +36,5 @@ exception No_graph_found
val make_scheme : Evd.evar_map ref ->
(pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list
-val build_scheme : (Id.t*Libnames.reference*Sorts.family) list -> unit
-val build_case_scheme : (Id.t*Libnames.reference*Sorts.family) -> unit
+val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit
+val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 9899b7b21..a2d31780d 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -168,7 +168,7 @@ END
let pr_fun_scheme_arg (princ_name,fun_name,s) =
Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
- Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++
+ Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++
Termops.pr_sort_family s
VERNAC ARGUMENT EXTEND fun_scheme_arg
@@ -181,11 +181,11 @@ let warning_error names e =
let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in
match e with
| Building_graph e ->
- let names = pr_enum Libnames.pr_reference names in
+ let names = pr_enum Libnames.pr_qualid names in
let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in
warn_cannot_define_graph (names,error)
| Defining_principle e ->
- let names = pr_enum Libnames.pr_reference names in
+ let names = pr_enum Libnames.pr_qualid names in
let error = if do_observe () then CErrors.print e else mt () in
warn_cannot_define_principle (names,error)
| _ -> raise e
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index cd640eebd..489a40ed0 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -362,17 +362,17 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
(*i The next call to mk_rel_id is valid since we have just construct the graph
Ensures by : do_built
i*)
- let f_R_mut = CAst.make @@ Ident (mk_rel_id (List.nth names 0)) in
+ let f_R_mut = qualid_of_ident @@ mk_rel_id (List.nth names 0) in
let ind_kn =
fst (locate_with_msg
- (pr_reference f_R_mut++str ": Not an inductive type!")
+ (pr_qualid f_R_mut++str ": Not an inductive type!")
locate_ind
f_R_mut)
in
let fname_kn (((fname,_),_,_,_,_),_) =
- let f_ref = CAst.map (fun n -> Ident n) fname in
- locate_with_msg
- (pr_reference f_ref++str ": Not an inductive type!")
+ let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in
+ locate_with_msg
+ (pr_qualid f_ref++str ": Not an inductive type!")
locate_constant
f_ref
in
@@ -477,7 +477,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
let unbounded_eq =
let f_app_args =
CAst.make @@ Constrexpr.CAppExpl(
- (None,CAst.make @@ Ident fname,None) ,
+ (None,qualid_of_ident fname,None) ,
(List.map
(function
| {CAst.v=Anonymous} -> assert false
@@ -487,7 +487,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
)
)
in
- CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (CAst.make @@ Qualid (qualid_of_string "Logic.eq"))),
+ CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (qualid_of_string "Logic.eq")),
[(f_app_args,None);(body,None)])
in
let eq = Constrexpr_ops.mkCProdN args unbounded_eq in
@@ -544,9 +544,9 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
| None ->
let ltof =
let make_dir l = DirPath.make (List.rev_map Id.of_string l) in
- CAst.make @@ Libnames.Qualid (Libnames.qualid_of_path
- (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")))
- in
+ Libnames.qualid_of_path
+ (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))
+ in
let fun_from_mes =
let applied_mes =
Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in
@@ -727,12 +727,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof
()
let rec add_args id new_args = CAst.map (function
- | CRef (r,_) as b ->
- begin match r with
- | {CAst.v=Libnames.Ident fname} when Id.equal fname id ->
- CAppExpl((None,r,None),new_args)
- | _ -> b
- end
+ | CRef (qid,_) as b ->
+ if qualid_is_ident qid && Id.equal (qualid_basename qid) id then
+ CAppExpl((None,qid,None),new_args)
+ else b
| CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.")
| CProdN(nal,b1) ->
CProdN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2)
@@ -746,13 +744,10 @@ let rec add_args id new_args = CAst.map (function
add_args id new_args b1)
| CLetIn(na,b1,t,b2) ->
CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2)
- | CAppExpl((pf,r,us),exprl) ->
- begin
- match r with
- | {CAst.v=Libnames.Ident fname} when Id.equal fname id ->
- CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl))
- | _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl)
- end
+ | CAppExpl((pf,qid,us),exprl) ->
+ if qualid_is_ident qid && Id.equal (qualid_basename qid) id then
+ CAppExpl((pf,qid,us),new_args@(List.map (add_args id new_args) exprl))
+ else CAppExpl((pf,qid,us),List.map (add_args id new_args) exprl)
| CApp((pf,b),bl) ->
CApp((pf,add_args id new_args b),
List.map (fun (e,o) -> add_args id new_args e,o) bl)
@@ -888,7 +883,7 @@ let make_graph (f_ref : GlobRef.t) =
| Constrexpr.CLocalAssum (nal,_,_) ->
List.map
(fun {CAst.loc;v=n} -> CAst.make ?loc @@
- CRef(CAst.make ?loc @@ Libnames.Ident(Nameops.Name.get_id n),None))
+ CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None))
nal
| Constrexpr.CLocalPattern _ -> assert false
)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index c6faa142a..4eee2c7a4 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -31,9 +31,7 @@ let id_of_name = function
Name id -> id
| _ -> raise Not_found
-let locate ref =
- let {CAst.v=qid} = qualid_of_reference ref in
- Nametab.locate qid
+let locate qid = Nametab.locate qid
let locate_ind ref =
match locate ref with
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 346b21ef2..7e52ee224 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -20,11 +20,11 @@ val array_get_start : 'a array -> 'a array
val id_of_name : Name.t -> Id.t
-val locate_ind : Libnames.reference -> inductive
-val locate_constant : Libnames.reference -> Constant.t
+val locate_ind : Libnames.qualid -> inductive
+val locate_constant : Libnames.qualid -> Constant.t
val locate_with_msg :
- Pp.t -> (Libnames.reference -> 'a) ->
- Libnames.reference -> 'a
+ Pp.t -> (Libnames.qualid -> 'a) ->
+ Libnames.qualid -> 'a
val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list
val list_union_eq :
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index aa49148fc..7298342e1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1325,7 +1325,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials");
let hook _ _ =
let opacity =
- let na_ref = CAst.make @@ Libnames.Ident na in
+ let na_ref = qualid_of_ident na in
let na_global = Smartlocate.global_with_alias na_ref in
match na_global with
ConstRef c -> is_opaque_constant c
@@ -1577,7 +1577,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let hook _ _ =
let term_ref = Nametab.locate (qualid_of_ident term_id) in
let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
- let _ = Extraction_plugin.Table.extraction_inline true [CAst.make @@ Ident term_id] in
+ let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in
(* message "start second proof"; *)
let stop =
try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-26 18:31:19 +0000