aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/functional_principles_types.ml4
-rw-r--r--plugins/funind/g_indfun.mlg18
-rw-r--r--plugins/funind/gen_principle.ml7
-rw-r--r--plugins/funind/glob_term_to_relation.ml37
-rw-r--r--plugins/funind/glob_termops.ml6
-rw-r--r--plugins/funind/indfun_common.ml4
-rw-r--r--plugins/funind/invfun.ml3
-rw-r--r--plugins/funind/recdef.ml2
9 files changed, 43 insertions, 40 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index e50c6087bb..73eb943418 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -674,7 +674,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
|Prod _ ->
let new_infos = {dyn_infos with info = (f, args)} in
build_proof_args env sigma do_finalize new_infos
- | Const (c, _) when not (List.mem_f Constant.equal c fnames) ->
+ | Const (c, _) when not (List.mem_f Constant.CanOrd.equal c fnames) ->
let new_infos = {dyn_infos with info = (f, args)} in
(* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *)
build_proof_args env sigma do_finalize new_infos
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1ab747ca09..0ab9ac65d7 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -100,8 +100,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
let is_dom c =
match Constr.kind c with
- | Ind ((u, _), _) -> MutInd.equal u rel_as_kn
- | Construct (((u, _), _), _) -> MutInd.equal u rel_as_kn
+ | Ind ((u, _), _) -> Environ.QMutInd.equal env u rel_as_kn
+ | Construct (((u, _), _), _) -> Environ.QMutInd.equal env u rel_as_kn
| _ -> false
in
let get_fun_num c =
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index bbc4df7dde..ca6ae150a7 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -147,19 +147,19 @@ END
module Vernac = Pvernac.Vernac_
module Tactic = Pltac
-let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) =
- Genarg.create_arg "function_rec_definition_loc"
+let (wit_function_fix_definition : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) =
+ Genarg.create_arg "function_fix_definition"
-let function_rec_definition_loc =
- Pcoq.create_generic_entry2 "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
+let function_fix_definition =
+ Pcoq.create_generic_entry2 "function_fix_definition" (Genarg.rawwit wit_function_fix_definition)
}
GRAMMAR EXTEND Gram
- GLOBAL: function_rec_definition_loc ;
+ GLOBAL: function_fix_definition ;
- function_rec_definition_loc:
- [ [ g = Vernac.rec_definition -> { Loc.tag ~loc g } ]]
+ function_fix_definition:
+ [ [ g = Vernac.fix_definition -> { Loc.tag ~loc g } ]]
;
END
@@ -168,7 +168,7 @@ END
let () =
let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
- Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer
+ Pptactic.declare_extra_vernac_genarg_pprule wit_function_fix_definition raw_printer
let is_proof_termination_interactively_checked recsl =
List.exists (function
@@ -196,7 +196,7 @@ let is_interactive recsl =
}
VERNAC COMMAND EXTEND Function STATE CUSTOM
-| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
+| ["Function" ne_function_fix_definition_list_sep(recsl,"with")]
=> { classify_funind recsl }
-> {
if is_interactive recsl then
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 012fcee486..314c8abcaf 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1316,9 +1316,9 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list =
let prop_sort = Sorts.InProp in
let funs_indexes =
let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
+ let eq c1 c2 = Environ.QConstant.equal env c1 c2 in
List.map
- (function
- | cst -> List.assoc_f Constant.equal (fst cst) this_block_funs_indexes)
+ (function cst -> List.assoc_f eq (fst cst) this_block_funs_indexes)
funs
in
let ind_list =
@@ -2228,7 +2228,8 @@ let build_case_scheme fa =
let prop_sort = Sorts.InProp in
let funs_indexes =
let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
- List.assoc_f Constant.equal funs this_block_funs_indexes
+ let eq c1 c2 = Environ.QConstant.equal env c1 c2 in
+ List.assoc_f eq funs this_block_funs_indexes
in
let ind, sf =
let ind = (first_fun_kn, funs_indexes) in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 6ed61043f9..5bfb37f4cb 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -332,7 +332,7 @@ let add_pat_variables sigma pat typ env : Environ.env =
let constructors = Inductiveops.get_constructors env indf in
let constructor : Inductiveops.constructor_summary =
List.find
- (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr))
+ (fun cs -> Construct.CanOrd.equal c (fst cs.Inductiveops.cs_cstr))
(Array.to_list constructors)
in
let cs_args_types : types list =
@@ -402,7 +402,8 @@ let rec pattern_to_term_and_type env typ =
let constructors = Inductiveops.get_constructors env indf in
let constructor =
List.find
- (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr)
+ (fun cs ->
+ Construct.CanOrd.equal (fst cs.Inductiveops.cs_cstr) constr)
(Array.to_list constructors)
in
let cs_args_types : types list =
@@ -457,9 +458,11 @@ let rec pattern_to_term_and_type env typ =
but only the value of the function
*)
+let pr_glob_constr_env env x = pr_glob_constr_env env (Evd.from_env env) x
+
let rec build_entry_lc env sigma funnames avoid rt :
glob_constr build_entry_return =
- observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt);
+ observe (str " Entering : " ++ pr_glob_constr_env env rt);
let open CAst in
match DAst.get rt with
| GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _
@@ -637,9 +640,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
with Not_found ->
user_err
( str "Cannot find the inductive associated to "
- ++ Printer.pr_glob_constr_env env b
- ++ str " in "
- ++ Printer.pr_glob_constr_env env rt
+ ++ pr_glob_constr_env env b ++ str " in " ++ pr_glob_constr_env env rt
++ str ". try again with a cast" )
in
let case_pats = build_constructors_of_type (fst ind) [] in
@@ -661,9 +662,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
with Not_found ->
user_err
( str "Cannot find the inductive associated to "
- ++ Printer.pr_glob_constr_env env b
- ++ str " in "
- ++ Printer.pr_glob_constr_env env rt
+ ++ pr_glob_constr_env env b ++ str " in " ++ pr_glob_constr_env env rt
++ str ". try again with a cast" )
in
let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
@@ -1320,11 +1319,11 @@ let do_build_inductive evd (funconstants : pconstant list)
@@ Constrexpr.CLetIn
( CAst.make n
, with_full_print
- (Constrextern.extern_glob_constr Id.Set.empty)
+ Constrextern.(extern_glob_constr empty_extern_env)
t
, Some
(with_full_print
- (Constrextern.extern_glob_constr Id.Set.empty)
+ Constrextern.(extern_glob_constr empty_extern_env)
typ)
, acc )
| None ->
@@ -1334,7 +1333,7 @@ let do_build_inductive evd (funconstants : pconstant list)
( [CAst.make n]
, Constrexpr_ops.default_binder_kind
, with_full_print
- (Constrextern.extern_glob_constr Id.Set.empty)
+ Constrextern.(extern_glob_constr empty_extern_env)
t ) ]
, acc ))
rel_first_args
@@ -1409,11 +1408,11 @@ let do_build_inductive evd (funconstants : pconstant list)
@@ Constrexpr.CLetIn
( CAst.make n
, with_full_print
- (Constrextern.extern_glob_constr Id.Set.empty)
+ Constrextern.(extern_glob_constr empty_extern_env)
t
, Some
(with_full_print
- (Constrextern.extern_glob_constr Id.Set.empty)
+ Constrextern.(extern_glob_constr empty_extern_env)
typ)
, acc )
| None ->
@@ -1423,7 +1422,7 @@ let do_build_inductive evd (funconstants : pconstant list)
( [CAst.make n]
, Constrexpr_ops.default_binder_kind
, with_full_print
- (Constrextern.extern_glob_constr Id.Set.empty)
+ Constrextern.(extern_glob_constr empty_extern_env)
t ) ]
, acc ))
rel_first_args
@@ -1447,16 +1446,16 @@ let do_build_inductive evd (funconstants : pconstant list)
| Some typ ->
Constrexpr.CLocalDef
( CAst.make n
- , Constrextern.extern_glob_constr Id.Set.empty t
+ , Constrextern.(extern_glob_constr empty_extern_env) t
, Some
(with_full_print
- (Constrextern.extern_glob_constr Id.Set.empty)
+ Constrextern.(extern_glob_constr empty_extern_env)
typ) )
| None ->
Constrexpr.CLocalAssum
( [CAst.make n]
, Constrexpr_ops.default_binder_kind
- , Constrextern.extern_glob_constr Id.Set.empty t ))
+ , Constrextern.(extern_glob_constr empty_extern_env) t ))
rels_params
in
let ext_rels_constructors =
@@ -1465,7 +1464,7 @@ let do_build_inductive evd (funconstants : pconstant list)
( false
, ( CAst.make id
, with_full_print
- (Constrextern.extern_glob_type Id.Set.empty)
+ Constrextern.(extern_glob_type empty_extern_env)
((* zeta_normalize *) alpha_rt rel_params_ids t) ) )))
rel_constructors
in
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 8e1331ace9..164a446fe3 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -444,7 +444,8 @@ let rec are_unifiable_aux = function
match (DAst.get l, DAst.get r) with
| PatVar _, _ | _, PatVar _ -> are_unifiable_aux eqs
| PatCstr (constructor1, cpl1, _), PatCstr (constructor2, cpl2, _) ->
- if not (eq_constructor constructor2 constructor1) then raise NotUnifiable
+ if not (Construct.CanOrd.equal constructor2 constructor1) then
+ raise NotUnifiable
else
let eqs' =
try List.combine cpl1 cpl2 @ eqs
@@ -464,7 +465,8 @@ let rec eq_cases_pattern_aux = function
match (DAst.get l, DAst.get r) with
| PatVar _, PatVar _ -> eq_cases_pattern_aux eqs
| PatCstr (constructor1, cpl1, _), PatCstr (constructor2, cpl2, _) ->
- if not (eq_constructor constructor2 constructor1) then raise NotUnifiable
+ if not (Construct.CanOrd.equal constructor2 constructor1) then
+ raise NotUnifiable
else
let eqs' =
try List.combine cpl1 cpl2 @ eqs
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 0179215d6a..6464556e4e 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -108,7 +108,7 @@ let with_full_print f a =
Constrextern.print_universes := old_printuniverses;
Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name
old_printallowmatchdefaultclause;
- Dumpglob.continue ();
+ Dumpglob.pop_output ();
res
with reraise ->
Impargs.make_implicit_args old_implicit_args;
@@ -118,7 +118,7 @@ let with_full_print f a =
Constrextern.print_universes := old_printuniverses;
Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name
old_printallowmatchdefaultclause;
- Dumpglob.continue ();
+ Dumpglob.pop_output ();
raise reraise
(**********************)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 5d631aac84..118a917381 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -27,12 +27,13 @@ open Indfun_common
*)
let revert_graph kn post_tac hid =
Proofview.Goal.enter (fun gl ->
+ let env = Proofview.Goal.env gl in
let sigma = project gl in
let typ = pf_get_hyp_typ hid gl in
match EConstr.kind sigma typ with
| App (i, args) when isInd sigma i ->
let ((kn', num) as ind'), u = destInd sigma i in
- if MutInd.equal kn kn' then
+ if Environ.QMutInd.equal env kn kn' then
(* We have generated a graph hypothesis so that we must change it if we can *)
let info =
match find_Function_of_graph ind' with
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 33076a876b..9d896e9182 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -776,7 +776,7 @@ let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos
let a' = infos.info in
let new_info =
{ infos with
- info = mkCase (ci, t, iv, a', l)
+ info = mkCase (ci, a, iv, a', l)
; is_main_branch = expr_info.is_main_branch
; is_final = expr_info.is_final }
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 15:55:00 +0000