aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/functional_principles_types.ml3
-rw-r--r--plugins/funind/indfun.ml4
-rw-r--r--plugins/funind/indfun_common.ml2
-rw-r--r--plugins/funind/invfun.ml4
-rw-r--r--plugins/funind/recdef.ml7
-rw-r--r--plugins/setoid_ring/newring.ml41
-rw-r--r--plugins/subtac/subtac.ml11
-rw-r--r--plugins/subtac/subtac_classes.ml2
-rw-r--r--plugins/subtac/subtac_command.ml1
-rw-r--r--plugins/subtac/subtac_obligations.ml12
-rw-r--r--plugins/subtac/subtac_utils.ml6
-rw-r--r--plugins/subtac/subtac_utils.mli6
13 files changed, 27 insertions, 34 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c1b3c0b849..4f32bbd99d 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -973,7 +973,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
Ensures by: obvious
i*)
(mk_equation_id f_id)
- (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
+ (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
lemma_type
(fun _ _ -> ());
Pfedit.by (prove_replacement);
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d3949731bc..2ba29ced7a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -333,7 +333,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
begin
Lemmas.start_proof
new_princ_name
- (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
+ (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
new_principle_type
(hook new_principle_type)
;
@@ -382,7 +382,6 @@ let generate_functional_principle
let ce =
{ const_entry_body = value;
const_entry_type = None;
- const_entry_polymorphic = false;
const_entry_opaque = false }
in
ignore(
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 0e4dd12896..dd48765fb5 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -351,9 +351,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
| [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in
let ce,imps =
- Command.interp_definition bl false None body (Some ret_type)
+ Command.interp_definition bl None body (Some ret_type)
in
- Command.declare_definition
+ Command.declare_definition
fname (Decl_kinds.Global,Decl_kinds.Definition)
ce imps (fun _ _ -> ())
| _ ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a0d2061bcd..094d2e50fd 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -156,7 +156,7 @@ let definition_message id =
Flags.if_verbose message ((string_of_id id) ^ " is defined")
-let save with_clean id const (locality,p,kind) hook =
+let save with_clean id const (locality,kind) hook =
let {const_entry_body = pft;
const_entry_type = tpo;
const_entry_opaque = opacity } = const in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ce484ca236..426b496dd1 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -788,7 +788,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
Ensures by: obvious
i*)
(mk_correct_id f_id)
- (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
+ (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
(fst lemmas_types_infos.(i))
(fun _ _ -> ());
Pfedit.by (observe_tac ("prove correctness ("^(string_of_id f_id)^")") (proving_tac i));
@@ -840,7 +840,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
Ensures by: obvious
i*)
(mk_complete_id f_id)
- (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
+ (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
(fst lemmas_types_infos.(i))
(fun _ _ -> ());
Pfedit.by (observe_tac ("prove completeness ("^(string_of_id f_id)^")") (proving_tac i));
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 24379e7b4e..11fbc01baf 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1021,7 +1021,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
in
start_proof
na
- (Decl_kinds.Global, false, Decl_kinds.Proof Decl_kinds.Lemma)
+ (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma)
sign
gls_type
hook ;
@@ -1071,7 +1071,7 @@ let com_terminate
let start_proof (tac_start:tactic) (tac_end:tactic) =
let (evmap, env) = Lemmas.get_current_context() in
start_proof thm_name
- (Global, false, Proof Lemma) (Environ.named_context_val env)
+ (Global, Proof Lemma) (Environ.named_context_val env)
(hyp_terminates nb_args fonctional_ref) hook;
by (observe_tac "starting_tac" tac_start);
@@ -1140,7 +1140,6 @@ let (declare_fun : identifier -> logical_kind -> constr -> global_reference) =
fun f_id kind value ->
let ce = {const_entry_body = value;
const_entry_type = None;
- const_entry_polymorphic = false;
const_entry_opaque = false } in
ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
@@ -1350,7 +1349,7 @@ let (com_eqn : int -> identifier ->
let (evmap, env) = Lemmas.get_current_context() in
let f_constr = (constr_of_global f_ref) in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
- (start_proof eq_name (Global, false, Proof Lemma)
+ (start_proof eq_name (Global, Proof Lemma)
(Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
by
(start_equation f_ref terminate_ref
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index d434a890f1..38c65cdd09 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -159,7 +159,6 @@ let decl_constant na c =
mkConst(declare_constant (id_of_string na) (DefinitionEntry
{ const_entry_body = c;
const_entry_type = None;
- const_entry_polymorphic = false;
const_entry_opaque = true },
IsProof Lemma))
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 7faf780330..fbdaa8d3b1 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -113,7 +113,7 @@ let dump_constraint ty ((loc, n), _, _) =
let dump_variable lid = ()
let vernac_assumption env isevars kind l nl =
- let global = pi1 kind = Global in
+ let global = fst kind = Global in
List.iter (fun (is_coe,(idl,c)) ->
if Dumpglob.dump () then
List.iter (fun lid ->
@@ -137,8 +137,7 @@ let subtac (loc, command) =
Dumpglob.dump_definition lid false "def";
(match expr with
| ProveBody (bl, t) ->
- start_proof_and_print env isevars (Some lid)
- (pi1 defkind, pi2 defkind, DefinitionBody Definition) (bl,t)
+ start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t)
(fun _ _ -> ())
| DefineBody (bl, _, c, tycon) ->
ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon))
@@ -149,7 +148,7 @@ let subtac (loc, command) =
let _ = trace (str "Building fixpoint") in
ignore(Subtac_command.build_recursive l)
- | VernacStartTheoremProof (thkind, p, [Some id, (bl,t,guard)], lettop, hook) ->
+ | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) ->
if guard <> None then
error "Do not support building theorems as a fixpoint.";
Dumpglob.dump_definition id false "prf";
@@ -161,12 +160,12 @@ let subtac (loc, command) =
errorlabstrm "Subtac_command.StartProof"
(str "Proof editing mode not supported in module types");
check_fresh id;
- start_proof_and_print env isevars (Some id) (Global, p, Proof thkind) (bl,t) hook
+ start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
| VernacAssumption (stre,nl,l) ->
vernac_assumption env isevars stre l nl
- | VernacInstance (abst, glob, poly, sup, is, props, pri) ->
+ | VernacInstance (abst, glob, sup, is, props, pri) ->
dump_constraint "inst" is;
if abst then
error "Declare Instance not supported here.";
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 0a3da4d0c8..05e634c58b 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -180,4 +180,4 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
in
let evm = Subtac_utils.evars_of_term !evars Evd.empty term in
let obls, _, constr, typ = Eterm.eterm_obligations env id !evars evm 0 term termtype in
- id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,false,Instance) ~hook obls
+ id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,Instance) ~hook obls
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 5c7f7b5ec0..f02e83ad1a 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -327,7 +327,6 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
let ce =
{ const_entry_body = Evarutil.nf_evar !isevars body;
const_entry_type = Some ty;
- const_entry_polymorphic = false;
const_entry_opaque = false }
in
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 874cce85c9..76cc7644d6 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -231,11 +231,10 @@ let subst_body expand prg =
let declare_definition prg =
let body, typ = subst_body true prg in
- let (local, poly, kind) = prg.prg_kind in
+ let (local, kind) = prg.prg_kind in
let ce =
{ const_entry_body = body;
const_entry_type = Some typ;
- const_entry_polymorphic = poly;
const_entry_opaque = false }
in
(Command.get_declare_definition_hook ()) ce;
@@ -254,7 +253,7 @@ let declare_definition prg =
| (Global|Local) ->
let c =
Declare.declare_constant
- prg.prg_name (DefinitionEntry ce,IsDefinition (pi3 prg.prg_kind))
+ prg.prg_name (DefinitionEntry ce,IsDefinition (snd prg.prg_kind))
in
let gr = ConstRef c in
if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
@@ -302,7 +301,7 @@ let declare_mutual_definition l =
let fixkind = Option.get first.prg_fixkind in
let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
- let (local,poly,kind) = first.prg_kind in
+ let (local,kind) = first.prg_kind in
let fixnames = first.prg_deps in
let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
let indexes, fixdecls =
@@ -335,7 +334,6 @@ let declare_obligation prg obl body =
let ce =
{ const_entry_body = body;
const_entry_type = Some ty;
- const_entry_polymorphic = false;
const_entry_opaque = opaque }
in
let constant = Declare.declare_constant obl.obl_name
@@ -604,7 +602,7 @@ let show_term n =
my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
++ my_print_constr (Global.env ()) prg.prg_body)
-let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
@@ -622,7 +620,7 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?ta
| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
| _ -> res)
-let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
+let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
?(hook=fun _ _ -> ()) notations fixkind =
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
let upd = List.fold_left
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 6487a14b7f..7fba23dc23 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -218,13 +218,13 @@ let non_instanciated_map env evd evm =
Evd.empty (Evarutil.non_instantiated evm)
let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
-let goal_kind = Decl_kinds.Global, false, Decl_kinds.DefinitionBody Decl_kinds.Definition
+let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma
-let goal_proof_kind = Decl_kinds.Global, false, Decl_kinds.Proof Decl_kinds.Lemma
+let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma
let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint
-let goal_fix_kind = Decl_kinds.Global, false, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
+let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
open Tactics
open Tacticals
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index d2c3fd0c8c..2753a2522c 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -95,11 +95,11 @@ val string_of_hole_kind : hole_kind -> string
val evars_of_term : evar_map -> evar_map -> constr -> evar_map
val non_instanciated_map : env -> evar_map ref -> evar_map -> evar_map
val global_kind : logical_kind
-val goal_kind : locality * polymorphic * goal_object_kind
+val goal_kind : locality * goal_object_kind
val global_proof_kind : logical_kind
-val goal_proof_kind : locality * polymorphic * goal_object_kind
+val goal_proof_kind : locality * goal_object_kind
val global_fix_kind : logical_kind
-val goal_fix_kind : locality * polymorphic * goal_object_kind
+val goal_fix_kind : locality * goal_object_kind
val mkSubset : name -> constr -> constr -> constr
val mkProj1 : constr -> constr -> constr -> constr
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:22:24 +0000