aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml4
-rw-r--r--vernac/auto_ind_decl.ml46
-rw-r--r--vernac/classes.ml3
-rw-r--r--vernac/command.ml74
-rw-r--r--vernac/discharge.ml2
-rw-r--r--vernac/explainErr.ml2
-rw-r--r--vernac/himsg.ml6
-rw-r--r--vernac/indschemes.ml30
-rw-r--r--vernac/indschemes.mli2
-rw-r--r--vernac/lemmas.ml4
-rw-r--r--vernac/metasyntax.ml6
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/record.ml86
-rw-r--r--vernac/vernacentries.ml39
14 files changed, 149 insertions, 161 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index bf274901bd..726115653b 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -131,7 +131,7 @@ let lookup_constant_in_impl cst fallback =
- The label has not been found in the structure. This is an error *)
match fallback with
| Some cb -> cb
- | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst)
+ | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst ++ str ".")
let lookup_constant cst =
try
@@ -146,7 +146,7 @@ let lookup_mind_in_impl mind =
let fields = memoize_fields_of_mp mp in
search_mind_label lab fields
with Not_found ->
- anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind)
+ anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind ++ str ".")
let lookup_mind mind =
try Global.lookup_mind mind
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index cf534f13a2..9e6e5e313b 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -365,7 +365,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
)))
)
in
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in
let sigma = Tacmach.New.project gl in
let u,v = destruct_ind sigma type_of_pq
@@ -397,7 +397,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
Tacticals.New.tclTHENLIST [
Proofview.tclEFFECTS eff;
Equality.replace p q ; apply app ; Auto.default_auto]
- end }
+ end
(* used in the bool -> leib side *)
let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
@@ -430,7 +430,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let rec aux l1 l2 =
match (l1,l2) with
| (t1::q1,t2::q2) ->
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
let sigma = Tacmach.New.project gl in
if EConstr.eq_constr sigma t1 t2 then aux q1 q2
@@ -472,7 +472,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
aux q1 q2 ]
)
)
- end }
+ end
| ([],[]) -> Proofview.tclUNIT ()
| _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.")
in
@@ -533,7 +533,7 @@ open Namegen
let compute_bl_goal ind lnamesparrec nparrec =
let eqI, eff = eqI ind lnamesparrec in
let list_id = list_id lnamesparrec in
- let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+ let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name 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
@@ -581,7 +581,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
in
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -604,18 +604,18 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
Tacticals.New.tclREPEAT (
Tacticals.New.tclTHENLIST [
Simple.apply_in freshz (EConstr.of_constr (andb_prop()));
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let fresht = fresh_id (Id.of_string "Z") gl in
destruct_on_as (EConstr.mkVar freshz)
(IntroOrPattern [[Loc.tag @@ IntroNaming (IntroIdentifier fresht);
Loc.tag @@ IntroNaming (IntroIdentifier freshz)]])
- end }
+ end
]);
(*
Ci a1 ... an = Ci b1 ... bn
replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto
*)
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
match EConstr.kind sigma concl with
@@ -635,10 +635,10 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
| _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.")
)
| _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
- end }
+ end
]
- end }
+ end
let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
@@ -676,7 +676,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
let compute_lb_goal ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
- let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+ let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
let eqI, eff = eqI ind lnamesparrec in
let create_input c =
let x = next_ident_away (Id.of_string "x") avoid and
@@ -725,7 +725,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
in
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -748,7 +748,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro()));
simplest_split ;Auto.default_auto ]
);
- Proofview.Goal.enter { enter = begin fun gls ->
+ Proofview.Goal.enter begin fun gls ->
let concl = Proofview.Goal.concl gls in
let sigma = Tacmach.New.project gl in
(* assume the goal to be eq (eq_type ...) = true *)
@@ -765,9 +765,9 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
)
| _ ->
Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
- end }
+ end
]
- end }
+ end
let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
@@ -806,7 +806,7 @@ let compute_dec_goal ind lnamesparrec nparrec =
check_not_is_defined ();
let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
let list_id = list_id lnamesparrec in
- let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+ let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name 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
@@ -873,7 +873,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
in
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -904,7 +904,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
))
(Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto);
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let freshH2 = fresh_id (Id.of_string "H") gl in
Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [
(* left *)
@@ -916,7 +916,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
;
(*right *)
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let freshH3 = fresh_id (Id.of_string "H") gl in
Tacticals.New.tclTHENLIST [
simplest_right ;
@@ -938,11 +938,11 @@ let compute_dec_tact ind lnamesparrec nparrec =
true;
Equality.discr_tac false None
]
- end }
+ end
]
- end }
+ end
]
- end }
+ end
let make_eq_decidability mode mind =
let mib = Global.lookup_mind mind in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 004083dcf9..dc5ce1a537 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -20,7 +20,6 @@ open Libnames
open Globnames
open Constrintern
open Constrexpr
-open Sigma.Notations
open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
@@ -342,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
if not (Option.is_empty term) then
let init_refine =
Tacticals.New.tclTHENLIST [
- Refine.refine { run = fun evm -> Sigma (EConstr.of_constr (Option.get term), evm, Sigma.refl) };
+ Refine.refine (fun evm -> (evm,EConstr.of_constr (Option.get term)));
Proofview.Unsafe.tclNEWGOALS gls;
Tactics.New.reduce_after_refine;
]
diff --git a/vernac/command.ml b/vernac/command.ml
index e2ebb4d7fb..b1425d7034 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -35,7 +35,6 @@ open Evarconv
open Indschemes
open Misctypes
open Vernacexpr
-open Sigma.Notations
open Context.Rel.Declaration
open Entries
@@ -78,8 +77,7 @@ let red_constant_entry n ce sigma = function
let env = Global.env () in
let (redfun, _) = reduction_of_red_expr env red in
let redfun env sigma c =
- let sigma = Sigma.Unsafe.of_evar_map sigma in
- let Sigma (c, _, _) = redfun.e_redfun env sigma c in
+ let (_, c) = redfun env sigma c in
EConstr.Unsafe.to_constr c
in
{ ce with const_entry_body = Future.chain ~pure:true proof_out
@@ -211,7 +209,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
assert(Univ.ContextSet.is_empty ctx);
let typ = match ce.const_entry_type with
| Some t -> t
- | None -> EConstr.Unsafe.to_constr (Retyping.get_type_of env evd (EConstr.of_constr c))
+ | None -> EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr c))
in
Obligations.check_evars env evd;
let obls, _, c, cty =
@@ -411,8 +409,8 @@ let mk_mltype_data evdref env assums arity indname =
(is_ml_type,indname,assums)
let prepare_param = function
- | LocalAssum (na,t) -> out_name na, LocalAssumEntry t
- | LocalDef (na,b,_) -> out_name na, LocalDefEntry b
+ | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t
+ | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b
(** Make the arity conclusion flexible to avoid generating an upper bound universe now,
only if the universe does not appear anywhere else.
@@ -582,7 +580,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
let pl = (List.hd indl).ind_univs in
let ctx = Evd.make_evar_universe_context env0 pl in
let evdref = ref Evd.(from_ctx ctx) in
- let _, ((env_params, ctx_params), userimpls) =
+ let impls, ((env_params, ctx_params), userimpls) =
interp_context_evars env0 evdref paramsl
in
let ctx_params = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx_params in
@@ -590,7 +588,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
(* Names of parameters as arguments of the inductive type (defs removed) *)
let assums = List.filter is_local_assum ctx_params in
- let params = List.map (RelDecl.get_name %> out_name) assums in
+ let params = List.map (RelDecl.get_name %> Name.get_id) assums in
(* Interpret the arities *)
let arities = List.map (interp_ind_arity env_params evdref) indl in
@@ -603,7 +601,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
let indimpls = List.map (fun (_, _, impls) -> userimpls @
lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
- let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
+ let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in
let implsforntn = compute_internalization_env env0 Variable indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
@@ -674,7 +672,7 @@ let extract_coercions indl =
let extract_params indl =
let paramsl = List.map (fun (_,params,_,_) -> params) indl in
match paramsl with
- | [] -> anomaly (Pp.str "empty list of inductive types")
+ | [] -> anomaly (Pp.str "empty list of inductive types.")
| params::paramsl ->
if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str
"Parameters should be syntactically the same for each inductive type.");
@@ -907,23 +905,25 @@ let fixsub_module = subtac_dir @ ["Wf"]
let tactics_module = subtac_dir @ ["Tactics"]
let init_reference dir s () = Coqlib.coq_reference "Command" dir s
-let init_constant dir s () = EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "Command" dir s)
+let init_constant dir s evdref =
+ let (sigma, c) = Evarutil.new_global !evdref (Coqlib.coq_reference "Command" dir s)
+ in evdref := sigma; c
let make_ref l s = init_reference l s
let fix_proto = init_constant tactics_module "fix_proto"
let fix_sub_ref = make_ref fixsub_module "Fix_sub"
let measure_on_R_ref = make_ref fixsub_module "MR"
let well_founded = init_constant ["Init"; "Wf"] "well_founded"
-let mkSubset name typ prop =
+let mkSubset evdref name typ prop =
let open EConstr in
- mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).typ),
+ mkApp (Evarutil.e_new_global evdref (delayed_force build_sigma).typ,
[| typ; mkLambda (name, typ, prop) |])
let sigT = Lazy.from_fun build_sigma_type
let make_qref s = Qualid (Loc.tag @@ qualid_of_string s)
let lt_ref = make_qref "Init.Peano.lt"
-let rec telescope l =
+let rec telescope evdref l =
let open EConstr in
let open Vars in
match l with
@@ -935,10 +935,8 @@ let rec telescope l =
(fun (ty, tys, (k, constr)) decl ->
let t = RelDecl.get_type decl in
let pred = mkLambda (RelDecl.get_name decl, t, ty) in
- let ty = Universes.constr_of_global (Lazy.force sigT).typ in
- let ty = EConstr.of_constr ty in
- let intro = Universes.constr_of_global (Lazy.force sigT).intro in
- let intro = EConstr.of_constr intro in
+ let ty = Evarutil.e_new_global evdref (Lazy.force sigT).typ in
+ let intro = Evarutil.e_new_global evdref (Lazy.force sigT).intro in
let sigty = mkApp (ty, [|t; pred|]) in
let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in
(sigty, pred :: tys, (succ k, intro)))
@@ -947,17 +945,15 @@ let rec telescope l =
let (last, subst) = List.fold_right2
(fun pred decl (prev, subst) ->
let t = RelDecl.get_type decl in
- let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in
- let p1 = EConstr.of_constr p1 in
- let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in
- let p2 = EConstr.of_constr p2 in
+ let p1 = Evarutil.e_new_global evdref (Lazy.force sigT).proj1 in
+ let p2 = Evarutil.e_new_global evdref (Lazy.force sigT).proj2 in
let proj1 = applist (p1, [t; pred; prev]) in
let proj2 = applist (p2, [t; pred; prev]) in
(lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
(List.rev tys) tl (mkRel 1, [])
in ty, (LocalDef (n, last, t) :: subst), constr
- | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope tl in
+ | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope evdref tl in
ty, (LocalDef (n, b, t) :: subst), lift 1 term
let nf_evar_context sigma ctx =
@@ -976,7 +972,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let top_env = push_rel_context binders_rel env in
let top_arity = interp_type_evars top_env evdref arityc in
let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
- let argtyp, letbinders, make = telescope binders_rel in
+ let argtyp, letbinders, make = telescope evdref binders_rel in
let argname = Id.of_string "recarg" in
let arg = LocalAssum (Name argname, argtyp) in
let binders = letbinders @ [arg] in
@@ -1004,7 +1000,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
it_mkLambda_or_LetIn measure letbinders,
it_mkLambda_or_LetIn measure binders
in
- let comb = EConstr.of_constr (Universes.constr_of_global (delayed_force measure_on_R_ref)) in
+ let comb = Evarutil.e_new_global evdref (delayed_force measure_on_R_ref) in
let relargty = EConstr.of_constr relargty in
let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
let wf_rel_fun x y =
@@ -1012,15 +1008,15 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
subst1 y measure_body |])
in wf_rel, wf_rel_fun, measure
in
- let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in
+ let wf_proof = mkApp (well_founded evdref, [| argtyp ; wf_rel |]) in
let argid' = Id.of_string (Id.to_string argname ^ "'") in
let wfarg len = LocalAssum (Name argid',
- mkSubset (Name argid') argtyp
+ mkSubset evdref (Name argid') argtyp
(wf_rel_fun (mkRel 1) (mkRel (len + 1))))
in
let intern_bl = wfarg 1 :: [arg] in
let _intern_env = push_rel_context intern_bl env in
- let proj = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.proj1) in
+ let proj = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.proj1 in
let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
let projection = (* in wfarg :: arg :: before *)
mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
@@ -1033,7 +1029,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in
let curry_fun =
let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
- let intro = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro) in
+ let intro = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.intro in
let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
let rcurry = mkApp (rel, [| measure; lift len measure |]) in
@@ -1059,10 +1055,10 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
let prop = mkLambda (Name argname, argtyp, top_arity_let) in
let def =
- mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)),
+ mkApp (Evarutil.e_new_global evdref (delayed_force fix_sub_ref),
[| argtyp ; wf_rel ;
Evarutil.e_new_evar env evdref
- ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
+ ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof;
prop |])
in
let def = Typing.e_solve_evars env evdref def in
@@ -1075,12 +1071,12 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
if List.length binders_rel > 1 then
let name = add_suffix recname "_func" in
let hook l gr _ =
- let body = it_mkLambda_or_LetIn (mkApp (EConstr.of_constr (Universes.constr_of_global gr), [|make|])) binders_rel in
+ let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in
let ty = it_mkProd_or_LetIn top_arity binders_rel in
let ty = EConstr.Unsafe.to_constr ty in
let pl, univs = Evd.universe_context ?names:pl !evdref in
(*FIXME poly? *)
- let ce = definition_entry ~poly ~types:ty ~univs (EConstr.Unsafe.to_constr (Evarutil.nf_evar !evdref body)) in
+ let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
(** FIXME: include locality *)
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
@@ -1097,10 +1093,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
in hook, recname, typ
in
let hook = Lemmas.mk_hook hook in
- let fullcoqc = Evarutil.nf_evar !evdref def in
- let fullctyp = Evarutil.nf_evar !evdref typ in
- let fullcoqc = EConstr.Unsafe.to_constr fullcoqc in
- let fullctyp = EConstr.Unsafe.to_constr fullctyp in
+ let fullcoqc = EConstr.to_constr !evdref def in
+ let fullctyp = EConstr.to_constr !evdref typ in
Obligations.check_evars env !evdref;
let evars, _, evars_def, evars_typ =
Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp
@@ -1143,7 +1137,7 @@ let interp_recursive isfix fixl notations =
let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in
let fixprot =
try
- let app = mkApp (delayed_force fix_proto, [|sort; t|]) in
+ let app = mkApp (fix_proto evdref, [|sort; t|]) in
Typing.e_solve_evars env evdref app
with e when CErrors.noncritical e -> t
in
@@ -1303,9 +1297,9 @@ let do_program_recursive local p fixkind fixl ntns =
let collect_evars id def typ imps =
(* Generalize by the recursive prototypes *)
let def =
- EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign))
+ EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
and typ =
- EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign))
+ EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
in
let evm = collect_evars_of_term evd def typ in
let evars, _, def, typ =
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index b898f3e830..65ade78876 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -23,7 +23,7 @@ let detype_param =
function
| LocalAssum (Name id, p) -> id, LocalAssumEntry p
| LocalDef (Name id, p,_) -> id, LocalDefEntry p
- | _ -> anomaly (Pp.str "Unnamed inductive local variable")
+ | _ -> anomaly (Pp.str "Unnamed inductive local variable.")
(* Replace
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 040c86805e..021fde961e 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -109,7 +109,7 @@ let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) =
let () =
if not allow_uncaught && not (CErrors.handled (fst e)) then
let (e, info) = e in
- let msg = str "Uncaught exception " ++ str (Printexc.to_string e) in
+ let msg = str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." in
let err = CErrors.make_anomaly msg in
Util.iraise (err, info)
in
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 17bb87f2aa..6d8dd82ac6 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -682,12 +682,12 @@ let explain_wrong_abstraction_type env sigma na abs expected result =
let explain_abstraction_over_meta _ m n =
strbrk "Too complex unification problem: cannot find a solution for both " ++
- pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "."
+ Name.print m ++ spc () ++ str "and " ++ Name.print n ++ str "."
let explain_non_linear_unification env sigma m t =
let t = EConstr.to_constr sigma t in
strbrk "Cannot unambiguously instantiate " ++
- pr_name m ++ str ":" ++
+ Name.print m ++ str ":" ++
strbrk " which would require to abstract twice on " ++
pr_lconstr_env env sigma t ++ str "."
@@ -1055,7 +1055,7 @@ let explain_refiner_bad_type arg ty conclty =
let explain_refiner_unresolved_bindings l =
str "Unable to find an instance for the " ++
str (String.plural (List.length l) "variable") ++ spc () ++
- prlist_with_sep pr_comma pr_name l ++ str"."
+ prlist_with_sep pr_comma Name.print l ++ str"."
let explain_refiner_cannot_apply t harg =
str "In refiner, a term of type" ++ brk(1,1) ++
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index f57b1bba01..c2c27eb78e 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -453,11 +453,14 @@ let fold_left' f = function
[] -> invalid_arg "fold_left'"
| hd :: tl -> List.fold_left f hd tl
+let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.build_coq_and ())
+let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.build_coq_conj ())
+
let build_combined_scheme env schemes =
- let defs = List.map (fun cst -> (* FIXME *)
- let evd, c = Evd.fresh_constant_instance env (Evd.from_env env) cst in
- (c, Typeops.type_of_constant_in env c)) schemes in
-(* let nschemes = List.length schemes in *)
+ let evdref = ref (Evd.from_env env) in
+ let defs = List.map (fun cst ->
+ let evd, c = Evd.fresh_constant_instance env !evdref cst in
+ evdref := evd; (c, Typeops.type_of_constant_in env c)) schemes in
let find_inductive ty =
let (ctx, arity) = decompose_prod ty in
let (_, last) = List.hd ctx in
@@ -471,26 +474,27 @@ let build_combined_scheme env schemes =
let (c, t) = List.hd defs in
let ctx, ind, nargs = find_inductive t in
(* Number of clauses, including the predicates quantification *)
- let prods = nb_prod Evd.empty (EConstr.of_constr t) - (nargs + 1) (** FIXME *) in
- let coqand = Universes.constr_of_global @@ Coqlib.build_coq_and () in
- let coqconj = Universes.constr_of_global @@ Coqlib.build_coq_conj () in
+ let prods = nb_prod !evdref (EConstr.of_constr t) - (nargs + 1) in
+ let sigma, coqand = mk_coq_and !evdref in
+ let sigma, coqconj = mk_coq_conj sigma in
+ let () = evdref := sigma in
let relargs = rel_vect 0 prods in
let concls = List.rev_map
- (fun (cst, t) -> (* FIXME *)
+ (fun (cst, t) ->
mkApp(mkConstU cst, relargs),
snd (decompose_prod_n prods t)) defs in
let concl_bod, concl_typ =
fold_left'
(fun (accb, acct) (cst, x) ->
- mkApp (coqconj, [| x; acct; cst; accb |]),
- mkApp (coqand, [| x; acct |])) concls
+ mkApp (EConstr.to_constr !evdref coqconj, [| x; acct; cst; accb |]),
+ mkApp (EConstr.to_constr !evdref coqand, [| x; acct |])) concls
in
let ctx, _ =
list_split_rev_at prods
(List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in
let typ = List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) concl_typ ctx in
let body = it_mkLambda_or_LetIn concl_bod ctx in
- (body, typ)
+ (!evdref, body, typ)
let do_combined_scheme name schemes =
let csts =
@@ -501,9 +505,9 @@ let do_combined_scheme name schemes =
with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared."))
schemes
in
- let body,typ = build_combined_scheme (Global.env ()) csts in
+ let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
- ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ));
+ ignore (define (snd name) UserIndividualRequest sigma proof_output (Some typ));
fixpoint_message None [snd name]
(**********************************************************************)
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index e5d79fd514..0f559d2bd8 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -40,7 +40,7 @@ val do_scheme : (Id.t located option * scheme) list -> unit
(** Combine a list of schemes into a conjunction of them *)
-val build_combined_scheme : env -> constant list -> constr * types
+val build_combined_scheme : env -> constant list -> Evd.evar_map * constr * types
val do_combined_scheme : Id.t located -> Id.t located list -> unit
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d6ae0ea86f..77e356eb2c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -242,7 +242,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
| LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2)
| Lambda(na,ty,t) -> mkLambda(na,ty,body_i t)
| App (t, args) -> mkApp (body_i t, args)
- | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in
+ | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body ++ str ".") in
let body_i = body_i body in
match locality with
| Discharge ->
@@ -402,7 +402,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
let () = match thms with [_] -> () | _ -> assert false in
(if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
match thms with
- | [] -> anomaly (Pp.str "No proof to start")
+ | [] -> anomaly (Pp.str "No proof to start.")
| ((id,pl),(t,(_,imps)))::other_thms ->
let hook ctx strength ref =
let ctx = match ctx with
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 42494dd28a..34b9b97d8c 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -250,7 +250,7 @@ let rec find_pattern nt xl = function
| _, [] ->
user_err Pp.(str msg_expected_form_of_recursive_notation)
| ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
- anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right")
+ anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right.")
let rec interp_list_parser hd = function
| [] -> [], List.rev hd
@@ -271,7 +271,7 @@ let rec interp_list_parser hd = function
| NonTerminal _ as x :: tl ->
let xyl,tl' = interp_list_parser [x] tl in
xyl, List.rev_append hd tl'
- | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser")
+ | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser.")
(* Find non-terminal tokens of notation *)
@@ -645,7 +645,7 @@ let make_production etyps symbols =
let tkl = List.flatten
(List.map (function Terminal s -> [CLexer.terminal s]
| Break _ -> []
- | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator")) sl) in
+ | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in
match List.assoc x etyps with
| ETConstr typ -> expand_list_rule typ tkl x 1 0 [] ll
| ETBinder o ->
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index be58c67a9e..6dee95bc54 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -64,7 +64,7 @@ let subst_evar_constr evs n idf t =
ev_hyps = hyps ; ev_chop = chop } =
try evar_info k
with Not_found ->
- anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found")
+ anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found.")
in
seen := Int.Set.add id !seen;
(* Evar arguments are created in inverse order,
@@ -221,7 +221,7 @@ let eterm_obligations env name evm fs ?status t ty =
in
let loc, k = evar_source id evm in
let status = match k with
- | Evar_kinds.QuestionMark o -> o
+ | Evar_kinds.QuestionMark (o,_) -> o
| _ -> match status with
| Some o -> o
| None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))
@@ -325,7 +325,7 @@ type program_info = program_info_aux CEphemeron.key
let get_info x =
try CEphemeron.get x
with CEphemeron.InvalidKey ->
- CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker")
+ CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker.")
let assumption_message = Declare.assumption_message
diff --git a/vernac/record.ml b/vernac/record.ml
index 5accc8e379..2400fa6814 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -24,7 +24,6 @@ open Type_errors
open Constrexpr
open Constrexpr_ops
open Goptions
-open Sigma.Notations
open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
@@ -63,29 +62,28 @@ let interp_fields_evars env evars impls_env nots l =
List.fold_left2
(fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
let t', impl = interp_type_evars_impls env evars ~impls t in
- let b' = Option.map (fun x -> EConstr.Unsafe.to_constr (fst (interp_casted_constr_evars_impls env evars ~impls x t'))) b in
- let t' = EConstr.Unsafe.to_constr t' in
+ let b' = Option.map (fun x -> fst (interp_casted_constr_evars_impls env evars ~impls x t')) b in
let impls =
match i with
| Anonymous -> impls
- | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method t' impl) impls
+ | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method (EConstr.to_constr !evars t') impl) impls
in
let d = match b' with
| None -> LocalAssum (i,t')
| Some b' -> LocalDef (i,b',t')
in
List.iter (Metasyntax.set_notation_for_interpretation impls) no;
- (push_rel d env, impl :: uimpls, d::params, impls))
+ (EConstr.push_rel d env, impl :: uimpls, d::params, impls))
(env, [], [], impls_env) nots l
let compute_constructor_level evars env l =
List.fold_right (fun d (env, univ) ->
let univ =
if is_local_assum d then
- let s = Retyping.get_sort_of env evars (EConstr.of_constr (RelDecl.get_type d)) in
+ let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in
Univ.sup (univ_of_sort s) univ
else univ
- in (push_rel d env, univ))
+ in (EConstr.push_rel d env, univ))
l (env, Univ.type0m_univ)
let binder_of_decl = function
@@ -95,7 +93,7 @@ let binder_of_decl = function
let binders_of_decls = List.map binder_of_decl
-let typecheck_params_and_fields def id pl t ps nots fs =
+let typecheck_params_and_fields finite def id pl t ps nots fs =
let env0 = Global.env () in
let ctx = Evd.make_evar_universe_context env0 pl in
let evars = ref (Evd.from_ctx ctx) in
@@ -113,68 +111,68 @@ let typecheck_params_and_fields def id pl t ps nots fs =
Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps
in
let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in
- let newps = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) newps in
- let t', template = match t with
+ let typ, sort, template = match t with
| Some t ->
- let env = push_rel_context newps env0 in
+ let env = EConstr.push_rel_context newps env0 in
let poly =
match t with
| { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in
let s = interp_type_evars env evars ~impls:empty_internalization_env t in
let sred = Reductionops.whd_all env !evars s in
- let s = EConstr.Unsafe.to_constr s in
- let sred = EConstr.Unsafe.to_constr sred in
- (match kind_of_term sred with
- | Sort s' ->
+ (match EConstr.kind !evars sred with
+ | Sort s' ->
+ let s' = EConstr.ESorts.kind !evars s' in
(if poly then
match Evd.is_sort_variable !evars s' with
| Some l -> evars := Evd.make_flexible_variable !evars true l;
- sred, true
- | None -> s, false
- else s, false)
+ s, s', true
+ | None -> s, s', false
+ else s, s', false)
| _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
| None ->
let uvarkind = Evd.univ_flexible_alg in
- mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), true
+ let s = Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars in
+ EConstr.mkSort s, s, true
in
- let fullarity = it_mkProd_or_LetIn t' newps in
- let env_ar = push_rel_context newps (push_rel (LocalAssum (Name id,fullarity)) env0) in
+ let arity = EConstr.it_mkProd_or_LetIn typ newps in
+ let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in
+ let assums = List.filter is_local_assum newps in
+ let params = List.map (RelDecl.get_name %> out_name) assums in
+ let ty = Inductive (params,(finite != BiFinite)) in
+ let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr !evars arity] [imps] in
let env2,impls,newfs,data =
interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs)
in
- let sigma =
+ let evars =
Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars Evd.empty in
- let evars, nf = Evarutil.nf_evars_and_universes sigma in
- let arity = nf t' in
- let arity, evars =
+ let typ, evars =
let _, univ = compute_constructor_level evars env_ar newfs in
- let ctx, aritysort = Reduction.dest_arity env0 arity in
- assert(List.is_empty ctx); (* Ensured by above analysis *)
- if not def && (Sorts.is_prop aritysort ||
- (Sorts.is_set aritysort && is_impredicative_set env0)) then
- arity, evars
+ if not def && (Sorts.is_prop sort ||
+ (Sorts.is_set sort && is_impredicative_set env0)) then
+ typ, evars
else
- let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in
+ let evars = Evd.set_leq_sort env_ar evars (Type univ) sort in
if Univ.is_small_univ univ &&
- Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars aritysort) then
+ Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars sort) then
(* We can assume that the level in aritysort is not constrained
and clear it, if it is flexible *)
- mkArity (ctx, Sorts.sort_of_univ univ),
- Evd.set_eq_sort env_ar evars (Prop Pos) aritysort
- else arity, evars
+ EConstr.mkSort (Sorts.sort_of_univ univ),
+ Evd.set_eq_sort env_ar evars (Prop Pos) sort
+ else typ, evars
in
let evars, nf = Evarutil.nf_evars_and_universes evars in
- let newps = Context.Rel.map nf newps in
- let newfs = Context.Rel.map nf newfs in
+ let newfs = List.map (EConstr.to_rel_decl evars) newfs in
+ let newps = List.map (EConstr.to_rel_decl evars) newps in
+ let typ = EConstr.to_constr evars typ in
let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in
List.iter (iter_constr ce) (List.rev newps);
List.iter (iter_constr ce) (List.rev newfs);
- Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs
+ Evd.universe_context ?names:pl evars, typ, template, imps, newps, impls, newfs
let degenerate_decl decl =
let id = match RelDecl.get_name decl with
| Name id -> id
- | Anonymous -> anomaly (Pp.str "Unnamed record variable") in
+ | Anonymous -> anomaly (Pp.str "Unnamed record variable.") in
match decl with
| LocalAssum (_,t) -> (id, LocalAssumEntry t)
| LocalDef (_,b,_) -> (id, LocalDefEntry b)
@@ -366,15 +364,11 @@ let structure_signature ctx =
match l with [] -> Evd.empty
| [decl] ->
let env = Environ.empty_named_context_val in
- let evm = Sigma.Unsafe.of_evar_map evm in
- let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in
- let evm = Sigma.to_evar_map evm in
+ let (evm, _) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in
evm
| decl::tl ->
let env = Environ.empty_named_context_val in
- let evm = Sigma.Unsafe.of_evar_map evm in
- let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in
- let evm = Sigma.to_evar_map evm in
+ let (evm, ev) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in
let new_tl = Util.List.map_i
(fun pos decl ->
RelDecl.map_type (fun t -> EConstr.Unsafe.to_constr (Termops.replace_term evm (EConstr.mkRel pos) (EConstr.mkEvar(ev,[||])) (EConstr.of_constr t))) decl) 1 tl in
@@ -565,7 +559,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
(* Now, younger decl in params and fields is on top *)
let (pl, ctx), arity, template, implpars, params, implfs, fields =
States.with_state_protection (fun () ->
- typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in
+ typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in
let sign = structure_signature (fields@params) in
let gr = match kind with
| Class def ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c1d64cfe9..69492759be 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -31,7 +31,6 @@ open Redexpr
open Lemmas
open Misctypes
open Locality
-open Sigma.Notations
module NamedDecl = Context.Named.Declaration
@@ -67,7 +66,7 @@ let show_node () =
could, possibly, be cleaned away. (Feb. 2010) *)
()
-let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO")
+let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO.")
let show_top_evars () =
(* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
@@ -1003,12 +1002,12 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
let err_extra_args names =
user_err ~hdr:"vernac_declare_arguments"
(strbrk "Extra arguments: " ++
- prlist_with_sep pr_comma pr_name names ++ str ".")
+ prlist_with_sep pr_comma Name.print names ++ str ".")
in
let err_missing_args names =
user_err ~hdr:"vernac_declare_arguments"
(strbrk "The following arguments are not declared: " ++
- prlist_with_sep pr_comma pr_name names ++ str ".")
+ prlist_with_sep pr_comma Name.print names ++ str ".")
in
let rec check_extra_args extra_args =
@@ -1093,14 +1092,14 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
match !example_renaming with
| None -> mt ()
| Some (o,n) ->
- str "Argument " ++ pr_name o ++
- str " renamed to " ++ pr_name n ++ str ".");
+ str "Argument " ++ Name.print o ++
+ str " renamed to " ++ Name.print n ++ str ".");
let duplicate_names =
List.duplicates Name.equal (List.filter ((!=) Anonymous) names)
in
if not (List.is_empty duplicate_names) then begin
- let duplicates = prlist_with_sep pr_comma pr_name duplicate_names in
+ let duplicates = prlist_with_sep pr_comma Name.print duplicate_names in
user_err (strbrk "Some argument names are duplicated: " ++ duplicates)
end;
@@ -1129,7 +1128,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
anonymous argument implicit *)
| Anonymous :: _, (name, _) :: _ ->
user_err ~hdr:"vernac_declare_arguments"
- (strbrk"Argument "++ pr_name name ++
+ (strbrk"Argument "++ Name.print name ++
strbrk " cannot be declared implicit.")
| Name id :: inf_names, (name, impl) :: implicits ->
@@ -1550,8 +1549,7 @@ let vernac_check_may_eval ?loc redexp glopt rc =
let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in
let redfun env evm c =
let (redfun, _) = reduction_of_red_expr env r_interp in
- let evm = Sigma.Unsafe.of_evar_map evm in
- let Sigma (c, _, _) = redfun.Reductionops.e_redfun env evm c in
+ let (_, c) = redfun env evm c in
c
in
Feedback.msg_notice (print_eval redfun env sigma' rc j)
@@ -1765,12 +1763,11 @@ let vernac_locate = let open Feedback in function
let vernac_register id r =
if Pfedit.refining () then
user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
- let t = (Constrintern.global_reference (snd id)) in
- if not (isConst t) then
+ let kn = Constrintern.global_reference (snd id) in
+ if not (isConstRef kn) then
user_err Pp.(str "Register inline: a constant is expected");
- let kn = destConst t in
match r with
- | RegisterInline -> Global.register_inline (Univ.out_punivs kn)
+ | RegisterInline -> Global.register_inline (destConstRef kn)
(********************)
(* Proof management *)
@@ -1871,8 +1868,8 @@ exception End_of_input
*)
let vernac_load interp fname =
let interp x =
- let proof_mode = Proof_global.get_default_proof_mode_name () in
- Proof_global.activate_proof_mode proof_mode;
+ let proof_mode = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] in
+ Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
interp x in
let parse_sentence = Flags.with_option Flags.we_are_parsing
(fun po ->
@@ -1919,10 +1916,10 @@ let interp ?proof ?loc locality poly c =
| VernacToplevelControl e -> raise e
(* Resetting *)
- | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm")
- | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm")
- | VernacBack _ -> anomaly (str "VernacBack not handled by Stm")
- | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm")
+ | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.")
+ | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.")
+ | VernacBack _ -> anomaly (str "VernacBack not handled by Stm.")
+ | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm.")
(* This one is possible to handle here *)
| VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command")
@@ -2055,7 +2052,7 @@ let interp ?proof ?loc locality poly c =
| VernacProof (Some tac, Some l) ->
Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:yes";
vernac_set_end_tac tac; vernac_set_used_variables l
- | VernacProofMode mn -> Proof_global.set_proof_mode mn
+ | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
(* Extensions *)
| VernacExtend (opn,args) -> Vernacinterp.call ?locality (opn,args)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 14:19:23 +0000