aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml6
-rw-r--r--vernac/comFixpoint.ml21
-rw-r--r--vernac/comFixpoint.mli3
-rw-r--r--vernac/declare.ml31
-rw-r--r--vernac/declare.mli2
-rw-r--r--vernac/g_vernac.mlg65
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/pfedit.ml12
-rw-r--r--vernac/proof_global.ml7
-rw-r--r--vernac/vernacentries.ml2
10 files changed, 59 insertions, 92 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index ebea5e146c..743d1d2026 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -710,7 +710,7 @@ let make_bl_scheme mode mind =
let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
let side_eff = side_effect_of_mode mode in
let bl_goal = EConstr.of_constr bl_goal in
- let (ans, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal
+ let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal
(compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, EConstr.EInstance.empty) lnamesparrec nparrec)
in
([|ans|], ctx)
@@ -843,7 +843,7 @@ let make_lb_scheme mode mind =
let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
let side_eff = side_effect_of_mode mode in
let lb_goal = EConstr.of_constr lb_goal in
- let (ans, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal
+ let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal
(compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
in
([|ans|], ctx)
@@ -1014,7 +1014,7 @@ let make_eq_decidability mode mind =
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let side_eff = side_effect_of_mode mode in
- let (ans, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx
+ let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx
~typ:(EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec))
(compute_dec_tact ind lnamesparrec nparrec)
in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index e4fa212a23..d3c1d2e767 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -53,7 +53,7 @@ let rec partial_order cmp = function
(z, Inr (List.add_set cmp x (List.remove cmp y zge)))
else
(z, Inr zge)) res in
- browse ((y,Inl x)::res) xge' (List.union cmp xge (List.remove cmp x yge))
+ browse ((y,Inl x)::res) xge' (List.union cmp xge yge)
else
browse res (List.add_set cmp y (List.union cmp xge' yge)) xge
with Not_found -> browse res (List.add_set cmp y xge') xge
@@ -82,16 +82,25 @@ let warn_non_full_mutual =
(fun (x,xge,y,yge,isfix,rest) ->
non_full_mutual_message x xge y yge isfix rest)
-let check_mutuality env evd isfix fixl =
+let warn_non_recursive =
+ CWarnings.create ~name:"non-recursive" ~category:"fixpoints"
+ (fun (x,isfix) ->
+ let k = if isfix then "fixpoint" else "cofixpoint" in
+ strbrk "Not a truly recursive " ++ str k ++ str ".")
+
+let check_true_recursivity env evd isfix fixl =
let names = List.map fst fixl in
let preorder =
List.map (fun (id,def) ->
- (id, List.filter (fun id' -> not (Id.equal id id') && Termops.occur_var env evd id' def) names))
+ (id, List.filter (fun id' -> Termops.occur_var env evd id' def) names))
fixl in
let po = partial_order Id.equal preorder in
match List.filter (function (_,Inr _) -> true | _ -> false) po with
| (x,Inr xge)::(y,Inr yge)::rest ->
warn_non_full_mutual (x,xge,y,yge,isfix,rest)
+ | _ ->
+ match po with
+ | [x,Inr []] -> warn_non_recursive (x,isfix)
| _ -> ()
let interp_fix_context ~program_mode ~cofix env sigma fix =
@@ -222,7 +231,7 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis
let check_recursive isfix env evd (fixnames,_,fixdefs,_) =
if List.for_all Option.has_some fixdefs then begin
let fixdefs = List.map Option.get fixdefs in
- check_mutuality env evd isfix (List.combine fixnames fixdefs)
+ check_true_recursivity env evd isfix (List.combine fixnames fixdefs)
end
let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) =
@@ -232,12 +241,12 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) =
Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes)
(* XXX: Unify with interp_recursive *)
-let interp_fixpoint ~cofix l :
+let interp_fixpoint ?(check_recursivity=true) ~cofix l :
( (Constr.t, Constr.types) recursive_preentry *
UState.universe_decl * UState.t *
(EConstr.rel_context * Impargs.manual_implicits * int option) list) =
let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in
- check_recursive true env evd fix;
+ if check_recursivity then check_recursive true env evd fix;
let uctx,fix = ground_fixpoint env evd fix in
(fix,pl,uctx,info)
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index a19b96f0f3..dcb61d38d9 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -58,7 +58,8 @@ val interp_recursive :
(** Exported for Funind *)
val interp_fixpoint
- : cofix:bool
+ : ?check_recursivity:bool ->
+ cofix:bool
-> lident option fix_expr_gen list
-> (Constr.t, Constr.types) recursive_preentry *
UState.universe_decl * UState.t *
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 366dd2d026..f4636c5724 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -135,11 +135,6 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified
(** Declaration of constants and parameters *)
-type constant_obj = {
- cst_kind : Decls.logical_kind;
- cst_locl : import_status;
-}
-
type 'a proof_entry = {
proof_entry_body : 'a Entries.const_entry_body;
(* List of section variables *)
@@ -265,8 +260,11 @@ type 'a constant_entry =
| ParameterEntry of Entries.parameter_entry
| PrimitiveEntry of Entries.primitive_entry
-(* At load-time, the segment starting from the module name to the discharge *)
-(* section (if Remark or Fact) is needed to access a construction *)
+type constant_obj = {
+ cst_kind : Decls.logical_kind;
+ cst_locl : import_status;
+}
+
let load_constant i ((sp,kn), obj) =
if Nametab.exists_cci sp then
raise (AlreadyDeclared (None, Libnames.basename sp));
@@ -292,8 +290,7 @@ let check_exists id =
raise (AlreadyDeclared (None, id))
let cache_constant ((sp,kn), obj) =
- (* Invariant: the constant must exist in the logical environment, except when
- redefining it when exiting a section. See [discharge_constant]. *)
+ (* Invariant: the constant must exist in the logical environment *)
let kn' =
if Global.exists_objlabel (Label.of_id (Libnames.basename sp))
then Constant.make1 kn
@@ -306,13 +303,7 @@ let cache_constant ((sp,kn), obj) =
let discharge_constant ((sp, kn), obj) =
Some obj
-(* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant cst = {
- cst_kind = cst.cst_kind;
- cst_locl = cst.cst_locl;
-}
-
-let classify_constant cst = Libobject.Substitute (dummy_constant cst)
+let classify_constant cst = Libobject.Substitute cst
let (objConstant : constant_obj Libobject.Dyn.tag) =
let open Libobject in
@@ -589,12 +580,12 @@ let fixpoint_message indexes l =
| [] -> CErrors.anomaly (Pp.str "no recursive definition.")
| [id] -> Id.print id ++ str " is recursively defined" ++
(match indexes with
- | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
+ | Some [|i|] -> str " (guarded on "++pr_rank i++str " argument)"
| _ -> mt ())
| l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
spc () ++ str "are recursively defined" ++
match indexes with
- | Some a -> spc () ++ str "(decreasing respectively on " ++
+ | Some a -> spc () ++ str "(guarded respectively on " ++
prvect_with_sep pr_comma pr_rank a ++
str " arguments)"
| None -> mt ()))
@@ -771,7 +762,7 @@ let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ t
let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
let sign = Environ.(val_of_named_context (named_context env)) in
- let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
+ let ce, status, uctx = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
let cb, uctx =
if side_eff then inline_private_constants ~uctx env ce
else
@@ -779,7 +770,7 @@ let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
let (cb, ctx), _eff = Future.force ce.proof_entry_body in
cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx
in
- cb, ce.proof_entry_type, status, univs
+ cb, ce.proof_entry_type, ce.proof_entry_universes, status, uctx
let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl =
(* EJGA: flush_and_check_evars is only used in abstract, could we
diff --git a/vernac/declare.mli b/vernac/declare.mli
index e23e148ddc..a297f25868 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -249,7 +249,7 @@ val build_by_tactic
-> poly:bool
-> typ:EConstr.types
-> unit Proofview.tactic
- -> Constr.constr * Constr.types option * bool * UState.t
+ -> Constr.constr * Constr.types option * Entries.universes_entry * bool * UState.t
(** {6 Helpers to obtain proof state when in an interactive proof } *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 13145d3757..3cb10364b5 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -68,6 +68,11 @@ let make_bullet s =
let add_control_flag ~loc ~flag { CAst.v = cmd } =
CAst.make ~loc { cmd with control = flag :: cmd.control }
+let test_hash_ident =
+ let open Pcoq.Lookahead in
+ to_entry "test_hash_ident" begin
+ lk_kw "#" >> lk_ident >> check_no_space
+ end
}
GRAMMAR EXTEND Gram
@@ -226,63 +231,9 @@ GRAMMAR EXTEND Gram
| IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> { VernacConstraint l }
] ]
;
-
- register_token:
- [ [ r = register_prim_token -> { CPrimitives.OT_op r }
- | r = register_type_token -> { CPrimitives.OT_type r } ] ]
- ;
-
- register_type_token:
- [ [ "#int63_type" -> { CPrimitives.PT_int63 }
- | "#float64_type" -> { CPrimitives.PT_float64 } ] ]
- ;
-
- register_prim_token:
- [ [ "#int63_head0" -> { CPrimitives.Int63head0 }
- | "#int63_tail0" -> { CPrimitives.Int63tail0 }
- | "#int63_add" -> { CPrimitives.Int63add }
- | "#int63_sub" -> { CPrimitives.Int63sub }
- | "#int63_mul" -> { CPrimitives.Int63mul }
- | "#int63_div" -> { CPrimitives.Int63div }
- | "#int63_mod" -> { CPrimitives.Int63mod }
- | "#int63_lsr" -> { CPrimitives.Int63lsr }
- | "#int63_lsl" -> { CPrimitives.Int63lsl }
- | "#int63_land" -> { CPrimitives.Int63land }
- | "#int63_lor" -> { CPrimitives.Int63lor }
- | "#int63_lxor" -> { CPrimitives.Int63lxor }
- | "#int63_addc" -> { CPrimitives.Int63addc }
- | "#int63_subc" -> { CPrimitives.Int63subc }
- | "#int63_addcarryc" -> { CPrimitives.Int63addCarryC }
- | "#int63_subcarryc" -> { CPrimitives.Int63subCarryC }
- | "#int63_mulc" -> { CPrimitives.Int63mulc }
- | "#int63_diveucl" -> { CPrimitives.Int63diveucl }
- | "#int63_div21" -> { CPrimitives.Int63div21 }
- | "#int63_addmuldiv" -> { CPrimitives.Int63addMulDiv }
- | "#int63_eq" -> { CPrimitives.Int63eq }
- | "#int63_lt" -> { CPrimitives.Int63lt }
- | "#int63_le" -> { CPrimitives.Int63le }
- | "#int63_compare" -> { CPrimitives.Int63compare }
- | "#float64_opp" -> { CPrimitives.Float64opp }
- | "#float64_abs" -> { CPrimitives.Float64abs }
- | "#float64_eq" -> { CPrimitives.Float64eq }
- | "#float64_lt" -> { CPrimitives.Float64lt }
- | "#float64_le" -> { CPrimitives.Float64le }
- | "#float64_compare" -> { CPrimitives.Float64compare }
- | "#float64_classify" -> { CPrimitives.Float64classify }
- | "#float64_add" -> { CPrimitives.Float64add }
- | "#float64_sub" -> { CPrimitives.Float64sub }
- | "#float64_mul" -> { CPrimitives.Float64mul }
- | "#float64_div" -> { CPrimitives.Float64div }
- | "#float64_sqrt" -> { CPrimitives.Float64sqrt }
- | "#float64_of_int63" -> { CPrimitives.Float64ofInt63 }
- | "#float64_normfr_mantissa" -> { CPrimitives.Float64normfr_mantissa }
- | "#float64_frshiftexp" -> { CPrimitives.Float64frshiftexp }
- | "#float64_ldshiftexp" -> { CPrimitives.Float64ldshiftexp }
- | "#float64_next_up" -> { CPrimitives.Float64next_up }
- | "#float64_next_down" -> { CPrimitives.Float64next_down }
- ] ]
- ;
-
+ register_token:
+ [ [ test_hash_ident; "#"; r = IDENT -> { CPrimitives.parse_op_or_type ~loc r } ] ]
+ ;
thm_token:
[ [ "Theorem" -> { Theorem }
| IDENT "Lemma" -> { Lemma }
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 060f069419..bed593234b 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -133,7 +133,7 @@ let solve_by_tac ?loc name evi t poly uctx =
try
(* the status is dropped. *)
let env = Global.env () in
- let body, types, _, uctx =
+ let body, types, _univs, _, uctx =
Declare.build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in
Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body);
Some (body, types, uctx)
diff --git a/vernac/pfedit.ml b/vernac/pfedit.ml
index d6b9592176..e6c66ee503 100644
--- a/vernac/pfedit.ml
+++ b/vernac/pfedit.ml
@@ -1,9 +1,19 @@
(* Compat API / *)
let get_current_context = Declare.get_current_context
+[@@ocaml.deprecated "Use [Declare.get_current_context]"]
let solve = Proof.solve
+[@@ocaml.deprecated "Use [Proof.solve]"]
let by = Declare.by
+[@@ocaml.deprecated "Use [Declare.by]"]
let refine_by_tactic = Proof.refine_by_tactic
+[@@ocaml.deprecated "Use [Proof.refine_by_tactic]"]
(* We don't want to export this anymore, but we do for now *)
-let build_by_tactic = Declare.build_by_tactic
+let build_by_tactic ?side_eff env ~uctx ~poly ~typ tac =
+ let b, t, _unis, safe, uctx =
+ Declare.build_by_tactic ?side_eff env ~uctx ~poly ~typ tac in
+ b, t, safe, uctx
+[@@ocaml.deprecated "Use [Proof.build_by_tactic]"]
+
let build_constant_by_tactic = Declare.build_constant_by_tactic
+[@@ocaml.deprecated "Use [Proof.build_constant_by_tactic]"]
diff --git a/vernac/proof_global.ml b/vernac/proof_global.ml
index b6c07042e2..54d1db44a4 100644
--- a/vernac/proof_global.ml
+++ b/vernac/proof_global.ml
@@ -1,7 +1,12 @@
(* compatibility module; can be removed once we agree on the API *)
type t = Declare.Proof.t
+[@@ocaml.deprecated "Use [Declare.Proof.t]"]
let map_proof = Declare.Proof.map_proof
+[@@ocaml.deprecated "Use [Declare.Proof.map_proof]"]
let get_proof = Declare.Proof.get_proof
+[@@ocaml.deprecated "Use [Declare.Proof.get_proof]"]
-type opacity_flag = Declare.opacity_flag = Opaque | Transparent
+type opacity_flag = Declare.opacity_flag =
+ | Opaque [@ocaml.deprecated "Use [Declare.Opaque]"]
+ | Transparent [@ocaml.deprecated "Use [Declare.Transparent]"]
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index df39c617d3..df94f69cf6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -475,7 +475,7 @@ let program_inference_hook env sigma ev =
Evarutil.is_ground_term sigma concl)
then None
else
- let c, _, _, ctx =
+ let c, _, _, _, ctx =
Declare.build_by_tactic ~poly:false env ~uctx:(Evd.evar_universe_context sigma) ~typ:concl tac
in
Some (Evd.set_universe_context sigma ctx, EConstr.of_constr c)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 19:30:28 +0000