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/indschemes.ml | |
| parent | 82bccc5d62cbdcf0d79d8a85c98ca19823a33629 (diff) | |
Remove the internal_flag argument from Declare API.
It was never used actually.
Diffstat (limited to 'vernac/indschemes.ml')
| -rw-r--r-- | vernac/indschemes.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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] (**********************************************************************) |