aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/autoinstance.ml2
-rw-r--r--toplevel/class.ml1
-rw-r--r--toplevel/classes.ml12
-rw-r--r--toplevel/classes.mli2
-rw-r--r--toplevel/command.ml11
-rw-r--r--toplevel/command.mli2
-rw-r--r--toplevel/ind_tables.ml1
-rw-r--r--toplevel/indschemes.ml1
-rw-r--r--toplevel/lemmas.ml9
-rw-r--r--toplevel/record.ml3
-rw-r--r--toplevel/vernacentries.ml24
-rw-r--r--toplevel/vernacexpr.ml7
12 files changed, 29 insertions, 46 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 7027b89ee..af1330a42 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -181,7 +181,6 @@ let declare_record_instance gr ctx params =
let def = deep_refresh_universes def in
let ce = { const_entry_body=def;
const_entry_type=None;
- const_entry_polymorphic = true;
const_entry_opaque=false } in
let cst = Declare.declare_constant ident
(DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in
@@ -197,7 +196,6 @@ let declare_class_instance gr ctx params =
let ce = Entries.DefinitionEntry
{ const_entry_type=Some typ;
const_entry_body=def;
- const_entry_polymorphic=true;
const_entry_opaque=false } in
try
let cst = Declare.declare_constant ident
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 77b49b4bd..4e729f446 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -218,7 +218,6 @@ let build_id_coercion idf_opt source =
DefinitionEntry
{ const_entry_body = mkCast (val_f, DEFAULTcast, typ_f);
const_entry_type = Some typ_f;
- const_entry_polymorphic = false;
const_entry_opaque = false } in
let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in
ConstRef kn
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 9535e9aaa..8d7581179 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -104,13 +104,12 @@ let instance_hook k pri global imps ?hook cst =
Typeclasses.add_instance inst;
(match hook with Some h -> h cst | None -> ())
-let declare_instance_constant k pri global imps ?hook poly id term termtype =
+let declare_instance_constant k pri global imps ?hook id term termtype =
let cdecl =
let kind = IsDefinition Instance in
let entry =
{ const_entry_body = term;
const_entry_type = Some termtype;
- const_entry_polymorphic = poly;
const_entry_opaque = false }
in DefinitionEntry entry, kind
in
@@ -119,7 +118,7 @@ let declare_instance_constant k pri global imps ?hook poly id term termtype =
instance_hook k pri global imps ?hook (ConstRef kn);
id
-let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) props
+let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
?(generalize=true)
?(tac:Proof_type.tactic option) ?(hook:(global_reference -> unit) option) pri =
let env = Global.env() in
@@ -255,10 +254,10 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
let evm = undefined_evars !evars in
Evarutil.check_evars env Evd.empty !evars termtype;
if Evd.is_empty evm && term <> None then
- declare_instance_constant k pri global imps ?hook poly id (Option.get term) termtype
+ declare_instance_constant k pri global imps ?hook id (Option.get term) termtype
else begin
evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars;
- let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+ let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
Flags.silently (fun () ->
Lemmas.start_proof id kind termtype (fun _ -> instance_hook k pri global imps ?hook);
if term <> None then
@@ -300,7 +299,6 @@ let rec declare_subclasses gr (rels, (tc, args)) =
let ce = {
const_entry_body = it_mkLambda_or_LetIn (mkApp (p, projargs)) rels;
const_entry_type = None;
- const_entry_polymorphic = false;
const_entry_opaque = false }
in
let cst = Declare.declare_constant ~internal:Declare.KernelSilent
@@ -341,7 +339,7 @@ let context l =
(fun (x,_) ->
match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
in
- Command.declare_assumption false (Local (* global *), false, Definitional) t
+ Command.declare_assumption false (Local (* global *), Definitional) t
[] impl (* implicit *) None (* inline *) (dummy_loc, id))
(* match class_of_constr t with *)
(* | None -> () *)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 5ef5feffd..b57f1bea0 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -40,7 +40,6 @@ val declare_instance_constant :
bool -> (** globality *)
Impargs.manual_explicitation list -> (** implicits *)
?hook:(Libnames.global_reference -> unit) ->
- polymorphic ->
identifier -> (** name *)
Term.constr -> (** body *)
Term.types -> (** type *)
@@ -49,7 +48,6 @@ val declare_instance_constant :
val new_instance :
?abstract:bool -> (** Not abstract by default. *)
?global:bool -> (** Not global by default. *)
- polymorphic ->
local_binder list ->
typeclass_constraint ->
constr_expr option ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index ea606210b..90376a431 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -64,7 +64,7 @@ let red_constant_entry n ce = function
{ ce with const_entry_body =
under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body }
-let interp_definition bl p red_option c ctypopt =
+let interp_definition bl red_option c ctypopt =
let env = Global.env() in
let evdref = ref Evd.empty in
let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in
@@ -78,7 +78,6 @@ let interp_definition bl p red_option c ctypopt =
imps1@(Impargs.lift_implicits nb_args imps2),
{ const_entry_body = body;
const_entry_type = None;
- const_entry_polymorphic = p;
const_entry_opaque = false }
| Some ctyp ->
let ty, impsty = interp_type_evars_impls ~impls ~evdref ~fail_evar:false env_bl ctyp in
@@ -90,7 +89,6 @@ let interp_definition bl p red_option c ctypopt =
imps1@(Impargs.lift_implicits nb_args imps2),
{ const_entry_body = body;
const_entry_type = Some typ;
- const_entry_polymorphic = p;
const_entry_opaque = false }
in
red_constant_entry (rel_context_length ctx) ce red_option, imps
@@ -128,7 +126,7 @@ let declare_definition ident (local,k) ce imps hook =
(* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
-let declare_assumption is_coe (local,p,kind) c imps impl nl (_,ident) =
+let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) =
let r = match local with
| Local when Lib.sections_are_opened () ->
let _ =
@@ -474,7 +472,6 @@ let declare_fix kind f def t imps =
let ce = {
const_entry_body = def;
const_entry_type = Some t;
- const_entry_polymorphic = false;
const_entry_opaque = false }
in
let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
@@ -554,7 +551,7 @@ let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
let init_tac =
Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
fixdefs) in
- Lemmas.start_proof_with_initialization (Global,false,DefinitionBody Fixpoint)
+ Lemmas.start_proof_with_initialization (Global,DefinitionBody Fixpoint)
(Some(false,indexes,init_tac)) thms None (fun _ _ -> ())
else begin
(* We shortcut the proof process *)
@@ -579,7 +576,7 @@ let declare_cofixpoint ((fixnames,fixdefs,fixtypes),fiximps) ntns =
let init_tac =
Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
fixdefs) in
- Lemmas.start_proof_with_initialization (Global,false,DefinitionBody CoFixpoint)
+ Lemmas.start_proof_with_initialization (Global,DefinitionBody CoFixpoint)
(Some(true,[],init_tac)) thms None (fun _ _ -> ())
else begin
(* We shortcut the proof process *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 0430e401a..8ffdbdec4 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -31,7 +31,7 @@ val set_declare_assumptions_hook : (types -> unit) -> unit
(** {6 Definitions/Let} *)
val interp_definition :
- local_binder list -> polymorphic -> red_expr option -> constr_expr ->
+ local_binder list -> red_expr option -> constr_expr ->
constr_expr option -> definition_entry * Impargs.manual_implicits
val declare_definition : identifier -> locality * definition_object_kind ->
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 33a842449..51dc1dc30 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -115,7 +115,6 @@ let define internal id c =
(DefinitionEntry
{ const_entry_body = c;
const_entry_type = None;
- const_entry_polymorphic = true;
const_entry_opaque = false },
Decl_kinds.IsDefinition Scheme) in
(match internal with
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index b280836af..52c9be675 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -105,7 +105,6 @@ let define id internal c t =
(DefinitionEntry
{ const_entry_body = c;
const_entry_type = t;
- const_entry_polymorphic = true;
const_entry_opaque = false },
Decl_kinds.IsDefinition Scheme) in
definition_message id;
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index a72a6b5ab..7f3edefbb 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -155,7 +155,7 @@ let look_for_possibly_mutual_statements = function
(* Saving a goal *)
-let save id const do_guard (locality,poly,kind) hook =
+let save id const do_guard (locality,kind) hook =
let const = adjust_guardness_conditions const do_guard in
let {const_entry_body = pft;
const_entry_type = tpo;
@@ -187,7 +187,7 @@ let compute_proof_name locality = function
| None ->
next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ())
-let save_remaining_recthms (local,p,kind) body opaq i (id,(t_i,(_,imps))) =
+let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
match body with
| None ->
(match local with
@@ -216,7 +216,6 @@ let save_remaining_recthms (local,p,kind) body opaq i (id,(t_i,(_,imps))) =
let const =
{ const_entry_body = body_i;
const_entry_type = Some t_i;
- const_entry_polymorphic = p;
const_entry_opaque = opaq } in
let kn = declare_constant id (DefinitionEntry const, k) in
(Global,ConstRef kn,imps)
@@ -245,7 +244,7 @@ let save_anonymous_with_strength kind opacity save_ident =
let id,const,do_guard,_,hook = get_proof opacity in
check_anonymity id save_ident;
(* we consider that non opaque behaves as local for discharge *)
- save save_ident const do_guard (Global, const.const_entry_polymorphic, Proof kind) hook
+ save save_ident const do_guard (Global, Proof kind) hook
(* Starting a goal *)
@@ -318,7 +317,7 @@ let start_proof_com kind thms hook =
let t', imps' = interp_type_evars_impls ~impls ~evdref env t in
Sign.iter_rel_context (check_evars env Evd.empty !evdref) ctx;
let ids = List.map pi1 ctx in
- (compute_proof_name (pi1 kind) sopt,
+ (compute_proof_name (fst kind) sopt,
(nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
(ids, imps @ lift_implicits (List.length ids) imps'),
guard)))
diff --git a/toplevel/record.ml b/toplevel/record.ml
index bcaf86ae3..36d29c1a1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -201,7 +201,6 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
let cie = {
const_entry_body = proj;
const_entry_type = Some projtyp;
- const_entry_polymorphic = true;
const_entry_opaque = false } in
let k = (DefinitionEntry cie,IsDefinition kind) in
let kn = declare_constant ~internal:KernelSilent fid k in
@@ -311,7 +310,6 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
let class_entry =
{ const_entry_body = class_body;
const_entry_type = class_type;
- const_entry_polymorphic = true;
const_entry_opaque = false }
in
let cst = Declare.declare_constant (snd id)
@@ -323,7 +321,6 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
let proj_entry =
{ const_entry_body = proj_body;
const_entry_type = Some proj_type;
- const_entry_polymorphic = true;
const_entry_opaque = false }
in
let proj_cst = Declare.declare_constant proj_name
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2ed871d1e..088fb3b96 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -329,13 +329,13 @@ let start_proof_and_print k l hook =
print_subgoals ();
if !pcoq <> None then (Option.get !pcoq).start_proof ()
-let vernac_definition (local,p,k) (loc,id as lid) def hook =
+let vernac_definition (local,k) (loc,id as lid) def hook =
if local = Local then Dumpglob.dump_definition lid true "var"
else Dumpglob.dump_definition lid false "def";
(match def with
| ProveBody (bl,t) -> (* local binders, typ *)
let hook _ _ = () in
- start_proof_and_print (local,p,DefinitionBody Definition)
+ start_proof_and_print (local,DefinitionBody Definition)
[Some lid, (bl,t,None)] hook
| DefineBody (bl,red_option,c,typ_opt) ->
let red_option = match red_option with
@@ -343,10 +343,10 @@ let vernac_definition (local,p,k) (loc,id as lid) def hook =
| Some r ->
let (evc,env)= get_current_context () in
Some (interp_redexp env evc r) in
- let ce,imps = interp_definition bl p red_option c typ_opt in
+ let ce,imps = interp_definition bl red_option c typ_opt in
declare_definition id (local,k) ce imps hook)
-let vernac_start_proof kind p l lettop hook =
+let vernac_start_proof kind l lettop hook =
if Dumpglob.dump () then
List.iter (fun (id, _) ->
match id with
@@ -356,7 +356,7 @@ let vernac_start_proof kind p l lettop hook =
if lettop then
errorlabstrm "Vernacentries.StartProof"
(str "Let declarations can only be used in proof editing mode.");
- start_proof_and_print (Global, p, Proof kind) l hook
+ start_proof_and_print (Global, Proof kind) l hook
let vernac_end_proof = function
| Admitted -> admit ()
@@ -380,7 +380,7 @@ let vernac_assumption kind l nl=
if Pfedit.refining () then
errorlabstrm ""
(str "Cannot declare an assumption while in proof editing mode.");
- let global = Util.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 ->
@@ -628,9 +628,9 @@ let vernac_identity_coercion stre id qids qidt =
(* Type classes *)
-let vernac_instance abst glob poly sup inst props pri =
+let vernac_instance abst glob sup inst props pri =
Dumpglob.dump_constraint inst false "inst";
- ignore(Classes.new_instance ~abstract:abst ~global:glob poly sup inst props pri)
+ ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri)
let vernac_context l =
Classes.context l
@@ -1334,7 +1334,7 @@ let interp c = match c with
(* Gallina *)
| VernacDefinition (k,lid,d,f) -> vernac_definition k lid d f
- | VernacStartTheoremProof (k,p,l,top,f) -> vernac_start_proof k p l top f
+ | VernacStartTheoremProof (k,l,top,f) -> vernac_start_proof k l top f
| VernacEndProof e -> vernac_end_proof e
| VernacExactProof c -> vernac_exact_proof c
| VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl
@@ -1365,8 +1365,8 @@ let interp c = match c with
| VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t
(* Type classes *)
- | VernacInstance (abst, glob, poly, sup, inst, props, pri) ->
- vernac_instance abst glob poly sup inst props pri
+ | VernacInstance (abst, glob, sup, inst, props, pri) ->
+ vernac_instance abst glob sup inst props pri
| VernacContext sup -> vernac_context sup
| VernacDeclareInstances (glob, ids) -> vernac_declare_instances glob ids
| VernacDeclareClass id -> vernac_declare_class id
@@ -1420,7 +1420,7 @@ let interp c = match c with
| VernacNop -> ()
(* Proof management *)
- | VernacGoal t -> vernac_start_proof Theorem false [None,([],t,None)] false (fun _ _->())
+ | VernacGoal t -> vernac_start_proof Theorem [None,([],t,None)] false (fun _ _->())
| VernacAbort id -> vernac_abort id
| VernacAbortAll -> vernac_abort_all ()
| VernacRestart -> vernac_restart ()
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 9bd6bb1b0..216306f5e 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -223,9 +223,9 @@ type vernac_expr =
scope_name option
(* Gallina *)
- | VernacDefinition of definition_kind
- * lident * definition_expr * declaration_hook
- | VernacStartTheoremProof of theorem_kind * polymorphic *
+ | VernacDefinition of definition_kind * lident * definition_expr *
+ declaration_hook
+ | VernacStartTheoremProof of theorem_kind *
(lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list *
bool * declaration_hook
| VernacEndProof of proof_end
@@ -253,7 +253,6 @@ type vernac_expr =
| VernacInstance of
bool * (* abstract instance *)
bool * (* global *)
- bool * (* polymorphic *)
local_binder list * (* super *)
typeclass_constraint * (* instance name, class name, params *)
constr_expr option * (* props *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 12:50:02 +0000