aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml12
-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.ml415
-rw-r--r--plugins/funind/glob_term_to_relation.ml1
-rw-r--r--plugins/funind/glob_termops.ml14
-rw-r--r--plugins/funind/indfun.ml47
-rw-r--r--plugins/funind/indfun.mli2
-rw-r--r--plugins/funind/indfun_common.ml6
-rw-r--r--plugins/funind/indfun_common.mli8
-rw-r--r--plugins/funind/invfun.ml8
-rw-r--r--plugins/funind/invfun.mli2
-rw-r--r--plugins/funind/recdef.ml12
13 files changed, 66 insertions, 69 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5e0d3e8eed..5336948642 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -230,7 +230,7 @@ let isAppConstruct ?(env=Global.env ()) sigma t =
with Not_found -> false
let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
- Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty
+ Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env @@ Evd.from_env Environ.empty_env
exception NoChange
@@ -598,7 +598,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
Proofview.V82.of_tactic (intro_using heq_id);
onLastHypId (fun heq_id -> tclTHENLIST [
(* Then the new hypothesis *)
- tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps;
+ tclMAP (fun id -> Proofview.V82.of_tactic (introduction id)) dyn_infos.rec_hyps;
observe_tac "after_introduction" (fun g' ->
(* We get infos on the equations introduced*)
let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in
@@ -1099,10 +1099,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let get_body const =
match Global.body_of_constant const with
| Some (body, _) ->
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
Tacred.cbv_norm_flags
(CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
- (Global.env ())
- (Evd.empty)
+ env
+ sigma
(EConstr.of_constr body)
| None -> user_err Pp.(str "Cannot define a principle over an axiom ")
in
@@ -1340,7 +1342,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
nb_rec_hyps = -100;
rec_hyps = [];
info =
- Reductionops.nf_betaiota (pf_env g) Evd.empty
+ Reductionops.nf_betaiota (pf_env g) (project g)
(applist(fbody_with_full_params,
(List.rev_map var_of_decl princ_params)@
(List.rev_map mkVar args_id)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index a158fc8ffc..31496513a7 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 33aeafef81..97f9acdb3a 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 90af20b4ca..a2d31780dd 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -15,7 +15,8 @@ open Indfun_common
open Indfun
open Genarg
open Stdarg
-open Misctypes
+open Tacarg
+open Tactypes
open Pcoq
open Pcoq.Prim
open Pcoq.Constr
@@ -38,7 +39,9 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
match opt_c with
| None -> mt ()
| Some b ->
- let (_, b) = b (Global.env ()) Evd.empty in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let (_, b) = b env evd in
spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
@@ -123,7 +126,7 @@ ARGUMENT EXTEND auto_using'
END
module Gram = Pcoq.Gram
-module Vernac = Pcoq.Vernac_
+module Vernac = Pvernac.Vernac_
module Tactic = Pltac
type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
@@ -165,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
@@ -178,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/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 3ba3bafa44..6b9b103122 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -10,7 +10,6 @@ open Indfun_common
open CErrors
open Util
open Glob_termops
-open Misctypes
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index ae238b846c..954fc3bab4 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,10 +1,10 @@
open Pp
+open Constr
open Glob_term
open CErrors
open Util
open Names
open Decl_kinds
-open Misctypes
(*
Some basic functions to rebuild glob_constr
@@ -16,8 +16,8 @@ let mkGApp(rt,rtl) = DAst.make @@ GApp(rt,rtl)
let mkGLambda(n,t,b) = DAst.make @@ GLambda(n,Explicit,t,b)
let mkGProd(n,t,b) = DAst.make @@ GProd(n,Explicit,t,b)
let mkGLetIn(n,b,t,c) = DAst.make @@ GLetIn(n,b,t,c)
-let mkGCases(rto,l,brl) = DAst.make @@ GCases(Term.RegularStyle,rto,l,brl)
-let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
+let mkGCases(rto,l,brl) = DAst.make @@ GCases(RegularStyle,rto,l,brl)
+let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None)
(*
Some basic functions to decompose glob_constrs
@@ -108,7 +108,7 @@ let change_vars =
| GHole _ as x -> x
| GCast(b,c) ->
GCast(change_vars mapping b,
- Miscops.map_cast_type (change_vars mapping) c)
+ 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) =
@@ -289,7 +289,7 @@ let rec alpha_rt excluded rt =
| GHole _ as rt -> rt
| GCast (b,c) ->
GCast(alpha_rt excluded b,
- Miscops.map_cast_type (alpha_rt excluded) c)
+ Glob_ops.map_cast_type (alpha_rt excluded) c)
| GApp(f,args) ->
GApp(alpha_rt excluded f,
List.map (alpha_rt excluded) args
@@ -439,7 +439,7 @@ let replace_var_by_term x_id term =
| GHole _ as rt -> rt
| GCast(b,c) ->
GCast(replace_var_by_pattern b,
- Miscops.map_cast_type replace_var_by_pattern c)
+ Glob_ops.map_cast_type replace_var_by_pattern c)
| GProj(p,c) ->
GProj(p,replace_var_by_pattern c)
) x
@@ -541,7 +541,7 @@ let expand_as =
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GCast(b,c) ->
GCast(expand_as map b,
- Miscops.map_cast_type (expand_as map) c)
+ Glob_ops.map_cast_type (expand_as map) c)
| 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)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index efbd029e48..489a40ed09 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -10,7 +10,7 @@ open Libnames
open Globnames
open Glob_term
open Declarations
-open Misctypes
+open Tactypes
open Decl_kinds
module RelDecl = Context.Rel.Declaration
@@ -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)
@@ -782,7 +777,7 @@ let rec add_args id new_args = CAst.map (function
| CSort _ as b -> b
| CCast(b1,b2) ->
CCast(add_args id new_args b1,
- Miscops.map_cast_type (add_args id new_args) b2)
+ Glob_ops.map_cast_type (add_args id new_args) b2)
| CRecord pars ->
CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars)
| CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
@@ -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.mli b/plugins/funind/indfun.mli
index 24304e361b..f209fb19fd 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,5 +1,5 @@
open Names
-open Misctypes
+open Tactypes
val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b0c9ff8fcb..4eee2c7a45 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
@@ -109,7 +107,7 @@ let const_of_id id =
let def_of_const t =
match Constr.kind t with
- Term.Const sp ->
+ Const sp ->
(try (match Environ.constant_opt_value_in (Global.env()) sp with
| Some c -> c
| _ -> assert false)
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 346b21ef2a..7e52ee224f 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/invfun.ml b/plugins/funind/invfun.ml
index b9d5ebf57c..439274240f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -23,7 +23,7 @@ open Tacticals
open Tactics
open Indfun_common
open Tacmach
-open Misctypes
+open Tactypes
open Termops
open Context.Rel.Declaration
@@ -67,7 +67,7 @@ let observe_tac s tac g =
let nf_zeta =
Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
Environ.empty_env
- Evd.empty
+ (Evd.from_env Environ.empty_env)
let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
@@ -239,7 +239,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
List.map
(fun decl ->
List.map
- (fun id -> CAst.make @@ IntroNaming (IntroIdentifier id))
+ (fun id -> CAst.make @@ IntroNaming (Namegen.IntroIdentifier id))
(generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl)))))
)
branches
@@ -257,7 +257,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
List.fold_right
(fun {CAst.v=pat} acc ->
match pat with
- | IntroNaming (IntroIdentifier id) -> id::acc
+ | IntroNaming (Namegen.IntroIdentifier id) -> id::acc
| _ -> anomaly (Pp.str "Not an identifier.")
)
(List.nth intro_pats (pred i))
diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli
index 9151fd0e28..3ddc609201 100644
--- a/plugins/funind/invfun.mli
+++ b/plugins/funind/invfun.mli
@@ -9,7 +9,7 @@
(************************************************************************)
val invfun :
- Misctypes.quantified_hypothesis ->
+ Tactypes.quantified_hypothesis ->
Names.GlobRef.t option ->
Evar.t Evd.sigma -> Evar.t list Evd.sigma
val derive_correctness :
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ab03f18310..7298342e1e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -37,7 +37,7 @@ open Glob_term
open Pretyping
open Termops
open Constrintern
-open Misctypes
+open Tactypes
open Genredexpr
open Equality
@@ -106,12 +106,12 @@ let const_of_ref = function
let nf_zeta env =
Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
- env
- Evd.empty
+ env (Evd.from_env env)
let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
- Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty
+ Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env
+ (Evd.from_env Environ.empty_env)
@@ -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.25.1) at 2026-03-08 10:23:53 +0000