aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml198
-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/declaremods.ml97
-rw-r--r--vernac/g_vernac.mlg65
-rw-r--r--vernac/himsg.ml6
-rw-r--r--vernac/library.ml81
-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
13 files changed, 254 insertions, 273 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 215d5d97a0..743d1d2026 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -122,6 +122,53 @@ let check_no_indices mib =
let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
+let build_beq_scheme_deps kn =
+ (* fetching global env *)
+ let env = Global.env() in
+ (* fetching the mutual inductive body *)
+ let mib = Global.lookup_mind kn in
+ (* number of inductives in the mutual *)
+ let nb_ind = Array.length mib.mind_packets in
+ (* number of params in the type *)
+ let nparrec = mib.mind_nparams_rec in
+ check_no_indices mib;
+ let make_one_eq accu i =
+ (* This function is only trying to recursively compute the inductive types
+ appearing as arguments of the constructors. This is done to support
+ equality decision over hereditarily first-order types. It could be
+ perfomed in a much cleaner way, e.g. using the kernel normal form of
+ constructor types and kernel whd_all for the argument types. *)
+ let rec aux accu c =
+ let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in
+ let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in
+ match Constr.kind c with
+ | Cast (x,_,_) -> aux accu (Term.applist (x,a))
+ | App _ -> assert false
+ | Ind ((kn', _), _) ->
+ if MutInd.equal kn kn' then accu
+ else
+ let eff = SchemeMutualDep (kn', !beq_scheme_kind_aux ()) in
+ List.fold_left aux (eff :: accu) a
+ | Const (kn, u) ->
+ (match Environ.constant_opt_value_in env (kn, u) with
+ | Some c -> aux accu (Term.applist (c,a))
+ | None -> accu)
+ | Rel _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | Proj _
+ | Construct _ | Case _ | CoFix _ | Fix _ | Meta _ | Evar _ | Int _
+ | Float _ -> accu
+ in
+ let u = Univ.Instance.empty in
+ let constrs n = get_constructors env (make_ind_family (((kn, i), u),
+ Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt)) in
+ let constrsi = constrs (3+nparrec) in
+ let fold i accu arg =
+ let fold accu c = aux accu (RelDecl.get_type c) in
+ List.fold_left fold accu arg.cs_args
+ in
+ Array.fold_left_i fold accu constrsi
+ in
+ Array.fold_left_i (fun i accu _ -> make_one_eq accu i) [] mib.mind_packets
+
let build_beq_scheme mode kn =
check_bool_is_defined ();
(* fetching global env *)
@@ -194,7 +241,7 @@ let build_beq_scheme mode kn =
let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in
let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in
match Constr.kind c with
- | Rel x -> mkRel (x-nlist+ndx), Evd.empty_side_effects
+ | Rel x -> mkRel (x-nlist+ndx)
| Var x ->
(* Support for working in a context with "eq_x : x -> x -> bool" *)
let eid = Id.of_string ("eq_"^(Id.to_string x)) in
@@ -202,26 +249,23 @@ let build_beq_scheme mode kn =
try ignore (Environ.lookup_named eid env)
with Not_found -> raise (ParameterWithoutEquality (GlobRef.VarRef x))
in
- mkVar eid, Evd.empty_side_effects
+ mkVar eid
| Cast (x,_,_) -> aux (Term.applist (x,a))
| App _ -> assert false
| Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
- if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Evd.empty_side_effects
+ if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
else begin
try
- let eq, eff =
- let c, eff = find_scheme ~mode (!beq_scheme_kind_aux()) (kn',i) in
- mkConst c, eff in
- let eqa, eff =
- let eqa, effs = List.split (List.map aux a) in
- Array.of_list eqa,
- List.fold_left Evd.concat_side_effects eff (List.rev effs)
- in
+ let eq = match lookup_scheme (!beq_scheme_kind_aux()) ind' with
+ | Some c -> mkConst c
+ | None -> assert false
+ in
+ let eqa = Array.of_list @@ List.map aux a in
let args =
Array.append
(Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in
- if Int.equal (Array.length args) 0 then eq, eff
- else mkApp (eq, args), eff
+ if Int.equal (Array.length args) 0 then eq
+ else mkApp (eq, args)
with Not_found -> raise(EqNotFound (ind', fst ind))
end
| Sort _ -> raise InductiveWithSort
@@ -238,8 +282,7 @@ let build_beq_scheme mode kn =
let kneq = Constant.change_label kn eq_lbl in
if Environ.mem_constant kneq env then
let _ = Environ.constant_opt_value_in env (kneq, u) in
- Term.applist (mkConst kneq,a),
- Evd.empty_side_effects
+ Term.applist (mkConst kneq,a)
else raise (ParameterWithoutEquality (GlobRef.ConstRef kn)))
| Proj _ -> raise (EqUnknown "projection")
| Construct _ -> raise (EqUnknown "constructor")
@@ -271,7 +314,6 @@ let build_beq_scheme mode kn =
let constrsi = constrs (3+nparrec) in
let n = Array.length constrsi in
let ar = Array.make n (ff ()) in
- let eff = ref Evd.empty_side_effects in
for i=0 to n-1 do
let nb_cstr_args = List.length constrsi.(i).cs_args in
let ar2 = Array.make n (ff ()) in
@@ -283,13 +325,12 @@ let build_beq_scheme mode kn =
| _ -> let eqs = Array.make nb_cstr_args (tt ()) in
for ndx = 0 to nb_cstr_args-1 do
let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in
- let eqA, eff' = compute_A_equality rel_list
+ let eqA = compute_A_equality rel_list
nparrec
(nparrec+3+2*nb_cstr_args)
(nb_cstr_args+ndx+1)
cc
in
- eff := Evd.concat_side_effects eff' !eff;
Array.set eqs ndx
(mkApp (eqA,
[|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|]
@@ -315,21 +356,18 @@ let build_beq_scheme mode kn =
done;
mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1)) (
mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2)) (
- mkCase (ci, do_predicate rel_list 0,mkVar (Id.of_string "X"),ar))),
- !eff
+ mkCase (ci, do_predicate rel_list 0,mkVar (Id.of_string "X"),ar)))
in (* build_beq_scheme *)
let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
types = Array.make nb_ind mkSet and
cores = Array.make nb_ind mkSet in
- let eff = ref Evd.empty_side_effects in
let u = Univ.Instance.empty in
for i=0 to (nb_ind-1) do
names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant;
types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0) Sorts.Relevant
(mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ()));
- let c, eff' = make_one_eq i in
+ let c = make_one_eq i in
cores.(i) <- c;
- eff := Evd.concat_side_effects eff' !eff
done;
(Array.init nb_ind (fun i ->
let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in
@@ -347,10 +385,12 @@ let build_beq_scheme mode kn =
Vars.substl subst cores.(i)
in
create_input fix),
- UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())),
- !eff
+ UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()))
-let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme
+let beq_scheme_kind =
+ declare_mutual_scheme_object "_beq"
+ ~deps:build_beq_scheme_deps
+ build_beq_scheme
let _ = beq_scheme_kind_aux := fun () -> beq_scheme_kind
@@ -401,24 +441,9 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
let type_of_pq = Tacmach.New.pf_get_type_of gl p in
let sigma = Tacmach.New.project gl in
let env = Tacmach.New.pf_env gl in
- let u,v = destruct_ind env sigma type_of_pq
- in let lb_type_of_p =
- try
- let c, eff = find_scheme ~mode lb_scheme_key (fst u) (*FIXME*) in
- Proofview.tclUNIT (mkConst c, eff)
- with Not_found ->
- (* spiwack: the format of this error message should probably
- be improved. *)
- let err_msg =
- (str "Leibniz->boolean:" ++
- str "You have to declare the" ++
- str "decidability over " ++
- Printer.pr_econstr_env env sigma type_of_pq ++
- str " first.")
- in
- Tacticals.New.tclZEROMSG err_msg
- in
- lb_type_of_p >>= fun (lb_type_of_p,eff) ->
+ let u,v = destruct_ind env sigma type_of_pq in
+ find_scheme ~mode lb_scheme_key (fst u) (*FIXME*) >>= fun c ->
+ let lb_type_of_p = mkConst c in
Proofview.tclEVARMAP >>= fun sigma ->
let lb_args = Array.append (Array.append
v
@@ -428,7 +453,6 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
in
Tacticals.New.tclTHENLIST [
- Proofview.tclEFFECTS eff;
Equality.replace p q ; apply app ; Auto.default_auto]
end
@@ -474,22 +498,9 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
in if eq_ind (fst u) ind
then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ]
else (
- let bl_t1, eff =
- try
- let c, eff = find_scheme bl_scheme_key (fst u) (*FIXME*) in
- mkConst c, eff
- with Not_found ->
- (* spiwack: the format of this error message should probably
- be improved. *)
- let err_msg =
- (str "boolean->Leibniz:" ++
- str "You have to declare the" ++
- str "decidability over " ++
- Printer.pr_econstr_env env sigma tt1 ++
- str " first.")
- in
- user_err err_msg
- in let bl_args =
+ find_scheme bl_scheme_key (fst u) (*FIXME*) >>= fun c ->
+ let bl_t1 = mkConst c in
+ let bl_args =
Array.append (Array.append
v
(Array.Smart.map (fun x -> do_arg env sigma u x 1) v))
@@ -499,7 +510,6 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
then bl_t1 else mkApp (bl_t1,bl_args)
in
Tacticals.New.tclTHENLIST [
- Proofview.tclEFFECTS eff;
Equality.replace_by t1 t2
(Tacticals.New.tclTHEN (apply app) (Auto.default_auto)) ;
aux q1 q2 ]
@@ -552,11 +562,12 @@ let eqI ind l =
let list_id = list_id l in
let eA = Array.of_list((List.map (fun (s,_,_,_) -> mkVar s) list_id)@
(List.map (fun (_,seq,_,_)-> mkVar seq) list_id ))
- and e, eff =
- try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff
- with Not_found -> user_err ~hdr:"AutoIndDecl.eqI"
+ and e = match lookup_scheme beq_scheme_kind ind with
+ | Some c -> mkConst c
+ | None ->
+ user_err ~hdr:"AutoIndDecl.eqI"
(str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed.");
- in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)), eff
+ in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA))
(**********************************************************************)
(* Boolean->Leibniz *)
@@ -564,7 +575,7 @@ let eqI ind l =
open Namegen
let compute_bl_goal ind lnamesparrec nparrec =
- let eqI, eff = eqI ind lnamesparrec in
+ let eqI = eqI ind lnamesparrec in
let list_id = list_id lnamesparrec in
let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
let create_input c =
@@ -605,7 +616,7 @@ let compute_bl_goal ind lnamesparrec nparrec =
(mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar n;mkVar m|]);tt ()|]))
Sorts.Relevant
(mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
- ))), eff
+ )))
let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
@@ -695,16 +706,19 @@ let make_bl_scheme mode mind =
let nparrec = mib.mind_nparams_rec in
let lnonparrec,lnamesparrec = (* TODO subst *)
context_chop (nparams-nparrec) mib.mind_params_ctxt in
- let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
+ let bl_goal = compute_bl_goal ind lnamesparrec nparrec in
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), eff
+ ([|ans|], ctx)
-let bl_scheme_kind = declare_mutual_scheme_object "_dec_bl" make_bl_scheme
+let bl_scheme_kind =
+ declare_mutual_scheme_object "_dec_bl"
+ ~deps:(fun ind -> [SchemeMutualDep (ind, beq_scheme_kind)])
+ make_bl_scheme
let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
@@ -715,7 +729,7 @@ let compute_lb_goal ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
let eq = eq () and tt = tt () and bb = bb () in
let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
- let eqI, eff = eqI ind lnamesparrec in
+ let eqI = eqI ind lnamesparrec in
let create_input c =
let x = next_ident_away (Id.of_string "x") avoid and
y = next_ident_away (Id.of_string "y") avoid in
@@ -755,7 +769,7 @@ let compute_lb_goal ind lnamesparrec nparrec =
(mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar n;mkVar m|]))
Sorts.Relevant
(mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
- ))), eff
+ )))
let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
@@ -825,16 +839,19 @@ let make_lb_scheme mode mind =
let nparrec = mib.mind_nparams_rec in
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
- let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
+ let lb_goal = compute_lb_goal ind lnamesparrec nparrec in
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), eff
+ ([|ans|], ctx)
-let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme
+let lb_scheme_kind =
+ declare_mutual_scheme_object "_dec_lb"
+ ~deps:(fun ind -> [SchemeMutualDep (ind, beq_scheme_kind)])
+ make_lb_scheme
let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind
@@ -909,7 +926,8 @@ let compute_dec_tact ind lnamesparrec nparrec =
let eq = eq () and tt = tt ()
and ff = ff () and bb = bb () in
let list_id = list_id lnamesparrec in
- let eqI, eff = eqI ind lnamesparrec in
+ find_scheme beq_scheme_kind ind >>= fun _ ->
+ let eqI = eqI ind lnamesparrec in
let avoid = ref [] in
let eqtrue x = mkApp(eq,[|bb;x;tt|]) in
let eqfalse x = mkApp(eq,[|bb;x;ff|]) in
@@ -931,21 +949,11 @@ let compute_dec_tact ind lnamesparrec nparrec =
let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in
let arfresh = Array.of_list fresh_first_intros in
let xargs = Array.sub arfresh 0 (2*nparrec) in
- begin try
- let c, eff = find_scheme bl_scheme_kind ind in
- Proofview.tclUNIT (mkConst c,eff) with
- Not_found ->
- Tacticals.New.tclZEROMSG (str "Error during the decidability part, boolean to leibniz equality is required.")
- end >>= fun (blI,eff') ->
- begin try
- let c, eff = find_scheme lb_scheme_kind ind in
- Proofview.tclUNIT (mkConst c,eff) with
- Not_found ->
- Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.")
- end >>= fun (lbI,eff'') ->
- let eff = (Evd.concat_side_effects eff'' (Evd.concat_side_effects eff' eff)) in
+ find_scheme bl_scheme_kind ind >>= fun c ->
+ let blI = mkConst c in
+ find_scheme lb_scheme_kind ind >>= fun c ->
+ let lbI = mkConst c in
Tacticals.New.tclTHENLIST [
- Proofview.tclEFFECTS eff;
intros_using fresh_first_intros;
intros_using [freshn;freshm];
(*we do this so we don't have to prove the same goal twice *)
@@ -1006,11 +1014,11 @@ 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
- ([|ans|], ctx), Evd.empty_side_effects
+ ([|ans|], ctx)
let eq_dec_scheme_kind =
declare_mutual_scheme_object "_eq_dec" make_eq_decidability
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/declaremods.ml b/vernac/declaremods.ml
index 438509e28a..50fa6052f6 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -651,26 +651,28 @@ let mk_params_entry args =
let mk_funct_type env args seb0 =
List.fold_left
- (fun seb (arg_id,arg_t,arg_inl) ->
+ (fun (seb,cst) (arg_id,arg_t,arg_inl) ->
let mp = MPbound arg_id in
- let arg_t = Mod_typing.translate_modtype env mp arg_inl ([],arg_t) in
- MoreFunctor(arg_id,arg_t,seb))
+ let arg_t, cst' = Mod_typing.translate_modtype env mp arg_inl ([],arg_t) in
+ MoreFunctor(arg_id,arg_t,seb), Univ.Constraint.union cst cst')
seb0 args
(** Prepare the module type list for check of subtypes *)
let build_subtypes env mp args mtys =
- let (cst, ans) = List.fold_left_map
- (fun cst (m,ann) ->
+ let (ctx, ans) = List.fold_left_map
+ (fun ctx (m,ann) ->
let inl = inl2intopt ann in
- let mte, _, cst' = Modintern.interp_module_ast env Modintern.ModType m in
- let env = Environ.push_context_set ~strict:true cst' env in
- let cst = Univ.ContextSet.union cst cst' in
- let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in
- cst, { mtb with mod_type = mk_funct_type env args mtb.mod_type })
+ let mte, _, ctx' = Modintern.interp_module_ast env Modintern.ModType m in
+ let env = Environ.push_context_set ~strict:true ctx' env in
+ let ctx = Univ.ContextSet.union ctx ctx' in
+ let mtb, cst = Mod_typing.translate_modtype env mp inl ([],mte) in
+ let mod_type, cst = mk_funct_type env args (mtb.mod_type,cst) in
+ let ctx = Univ.ContextSet.add_constraints cst ctx in
+ ctx, { mtb with mod_type })
Univ.ContextSet.empty mtys
in
- (ans, cst)
+ (ans, ctx)
(** {6 Current module information}
@@ -703,23 +705,23 @@ module RawModOps = struct
let start_module export id args res fs =
let mp = Global.start_module id in
- let arg_entries_r, cst = intern_args args in
- let () = Global.push_context_set ~strict:true cst in
+ let arg_entries_r, ctx = intern_args args in
+ let () = Global.push_context_set ~strict:true ctx in
let env = Global.env () in
- let res_entry_o, subtyps, cst = match res with
+ let res_entry_o, subtyps, ctx = match res with
| Enforce (res,ann) ->
let inl = inl2intopt ann in
- let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType res in
- let env = Environ.push_context_set ~strict:true cst env in
+ let (mte, _, ctx) = Modintern.interp_module_ast env Modintern.ModType res in
+ let env = Environ.push_context_set ~strict:true ctx env in
(* We check immediately that mte is well-formed *)
- let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in
- let cst = Univ.ContextSet.union cst cst' in
- Some (mte, inl), [], cst
+ let _, _, _, cst = Mod_typing.translate_mse env None inl mte in
+ let ctx = Univ.ContextSet.add_constraints cst ctx in
+ Some (mte, inl), [], ctx
| Check resl ->
- let typs, cst = build_subtypes env mp arg_entries_r resl in
- None, typs, cst
+ let typs, ctx = build_subtypes env mp arg_entries_r resl in
+ None, typs, ctx
in
- let () = Global.push_context_set ~strict:true cst in
+ let () = Global.push_context_set ~strict:true ctx in
openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
let prefix = Lib.start_module export id mp fs in
Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix));
@@ -763,37 +765,38 @@ let end_module () =
mp
+(* TODO cleanup push universes directly to global env *)
let declare_module id args res mexpr_o fs =
(* We simulate the beginning of an interactive module,
then we adds the module parameters to the global env. *)
let mp = Global.start_module id in
- let arg_entries_r, cst = intern_args args in
+ let arg_entries_r, ctx = intern_args args in
let params = mk_params_entry arg_entries_r in
let env = Global.env () in
- let env = Environ.push_context_set ~strict:true cst env in
- let mty_entry_o, subs, inl_res, cst' = match res with
+ let env = Environ.push_context_set ~strict:true ctx env in
+ let mty_entry_o, subs, inl_res, ctx' = match res with
| Enforce (mty,ann) ->
let inl = inl2intopt ann in
- let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType mty in
- let env = Environ.push_context_set ~strict:true cst env in
+ let (mte, _, ctx) = Modintern.interp_module_ast env Modintern.ModType mty in
+ let env = Environ.push_context_set ~strict:true ctx env in
(* We check immediately that mte is well-formed *)
- let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in
- let cst = Univ.ContextSet.union cst cst' in
- Some mte, [], inl, cst
+ let _, _, _, cst = Mod_typing.translate_mse env None inl mte in
+ let ctx = Univ.ContextSet.add_constraints cst ctx in
+ Some mte, [], inl, ctx
| Check mtys ->
- let typs, cst = build_subtypes env mp arg_entries_r mtys in
- None, typs, default_inline (), cst
+ let typs, ctx = build_subtypes env mp arg_entries_r mtys in
+ None, typs, default_inline (), ctx
in
- let env = Environ.push_context_set ~strict:true cst' env in
- let cst = Univ.ContextSet.union cst cst' in
- let mexpr_entry_o, inl_expr, cst' = match mexpr_o with
+ let env = Environ.push_context_set ~strict:true ctx' env in
+ let ctx = Univ.ContextSet.union ctx ctx' in
+ let mexpr_entry_o, inl_expr, ctx' = match mexpr_o with
| None -> None, default_inline (), Univ.ContextSet.empty
| Some (mexpr,ann) ->
- let (mte, _, cst) = Modintern.interp_module_ast env Modintern.Module mexpr in
- Some mte, inl2intopt ann, cst
+ let (mte, _, ctx) = Modintern.interp_module_ast env Modintern.Module mexpr in
+ Some mte, inl2intopt ann, ctx
in
- let env = Environ.push_context_set ~strict:true cst' env in
- let cst = Univ.ContextSet.union cst cst' in
+ let env = Environ.push_context_set ~strict:true ctx' env in
+ let ctx = Univ.ContextSet.union ctx ctx' in
let entry = match mexpr_entry_o, mty_entry_o with
| None, None -> assert false (* No body, no type ... *)
| None, Some typ -> MType (params, typ)
@@ -812,7 +815,7 @@ let declare_module id args res mexpr_o fs =
| None -> None
| _ -> inl_res
in
- let () = Global.push_context_set ~strict:true cst in
+ let () = Global.push_context_set ~strict:true ctx in
let mp_env,resolver = Global.add_module id entry inl in
(* Name consistency check : kernel vs. library *)
@@ -864,20 +867,20 @@ let declare_modtype id args mtys (mty,ann) fs =
(* We simulate the beginning of an interactive module,
then we adds the module parameters to the global env. *)
let mp = Global.start_modtype id in
- let arg_entries_r, cst = intern_args args in
- let () = Global.push_context_set ~strict:true cst in
+ let arg_entries_r, ctx = intern_args args in
+ let () = Global.push_context_set ~strict:true ctx in
let params = mk_params_entry arg_entries_r in
let env = Global.env () in
- let mte, _, cst = Modintern.interp_module_ast env Modintern.ModType mty in
- let () = Global.push_context_set ~strict:true cst in
+ let mte, _, ctx = Modintern.interp_module_ast env Modintern.ModType mty in
+ let () = Global.push_context_set ~strict:true ctx in
let env = Global.env () in
(* We check immediately that mte is well-formed *)
let _, _, _, cst = Mod_typing.translate_mse env None inl mte in
- let () = Global.push_context_set ~strict:true cst in
+ let () = Global.push_context_set ~strict:true (Univ.LSet.empty,cst) in
let env = Global.env () in
let entry = params, mte in
- let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in
- let () = Global.push_context_set ~strict:true cst in
+ let sub_mty_l, ctx = build_subtypes env mp arg_entries_r mtys in
+ let () = Global.push_context_set ~strict:true ctx in
let env = Global.env () in
let sobjs = get_functor_sobjs false env inl entry in
let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in
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/himsg.ml b/vernac/himsg.ml
index fddc84b398..41f2ab9c63 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -729,9 +729,9 @@ let explain_undeclared_universe env sigma l =
spc () ++ str "(maybe a bugged tactic)."
let explain_disallowed_sprop () =
- Pp.(strbrk "SProp not allowed, you need to "
- ++ str "Set Allow StrictProp"
- ++ strbrk " or to use the -allow-sprop command-line-flag.")
+ Pp.(strbrk "SProp is disallowed because the "
+ ++ str "\"Allow StrictProp\""
+ ++ strbrk " flag is off.")
let explain_bad_relevance env =
strbrk "Bad relevance (maybe a bugged tactic)."
diff --git a/vernac/library.ml b/vernac/library.ml
index 01f5101764..85db501e84 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -20,11 +20,11 @@ open Libobject
(*s Low-level interning/externing of libraries to files *)
let raw_extern_library f =
- System.raw_extern_state Coq_config.vo_magic_number f
+ ObjFile.open_out ~file:f
let raw_intern_library f =
System.with_magic_number_check
- (System.raw_intern_state Coq_config.vo_magic_number) f
+ (fun file -> ObjFile.open_in ~file) f
(************************************************************************)
(** Serialized objects loaded on-the-fly *)
@@ -35,7 +35,7 @@ module Delayed :
sig
type 'a delayed
-val in_delayed : string -> in_channel -> 'a delayed * Digest.t
+val in_delayed : string -> ObjFile.in_handle -> segment:string -> 'a delayed * Digest.t
val fetch_delayed : 'a delayed -> 'a
end =
@@ -43,28 +43,32 @@ struct
type 'a delayed = {
del_file : string;
- del_off : int;
+ del_off : int64;
del_digest : Digest.t;
}
-let in_delayed f ch =
- let pos = pos_in ch in
- let _, digest = System.skip_in_segment f ch in
- ({ del_file = f; del_digest = digest; del_off = pos; }, digest)
+let in_delayed f ch ~segment =
+ let seg = ObjFile.get_segment ch ~segment in
+ let digest = seg.ObjFile.hash in
+ { del_file = f; del_digest = digest; del_off = seg.ObjFile.pos; }, digest
(** Fetching a table of opaque terms at position [pos] in file [f],
expecting to find first a copy of [digest]. *)
let fetch_delayed del =
let { del_digest = digest; del_file = f; del_off = pos; } = del in
- try
- let ch = raw_intern_library f in
- let () = seek_in ch pos in
- let obj, _, digest' = System.marshal_in_segment f ch in
- let () = close_in ch in
- if not (String.equal digest digest') then raise (Faulty f);
- obj
- with e when CErrors.noncritical e -> raise (Faulty f)
+ let ch = open_in_bin f in
+ let obj, digest' =
+ try
+ let () = LargeFile.seek_in ch pos in
+ let obj = System.marshal_in f ch in
+ let digest' = Digest.input ch in
+ obj, digest'
+ with e -> close_in ch; raise e
+ in
+ close_in ch;
+ if not (String.equal digest digest') then raise (Faulty f);
+ obj
end
@@ -92,7 +96,7 @@ type summary_disk = {
type library_t = {
library_name : compilation_unit_name;
- library_data : library_disk delayed;
+ library_data : library_disk;
library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
library_digests : Safe_typing.vodigest;
library_extra_univs : Univ.ContextSet.t;
@@ -200,7 +204,7 @@ let access_table what tables dp i =
with Faulty f ->
user_err ~hdr:"Library.access_table"
(str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
- str ") is inaccessible or corrupted,\ncannot load some " ++
+ str ") is corrupted,\ncannot load some " ++
str what ++ str " in it.\n")
in
tables := DPmap.add dp (Fetched t) !tables;
@@ -242,12 +246,11 @@ let mk_summary m = {
let intern_from_file f =
let ch = raw_intern_library f in
- let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in
- let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in
- let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
- let _ = System.skip_in_segment f ch in
- let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in
- close_in ch;
+ let (lsd : seg_sum), digest_lsd = ObjFile.marshal_in_segment ch ~segment:"summary" in
+ let ((lmd : seg_lib), digest_lmd) = ObjFile.marshal_in_segment ch ~segment:"library" in
+ let (univs : seg_univ option), digest_u = ObjFile.marshal_in_segment ch ~segment:"universes" in
+ let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in
+ ObjFile.close_in ch;
register_library_filename lsd.md_name f;
add_opaque_table lsd.md_name (ToFetch del_opaque);
let open Safe_typing in
@@ -297,7 +300,7 @@ let rec_intern_library ~lib_resolver libs (dir, f) =
let native_name_from_filename f =
let ch = raw_intern_library f in
- let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in
+ let (lmd : seg_sum), digest_lmd = ObjFile.marshal_in_segment ch ~segment:"summary" in
Nativecode.mod_uid_of_dirpath lmd.md_name
(**********************************************************************)
@@ -318,7 +321,7 @@ let native_name_from_filename f =
*)
let register_library m =
- let l = fetch_delayed m.library_data in
+ let l = m.library_data in
Declaremods.register_library
m.library_name
l.md_compiled
@@ -392,12 +395,12 @@ let require_library_from_dirpath ~lib_resolver modrefl export =
let load_library_todo f =
let ch = raw_intern_library f in
- let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
- let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
- let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
- let tasks, _, _ = System.marshal_in_segment f ch in
- let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in
- close_in ch;
+ let (s0 : seg_sum), _ = ObjFile.marshal_in_segment ch ~segment:"summary" in
+ let (s1 : seg_lib), _ = ObjFile.marshal_in_segment ch ~segment:"library" in
+ let (s2 : seg_univ option), _ = ObjFile.marshal_in_segment ch ~segment:"universes" in
+ let tasks, _ = ObjFile.marshal_in_segment ch ~segment:"tasks" in
+ let (s4 : seg_proofs), _ = ObjFile.marshal_in_segment ch ~segment:"opaques" in
+ ObjFile.close_in ch;
if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
@@ -433,15 +436,15 @@ let error_recursively_dependent_library dir =
let save_library_base f sum lib univs tasks proofs =
let ch = raw_extern_library f in
try
- System.marshal_out_segment f ch (sum : seg_sum);
- System.marshal_out_segment f ch (lib : seg_lib);
- System.marshal_out_segment f ch (univs : seg_univ option);
- System.marshal_out_segment f ch (tasks : 'tasks option);
- System.marshal_out_segment f ch (proofs : seg_proofs);
- close_out ch
+ ObjFile.marshal_out_segment ch ~segment:"summary" (sum : seg_sum);
+ ObjFile.marshal_out_segment ch ~segment:"library" (lib : seg_lib);
+ ObjFile.marshal_out_segment ch ~segment:"universes" (univs : seg_univ option);
+ ObjFile.marshal_out_segment ch ~segment:"tasks" (tasks : 'tasks option);
+ ObjFile.marshal_out_segment ch ~segment:"opaques" (proofs : seg_proofs);
+ ObjFile.close_out ch
with reraise ->
let reraise = Exninfo.capture reraise in
- close_out ch;
+ ObjFile.close_out ch;
Feedback.msg_warning (str "Removed file " ++ str f);
Sys.remove f;
Exninfo.iraise reraise
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-04-29 11:14:34 +0000