diff options
| author | Pierre-Marie Pédrot | 2019-06-24 13:24:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-25 17:51:01 +0200 |
| commit | 803c1dbf2de4e4fe1e447a69b9e5c48d19a72f5f (patch) | |
| tree | 14a3c6edead32f558a7703313413565483b9ba8c /vernac | |
| parent | 82bccc5d62cbdcf0d79d8a85c98ca19823a33629 (diff) | |
Remove the internal_flag argument from Declare API.
It was never used actually.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 2 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 8 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
4 files changed, 7 insertions, 7 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 8addfa054e..35108744cd 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -337,7 +337,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id + let cst = Declare.declare_constant id (Declare.ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); instance_hook pri global imps (ConstRef cst) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index e791118db2..e91d8b9d3e 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -280,7 +280,7 @@ let context ~poly l = let entry = Declare.definition_entry ~univs ~types:t b in (Declare.DefinitionEntry entry, IsAssumption Logical) in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in + let cst = Declare.declare_constant id decl in let env = Global.env () in Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst); status diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index b393f33d5d..9559edbea0 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -100,8 +100,8 @@ let () = (* Util *) -let define ~poly id internal sigma c t = - let f = declare_constant ~internal in +let define ~poly id sigma c t = + let f = declare_constant in let univs = Evd.univ_entry ~poly sigma in let open Proof_global in let kn = f id @@ -415,7 +415,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in let decltype = EConstr.to_constr sigma decltype in let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in - let cst = define ~poly fi UserIndividualRequest sigma proof_output (Some decltype) in + let cst = define ~poly fi sigma proof_output (Some decltype) in ConstRef cst :: lrecref in let _ = List.fold_right2 declare listdecl lrecnames [] in @@ -544,7 +544,7 @@ let do_combined_scheme name schemes = some other polymorphism they can also manually define the combined scheme. *) let poly = Global.is_polymorphic (ConstRef (List.hd csts)) in - ignore (define ~poly name.v UserIndividualRequest sigma proof_output (Some typ)); + ignore (define ~poly name.v sigma proof_output (Some typ)); fixpoint_message None [name.v] (**********************************************************************) diff --git a/vernac/record.ml b/vernac/record.ml index 268c778674..cc4f02349d 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -353,7 +353,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f proof_entry_inline_code = false; proof_entry_feedback = None } in let k = (Declare.DefinitionEntry entry,IsDefinition kind) in - let kn = declare_constant ~internal:InternalTacticRequest fid k in + let kn = declare_constant fid k in let constr_fip = let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in applist (mkConstU (kn,u),proj_args) |