aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml3
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/functional_principles_types.mli6
-rw-r--r--plugins/funind/glob_term_to_relation.ml11
-rw-r--r--plugins/funind/glob_termops.ml2
-rw-r--r--plugins/funind/indfun.ml6
-rw-r--r--plugins/funind/indfun_common.ml19
-rw-r--r--plugins/funind/invfun.ml13
-rw-r--r--plugins/funind/invfun.mli10
-rw-r--r--plugins/funind/recdef.ml8
10 files changed, 37 insertions, 43 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0efb27e3f0..08298bf02c 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -14,7 +14,6 @@ open Tacticals
open Tactics
open Indfun_common
open Libnames
-open Globnames
open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
@@ -1027,7 +1026,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
update_Function
{finfos with
equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
- ConstRef c -> c
+ GlobRef.ConstRef c -> c
| _ -> CErrors.anomaly (Pp.str "Not a constant.")
)
}
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index cb7a509829..d34faa22fa 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -84,7 +84,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let env_with_params_and_predicates = List.fold_right Environ.push_named new_predicates env_with_params in
let rel_as_kn =
fst (match princ_type_info.indref with
- | Some (Globnames.IndRef ind) -> ind
+ | Some (GlobRef.IndRef ind) -> ind
| _ -> user_err Pp.(str "Not a valid predicate")
)
in
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index b4f6f92f9c..7cadd4396d 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -33,8 +33,10 @@ val generate_functional_principle :
exception No_graph_found
-val make_scheme : Evd.evar_map ref ->
- (pconstant*Sorts.family) list -> Evd.side_effects Proof_global.proof_entry list
+val make_scheme
+ : Evd.evar_map ref
+ -> (pconstant*Sorts.family) list
+ -> Evd.side_effects Proof_global.proof_entry list
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/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index bcad6cedf1..6dc01a9f8f 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -6,7 +6,6 @@ open Context
open Vars
open Glob_term
open Glob_ops
-open Globnames
open Indfun_common
open CErrors
open Util
@@ -312,7 +311,7 @@ let build_constructors_of_type ind' argl =
let npar = mib.Declarations.mind_nparams in
Array.mapi (fun i _ ->
let construct = ind',i+1 in
- let constructref = ConstructRef(construct) in
+ let constructref = GlobRef.ConstructRef(construct) in
let _implicit_positions_of_cst =
Impargs.implicits_of_global constructref
in
@@ -328,7 +327,7 @@ let build_constructors_of_type ind' argl =
List.make npar (mkGHole ()) @ argl
in
let pat_as_term =
- mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
+ mkGApp(mkGRef (GlobRef.ConstructRef(ind',i+1)),argl)
in
cases_pattern_of_glob_constr (Global.env()) Anonymous pat_as_term
)
@@ -438,7 +437,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function
let patl_as_term =
List.map2 (pattern_to_term_and_type env) (List.rev cs_args_types) patternl
in
- mkGApp(mkGRef(ConstructRef constr),
+ mkGApp(mkGRef(GlobRef.ConstructRef constr),
implicit_args@patl_as_term
)
)
@@ -992,7 +991,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
in
mkGProd(n,t,new_b),id_to_exclude
with Continue ->
- let jmeq = Globnames.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
+ let jmeq = GlobRef.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in
let ind,args' = Inductiveops.find_inductive env Evd.(from_env env) ty' in
let mib,_ = Global.lookup_inductive (fst ind) in
@@ -1001,7 +1000,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
((Util.List.chop nparam args'))
in
let rt_typ = DAst.make @@
- GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None),
+ GApp(DAst.make @@ GRef (GlobRef.IndRef (fst ind),None),
(List.map
(fun p -> Detyping.detype Detyping.Now false Id.Set.empty
env (Evd.from_env env)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 7b758da8e8..d36d86a65b 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -375,7 +375,7 @@ let rec pattern_to_term pt = DAst.with_val (function
let patl_as_term =
List.map pattern_to_term patternl
in
- mkGApp(mkGRef(Globnames.ConstructRef constr),
+ mkGApp(mkGRef(GlobRef.ConstructRef constr),
implicit_args@patl_as_term
)
) pt
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 48e3129599..6e19ef4804 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -8,7 +8,6 @@ open EConstr
open Pp
open Indfun_common
open Libnames
-open Globnames
open Glob_term
open Declarations
open Tactypes
@@ -59,7 +58,7 @@ let functional_induction with_clean c princl pat =
let princ,g' = (* then we get the principle *)
try
let g',princ =
- Tacmach.pf_eapply (Evd.fresh_global) g (Globnames.ConstRef (Option.get princ_option )) in
+ Tacmach.pf_eapply (Evd.fresh_global) g (GlobRef.ConstRef (Option.get princ_option )) in
princ,g'
with Option.IsNone ->
(*i If there is not default lemma defined then,
@@ -286,7 +285,6 @@ let derive_inversion fix_names =
(evd',[])
in
Invfun.derive_correctness
- Functional_principles_types.make_scheme
fix_names_as_constant
lind;
with e when CErrors.noncritical e ->
@@ -836,7 +834,7 @@ let make_graph (f_ref : GlobRef.t) =
let sigma = Evd.from_env env in
let c,c_body =
match f_ref with
- | ConstRef c ->
+ | GlobRef.ConstRef c ->
begin try c,Global.lookup_constant c
with Not_found ->
raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) )
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index c906670dc0..a119586f7b 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -2,7 +2,6 @@ open Names
open Pp
open Constr
open Libnames
-open Globnames
open Refiner
let mk_prefix pre id = Id.of_string (pre^(Id.to_string id))
@@ -31,12 +30,12 @@ let locate qid = Nametab.locate qid
let locate_ind ref =
match locate ref with
- | IndRef x -> x
+ | GlobRef.IndRef x -> x
| _ -> raise Not_found
let locate_constant ref =
match locate ref with
- | ConstRef x -> x
+ | GlobRef.ConstRef x -> x
| _ -> raise Not_found
@@ -129,10 +128,10 @@ let save name const ?hook uctx scope kind =
| Discharge ->
let c = SectionLocalDef const in
let () = declare_variable ~name ~kind c in
- VarRef name
+ GlobRef.VarRef name
| Global local ->
let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
- ConstRef kn
+ GlobRef.ConstRef kn
in
DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r });
definition_message name
@@ -275,7 +274,7 @@ let pr_info env sigma f_info =
str "function_constant_type := " ++
(try
Printer.pr_lconstr_env env sigma
- (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant)))
+ (fst (Typeops.type_of_global_in_context env (GlobRef.ConstRef f_info.function_constant)))
with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
str "equation_lemma := " ++ pr_ocst env sigma f_info.equation_lemma ++ fnl () ++
str "completeness_lemma :=" ++ pr_ocst env sigma f_info.completeness_lemma ++ fnl () ++
@@ -299,7 +298,7 @@ let in_Function : function_info -> Libobject.obj =
let find_or_none id =
try Some
- (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.")
+ (match Nametab.locate (qualid_of_ident id) with GlobRef.ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.")
)
with Not_found -> None
@@ -328,7 +327,7 @@ let add_Function is_general f =
and sprop_lemma = find_or_none (Nameops.add_suffix f_id "_sind")
and graph_ind =
match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
- with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.")
+ with | GlobRef.IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.")
in
let finfos =
{ function_constant = f;
@@ -433,8 +432,8 @@ let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *)
match r with
- ConstRef sp -> EvalConstRef sp
- | VarRef id -> EvalVarRef id
+ GlobRef.ConstRef sp -> EvalConstRef sp
+ | GlobRef.VarRef id -> EvalVarRef id
| _ -> assert false;;
let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 8fa001278b..f6b5a06cac 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -19,7 +19,6 @@ open Context
open EConstr
open Vars
open Pp
-open Globnames
open Tacticals
open Tactics
open Indfun_common
@@ -93,7 +92,7 @@ let make_eq () =
let generate_type evd g_to_f f graph i =
(*i we deduce the number of arguments of the function and its returned type from the graph i*)
let evd',graph =
- Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd !evd graph)))
+ Evd.fresh_global (Global.env ()) !evd (GlobRef.IndRef (fst (destInd !evd graph)))
in
evd:=evd';
let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in
@@ -165,7 +164,7 @@ let find_induction_principle evd f =
match infos.rect_lemma with
| None -> raise Not_found
| Some rect_lemma ->
- let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in
+ let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (GlobRef.ConstRef rect_lemma) in
let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
evd:=evd';
rect_lemma,typ
@@ -737,11 +736,9 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
(* [derive_correctness make_scheme funs graphs] create correctness and completeness
lemmas for each function in [funs] w.r.t. [graphs]
-
- [make_scheme] is Functional_principle_types.make_scheme (dependency pb) and
*)
-let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list) =
+let derive_correctness (funs: pconstant list) (graphs:inductive list) =
assert (funs <> []);
assert (graphs <> []);
let funs = Array.of_list funs and graphs = Array.of_list graphs in
@@ -787,7 +784,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
(fun entry ->
(EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type ))
)
- (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs))
+ (Functional_principles_types.make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs))
)
)
in
@@ -978,7 +975,7 @@ let error msg = user_err Pp.(str msg)
let invfun qhyp f =
let f =
match f with
- | ConstRef f -> f
+ | GlobRef.ConstRef f -> f
| _ -> raise (CErrors.UserError(None,str "Not a function"))
in
try
diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli
index 96601785b6..c7538fae9a 100644
--- a/plugins/funind/invfun.mli
+++ b/plugins/funind/invfun.mli
@@ -12,8 +12,8 @@ val invfun :
Tactypes.quantified_hypothesis ->
Names.GlobRef.t option ->
Evar.t Evd.sigma -> Evar.t list Evd.sigma
-val derive_correctness :
- (Evd.evar_map ref ->
- (Constr.pconstant * Sorts.family) list ->
- 'a Proof_global.proof_entry list) ->
- Constr.pconstant list -> Names.inductive list -> unit
+
+val derive_correctness
+ : Constr.pconstant list
+ -> Names.inductive list
+ -> unit
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index cab82f7067..937118bf57 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -67,7 +67,7 @@ let find_reference sl s =
let declare_fun name kind ?univs value =
let ce = definition_entry ?univs value (*FIXME *) in
- ConstRef(declare_constant ~name ~kind (DefinitionEntry ce))
+ GlobRef.ConstRef(declare_constant ~name ~kind (DefinitionEntry ce))
let defined lemma =
Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None
@@ -95,7 +95,7 @@ let type_of_const sigma t =
let constant sl s = UnivGen.constr_of_monomorphic_global (find_reference sl s)
let const_of_ref = function
- ConstRef kn -> kn
+ GlobRef.ConstRef kn -> kn
| _ -> anomaly (Pp.str "ConstRef expected.")
(* Generic values *)
@@ -1312,7 +1312,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
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
+ GlobRef.ConstRef c -> is_opaque_constant c
| _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant.")
in
let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
@@ -1454,7 +1454,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref equation_lemm
let open CVars in
let opacity =
match terminate_ref with
- | ConstRef c -> is_opaque_constant c
+ | GlobRef.ConstRef c -> is_opaque_constant c
| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
in
let evd = Evd.from_ctx uctx in
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:19:32 +0000