aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/class.ml3
-rw-r--r--vernac/classes.ml22
-rw-r--r--vernac/classes.mli4
-rw-r--r--vernac/command.ml80
-rw-r--r--vernac/command.mli20
-rw-r--r--vernac/discharge.ml30
-rw-r--r--vernac/himsg.ml4
-rw-r--r--vernac/indschemes.ml14
-rw-r--r--vernac/indschemes.mli3
-rw-r--r--vernac/lemmas.ml80
-rw-r--r--vernac/lemmas.mli8
-rw-r--r--vernac/metasyntax.ml202
-rw-r--r--vernac/mltop.ml3
-rw-r--r--vernac/obligations.ml27
-rw-r--r--vernac/obligations.mli4
-rw-r--r--vernac/record.ml7
-rw-r--r--vernac/record.mli2
-rw-r--r--vernac/topfmt.ml5
-rw-r--r--vernac/vernacentries.ml47
-rw-r--r--vernac/vernacprop.ml3
20 files changed, 282 insertions, 286 deletions
diff --git a/vernac/class.ml b/vernac/class.ml
index be682977e..3915148a0 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -222,9 +222,10 @@ let build_id_coercion idf_opt source poly =
Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
(ident_key_of_class cl))
in
+ let univs = (snd (Evd.universe_context ~names:[] ~extensible:true sigma)) in
let constr_entry = (* Cast is necessary to express [val_f] is identity *)
DefinitionEntry
- (definition_entry ~types:typ_f ~poly ~univs:(snd (Evd.universe_context sigma))
+ (definition_entry ~types:typ_f ~poly ~univs
~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
in
let decl = (constr_entry, IsDefinition IdentityCoercion) in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index ab1892a18..c21345a2a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -111,14 +111,14 @@ let instance_hook k info global imps ?hook cst =
Typeclasses.declare_instance (Some info) (not global) cst;
(match hook with Some h -> h cst | None -> ())
-let declare_instance_constant k info global imps ?hook id pl poly evm term termtype =
+let declare_instance_constant k info global imps ?hook id decl poly evm term termtype =
let kind = IsDefinition Instance in
let evm =
let levels = Univ.LSet.union (Univops.universes_of_constr termtype)
(Univops.universes_of_constr term) in
Evd.restrict_universe_context evm levels
in
- let pl, uctx = Evd.universe_context ?names:pl evm in
+ let pl, uctx = Evd.check_univ_decl evm decl in
let entry =
Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
in
@@ -129,13 +129,13 @@ let declare_instance_constant k info global imps ?hook id pl poly evm term termt
instance_hook k info global imps ?hook (ConstRef kn);
id
-let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props
- ?(generalize=true)
- ?(tac:unit Proofview.tactic option) ?hook pri =
+let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
+ poly ctx (instid, bk, cl) props ?(generalize=true)
+ ?(tac:unit Proofview.tactic option) ?hook pri =
let env = Global.env() in
let ((loc, instid), pl) = instid in
- let uctx = Evd.make_evar_universe_context env pl in
- let evars = ref (Evd.from_ctx uctx) in
+ let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+ let evars = ref evd in
let tclass, ids =
match bk with
| Decl_kinds.Implicit ->
@@ -202,7 +202,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
nf t
in
Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
- let pl, ctx = Evd.universe_context ?names:pl !evars in
+ let pl, ctx = Evd.check_univ_decl !evars decl in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
(ParameterEntry
(None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
@@ -302,7 +302,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
in
let term = Option.map nf term in
if not (Evd.has_undefined evm) && not (Option.is_empty term) then
- declare_instance_constant k pri global imps ?hook id pl
+ declare_instance_constant k pri global imps ?hook id decl
poly evm (Option.get term) termtype
else if Flags.is_program_mode () || refine || Option.is_empty term then begin
let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
@@ -323,7 +323,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
let hook = Lemmas.mk_hook hook in
let ctx = Evd.evar_universe_context evm in
ignore (Obligations.add_definition id ?term:constr
- ?pl typ ctx ~kind:(Global,poly,Instance) ~hook obls);
+ ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls);
id
else
(Flags.silently
@@ -334,7 +334,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
the refinement manually.*)
let gls = List.rev (Evd.future_goals evm) in
let evm = Evd.reset_future_goals evm in
- Lemmas.start_proof id ?pl kind evm (EConstr.of_constr termtype)
+ Lemmas.start_proof id ~pl:decl kind evm (EConstr.of_constr termtype)
(Lemmas.mk_hook
(fun _ -> instance_hook k pri global imps ?hook));
(* spiwack: I don't know what to do with the status here. *)
diff --git a/vernac/classes.mli b/vernac/classes.mli
index fc2fdbbf3..fcdb5c3bc 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -30,7 +30,7 @@ val declare_instance_constant :
Impargs.manual_explicitation list -> (** implicits *)
?hook:(Globnames.global_reference -> unit) ->
Id.t -> (** name *)
- Id.t Loc.located list option ->
+ Univdecls.universe_decl ->
bool -> (* polymorphic *)
Evd.evar_map -> (* Universes *)
Constr.t -> (** body *)
@@ -43,7 +43,7 @@ val new_instance :
?refine:bool -> (** Allow refinement *)
Decl_kinds.polymorphic ->
local_binder_expr list ->
- typeclass_constraint ->
+ Vernacexpr.typeclass_constraint ->
(bool * constr_expr) option ->
?generalize:bool ->
?tac:unit Proofview.tactic ->
diff --git a/vernac/command.ml b/vernac/command.ml
index 0d6fd24cd..120f9590f 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -9,7 +9,6 @@
open Pp
open CErrors
open Util
-open Flags
open Term
open Vars
open Termops
@@ -91,8 +90,8 @@ let warn_implicits_in_term =
let interp_definition pl bl p red_option c ctypopt =
let env = Global.env() in
- let ctx = Evd.make_evar_universe_context env pl in
- let evdref = ref (Evd.from_ctx ctx) in
+ let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+ let evdref = ref evd in
let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
let nb_args = Context.Rel.nhyps ctx in
@@ -108,7 +107,7 @@ let interp_definition pl bl p red_option c ctypopt =
let body = nf (it_mkLambda_or_LetIn c ctx) in
let vars = Univops.universes_of_constr body in
let evd = Evd.restrict_universe_context !evdref vars in
- let pl, uctx = Evd.universe_context ?names:pl evd in
+ let pl, uctx = Evd.check_univ_decl evd decl in
imps1@(Impargs.lift_implicits nb_args imps2), pl,
definition_entry ~univs:uctx ~poly:p body
| Some ctyp ->
@@ -134,20 +133,20 @@ let interp_definition pl bl p red_option c ctypopt =
let vars = Univ.LSet.union (Univops.universes_of_constr body)
(Univops.universes_of_constr typ) in
let ctx = Evd.restrict_universe_context !evdref vars in
- let pl, uctx = Evd.universe_context ?names:pl ctx in
+ let pl, uctx = Evd.check_univ_decl ctx decl in
imps1@(Impargs.lift_implicits nb_args impsty), pl,
definition_entry ~types:typ ~poly:p
~univs:uctx body
in
- red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps
+ red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps
-let check_definition (ce, evd, _, imps) =
+let check_definition (ce, evd, _, _, imps) =
check_evars_are_solved (Global.env ()) evd Evd.empty;
ce
-let do_definition ident k pl bl red_option c ctypopt hook =
- let (ce, evd, pl', imps as def) =
- interp_definition pl bl (pi2 k) red_option c ctypopt
+let do_definition ident k univdecl bl red_option c ctypopt hook =
+ let (ce, evd, univdecl, pl', imps as def) =
+ interp_definition univdecl bl (pi2 k) red_option c ctypopt
in
if Flags.is_program_mode () then
let env = Global.env () in
@@ -164,8 +163,8 @@ let do_definition ident k pl bl red_option c ctypopt hook =
in
let ctx = Evd.evar_universe_context evd in
let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in
- ignore(Obligations.add_definition
- ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls)
+ ignore(Obligations.add_definition
+ ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
ignore(DeclareDef.declare_definition ident k ce pl' imps
(Lemmas.mk_hook
@@ -270,15 +269,15 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
let do_assumptions_bound_univs coe kind nl id pl c =
let env = Global.env () in
- let ctx = Evd.make_evar_universe_context env pl in
- let evdref = ref (Evd.from_ctx ctx) in
+ let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+ let evdref = ref evd in
let ty, impls = interp_type_evars_impls env evdref c in
let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
let ty = EConstr.Unsafe.to_constr ty in
let ty = nf ty in
let vars = Univops.universes_of_constr ty in
let evd = Evd.restrict_universe_context !evdref vars in
- let pl, uctx = Evd.universe_context ?names:pl evd in
+ let pl, uctx = Evd.check_univ_decl evd decl in
let uctx = Univ.ContextSet.of_context uctx in
let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in
st
@@ -318,7 +317,7 @@ let push_types env idl tl =
type structured_one_inductive_expr = {
ind_name : Id.t;
- ind_univs : lident list option;
+ ind_univs : Vernacexpr.universe_decl_expr option;
ind_arity : constr_expr;
ind_lc : (Id.t * constr_expr) list
}
@@ -367,7 +366,7 @@ let prepare_param = function
let rec check_anonymous_type ind =
let open Glob_term in
- match ind.CAst.v with
+ match DAst.get ind with
| GSort (GType []) -> true
| GProd ( _, _, _, e)
| GLetIn (_, _, _, e)
@@ -526,8 +525,8 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
List.iter check_param paramsl;
let env0 = Global.env() in
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 evd, decl = Univdecls.interp_univ_decl_opt env0 pl in
+ let evdref = ref evd in
let impls, ((env_params, ctx_params), userimpls) =
interp_context_evars env0 evdref paramsl
in
@@ -576,7 +575,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
let ctx_params = Context.Rel.map nf ctx_params in
let evd = !evdref in
- let pl, uctx = Evd.universe_context ?names:pl evd in
+ let pl, uctx = Evd.check_univ_decl evd decl in
List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities;
Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params;
List.iter (fun (_,ctyps,_) ->
@@ -692,7 +691,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
constrimpls)
impls;
let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in
- if_verbose Feedback.msg_info (minductive_message warn_prim names);
+ Flags.if_verbose Feedback.msg_info (minductive_message warn_prim names);
if mie.mind_entry_private == None
then declare_default_schemes mind;
mind
@@ -797,7 +796,7 @@ let check_mutuality env evd isfix fixl =
type structured_fixpoint_expr = {
fix_name : Id.t;
- fix_univs : lident list option;
+ fix_univs : universe_decl_expr option;
fix_annot : Id.t Loc.located option;
fix_binders : local_binder_expr list;
fix_body : constr_expr option;
@@ -917,8 +916,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
Coqlib.check_required_library ["Coq";"Program";"Wf"];
let env = Global.env() in
- let ctx = Evd.make_evar_universe_context env pl in
- let evdref = ref (Evd.from_ctx ctx) in
+ let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+ let evdref = ref evd in
let _, ((env', binders_rel), impls) = interp_context_evars env evdref bl in
let len = List.length binders_rel in
let top_env = push_rel_context binders_rel env in
@@ -1019,14 +1018,16 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let binders_rel = nf_evar_context !evdref binders_rel in
let binders = nf_evar_context !evdref binders in
let top_arity = Evarutil.nf_evar !evdref top_arity in
- let hook, recname, typ =
+ let pl, plext = Option.cata
+ (fun d -> d.univdecl_instance, d.univdecl_extensible_instance) ([],true) pl in
+ let hook, recname, typ =
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 (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
+ let pl, univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in
(*FIXME poly? *)
let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
(** FIXME: include locality *)
@@ -1052,7 +1053,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp
in
let ctx = Evd.evar_universe_context !evdref in
- ignore(Obligations.add_definition recname ~term:evars_def ?pl
+ ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
evars_typ ctx evars ~hook)
let interp_recursive isfix fixl notations =
@@ -1068,11 +1069,12 @@ let interp_recursive isfix fixl notations =
| None , acc -> acc
| x , None -> x
| Some ls , Some us ->
- if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then
+ let lsu = ls.univdecl_instance and usu = us.univdecl_instance in
+ if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) lsu usu) then
user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
Some us) fixl None in
- let ctx = Evd.make_evar_universe_context env all_universes in
- let evdref = ref (Evd.from_ctx ctx) in
+ let evd, decl = Univdecls.interp_univ_decl_opt env all_universes in
+ let evdref = ref evd in
let fixctxs, fiximppairs, fixannots =
List.split3 (List.map (interp_fix_context env evdref isfix) fixl) in
let fixctximpenvs, fixctximps = List.split fiximppairs in
@@ -1122,7 +1124,7 @@ let interp_recursive isfix fixl notations =
let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
(* Build the fix declaration block *)
- (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
+ (env,rec_sign,decl,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
let check_recursive isfix env evd (fixnames,fixdefs,_) =
check_evars_are_solved env evd Evd.empty;
@@ -1145,14 +1147,14 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
- List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps))))
+ List.map3 (fun id t (ctx,imps,_) -> (id,(t,(List.map RelDecl.get_name ctx,imps))))
fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
fixdefs) in
let evd = Evd.from_ctx ctx in
Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
- evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+ evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
else begin
(* We shortcut the proof process *)
let fixdefs = List.map Option.get fixdefs in
@@ -1165,8 +1167,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
let evd = Evd.from_ctx ctx in
let evd = Evd.restrict_universe_context evd vars in
+ let pl, ctx = Evd.check_univ_decl evd pl in
let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
- let pl, ctx = Evd.universe_context ?names:pl evd in
ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
@@ -1179,14 +1181,14 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
- List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps))))
+ List.map3 (fun id t (ctx,imps,_) -> (id,(t,(List.map RelDecl.get_name ctx,imps))))
fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
fixdefs) in
let evd = Evd.from_ctx ctx in
Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
- evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+ evd pl (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
else begin
(* We shortcut the proof process *)
let fixdefs = List.map Option.get fixdefs in
@@ -1197,8 +1199,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
let evd = Evd.from_ctx ctx in
let evd = Evd.restrict_universe_context evd vars in
- let pl, ctx = Evd.universe_context ?names:pl evd in
- ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
+ let pl, ctx = Evd.check_univ_decl evd pl in
+ ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
cofixpoint_message fixnames
@@ -1281,7 +1283,7 @@ let do_program_recursive local p fixkind fixl ntns =
| Obligations.IsFixpoint _ -> (local, p, Fixpoint)
| Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
in
- Obligations.add_mutual_definitions defs ~kind ?pl ctx ntns fixkind
+ Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind
let do_program_fixpoint local poly l =
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
diff --git a/vernac/command.mli b/vernac/command.mli
index 8d17f27c3..afa97aa24 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -26,11 +26,11 @@ val do_constraint : polymorphic ->
(** {6 Definitions/Let} *)
val interp_definition :
- lident list option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
+ Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
- Universes.universe_binders * Impargs.manual_implicits
+ Univdecls.universe_decl * Universes.universe_binders * Impargs.manual_implicits
-val do_definition : Id.t -> definition_kind -> lident list option ->
+val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
local_binder_expr list -> red_expr option -> constr_expr ->
constr_expr option -> unit Lemmas.declaration_hook -> unit
@@ -49,7 +49,7 @@ val declare_assumption : coercion_flag -> assumption_kind ->
global_reference * Univ.Instance.t * bool
val do_assumptions : locality * polymorphic * assumption_object_kind ->
- Vernacexpr.inline -> (plident list * constr_expr) with_coercion list -> bool
+ Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool
(* val declare_assumptions : variable Loc.located list -> *)
(* coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> *)
@@ -62,7 +62,7 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
type structured_one_inductive_expr = {
ind_name : Id.t;
- ind_univs : lident list option;
+ ind_univs : Vernacexpr.universe_decl_expr option;
ind_arity : constr_expr;
ind_lc : (Id.t * constr_expr) list
}
@@ -102,7 +102,7 @@ val do_mutual_inductive :
type structured_fixpoint_expr = {
fix_name : Id.t;
- fix_univs : lident list option;
+ fix_univs : Vernacexpr.universe_decl_expr option;
fix_annot : Id.t Loc.located option;
fix_binders : local_binder_expr list;
fix_body : constr_expr option;
@@ -127,24 +127,24 @@ type recursive_preentry =
val interp_fixpoint :
structured_fixpoint_expr list -> decl_notation list ->
- recursive_preentry * lident list option * Evd.evar_universe_context *
+ recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
(EConstr.rel_context * Impargs.manual_implicits * int option) list
val interp_cofixpoint :
structured_fixpoint_expr list -> decl_notation list ->
- recursive_preentry * lident list option * Evd.evar_universe_context *
+ recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
(EConstr.rel_context * Impargs.manual_implicits * int option) list
(** Registering fixpoints and cofixpoints in the environment *)
val declare_fixpoint :
locality -> polymorphic ->
- recursive_preentry * lident list option * Evd.evar_universe_context *
+ recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
(Context.Rel.t * Impargs.manual_implicits * int option) list ->
Proof_global.lemma_possible_guards -> decl_notation list -> unit
val declare_cofixpoint : locality -> polymorphic ->
- recursive_preentry * lident list option * Evd.evar_universe_context *
+ recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context *
(Context.Rel.t * Impargs.manual_implicits * int option) list ->
decl_notation list -> unit
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index 474c0b4dd..0e4bbd299 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -36,32 +36,32 @@ let detype_param =
I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
*)
-let abstract_inductive hyps nparams inds =
+let abstract_inductive decls nparamdecls inds =
let ntyp = List.length inds in
- let nhyp = Context.Named.length hyps in
- let args = Context.Named.to_instance mkVar (List.rev hyps) in
+ let ndecls = Context.Named.length decls in
+ let args = Context.Named.to_instance mkVar (List.rev decls) in
let args = Array.of_list args in
- let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in
+ let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in
let inds' =
List.map
(function (tname,arity,template,cnames,lc) ->
let lc' = List.map (substl subs) lc in
- let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b hyps) lc' in
- let arity' = Termops.it_mkNamedProd_wo_LetIn arity hyps in
+ let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b decls) lc' in
+ let arity' = Termops.it_mkNamedProd_wo_LetIn arity decls in
(tname,arity',template,cnames,lc''))
inds in
- let nparams' = nparams + Array.length args in
+ let nparamdecls' = nparamdecls + Array.length args in
(* To be sure to be the same as before, should probably be moved to process_inductive *)
let params' = let (_,arity,_,_,_) = List.hd inds' in
- let (params,_) = decompose_prod_n_assum nparams' arity in
+ let (params,_) = decompose_prod_n_assum nparamdecls' arity in
List.map detype_param params
in
let ind'' =
List.map
(fun (a,arity,template,c,lc) ->
- let _, short_arity = decompose_prod_n_assum nparams' arity in
+ let _, short_arity = decompose_prod_n_assum nparamdecls' arity in
let shortlc =
- List.map (fun c -> snd (decompose_prod_n_assum nparams' c)) lc in
+ List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in
{ mind_entry_typename = a;
mind_entry_arity = short_arity;
mind_entry_template = template;
@@ -77,9 +77,9 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
let ctx = List.rev mip.mind_arity_ctxt in
mkArity (List.rev ctx, Type ar.template_level), true
-let process_inductive (sechyps,_,_ as info) modlist mib =
- let sechyps = Lib.named_of_variable_context sechyps in
- let nparams = mib.mind_nparams in
+let process_inductive (section_decls,_,_ as info) modlist mib =
+ let section_decls = Lib.named_of_variable_context section_decls in
+ let nparamdecls = Context.Rel.length mib.mind_params_ctxt in
let subst, ind_univs =
match mib.mind_universes with
| Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx
@@ -105,8 +105,8 @@ let process_inductive (sechyps,_,_ as info) modlist mib =
Array.to_list mip.mind_consnames,
Array.to_list lc))
mib.mind_packets in
- let sechyps' = Context.Named.map discharge sechyps in
- let (params',inds') = abstract_inductive sechyps' nparams inds in
+ let section_decls' = Context.Named.map discharge section_decls in
+ let (params',inds') = abstract_inductive section_decls' nparamdecls inds in
let record = match mib.mind_record with
| Some (Some (id, _, _)) -> Some (Some id)
| Some None -> Some None
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 2be10a039..12b68fe38 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -418,7 +418,7 @@ let explain_not_product env sigma c =
let pr = pr_lconstr_env env sigma c in
str "The type of this term is a product" ++ spc () ++
str "while it is expected to be" ++
- (if is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
+ (if Term.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
(* TODO: use the names *)
(* (co)fixpoints *)
@@ -1176,7 +1176,7 @@ let error_not_allowed_case_analysis isrec kind i =
pr_inductive (Global.env()) (fst i) ++ str "."
let error_not_allowed_dependent_analysis isrec i =
- str "Dependent " ++ str (if isrec then "Induction" else "Case analysis") ++
+ str "Dependent " ++ str (if isrec then "induction" else "case analysis") ++
strbrk " is not allowed for inductive definition " ++
pr_inductive (Global.env()) i ++ str "."
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 6ea8bc7f2..90168843a 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -30,7 +30,6 @@ open Globnames
open Goptions
open Nameops
open Termops
-open Pretyping
open Nametab
open Smartlocate
open Vernacexpr
@@ -109,7 +108,7 @@ let _ =
let define id internal ctx c t =
let f = declare_constant ~internal in
- let _, univs = Evd.universe_context ctx in
+ let _, univs = Evd.universe_context ~names:[] ~extensible:true ctx in
let univs =
if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
else Monomorphic_const_entry univs
@@ -345,24 +344,23 @@ requested
let names inds recs isdep y z =
let ind = smart_global_inductive y in
let sort_of_ind = inductive_sort_family (snd (lookup_mind_specif env ind)) in
- let z' = interp_elimination_sort z in
let suffix = (
match sort_of_ind with
| InProp ->
- if isdep then (match z' with
+ if isdep then (match z with
| InProp -> inds ^ "_dep"
| InSet -> recs ^ "_dep"
| InType -> recs ^ "t_dep")
- else ( match z' with
+ else ( match z with
| InProp -> inds
| InSet -> recs
| InType -> recs ^ "t" )
| _ ->
- if isdep then (match z' with
+ if isdep then (match z with
| InProp -> inds
| InSet -> recs
| InType -> recs ^ "t" )
- else (match z' with
+ else (match z with
| InProp -> inds ^ "_nodep"
| InSet -> recs ^ "_nodep"
| InType -> recs ^ "t_nodep")
@@ -392,7 +390,7 @@ let do_mutual_induction_scheme lnamedepindsort =
evd, (ind,u), Some u
| Some ui -> evd, (ind, ui), inst
in
- (evd, (indu,dep,interp_elimination_sort sort) :: l, inst))
+ (evd, (indu,dep,sort) :: l, inst))
lnamedepindsort (Evd.from_env env0,[],None)
in
let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index 076e4938f..91c4c5825 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -11,7 +11,6 @@ open Names
open Term
open Environ
open Vernacexpr
-open Misctypes
(** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *)
@@ -32,7 +31,7 @@ val declare_rewriting_schemes : inductive -> unit
(** Mutual Minimality/Induction scheme *)
val do_mutual_induction_scheme :
- (Id.t located * bool * inductive * glob_sort) list -> unit
+ (Id.t located * bool * inductive * Sorts.family) list -> unit
(** Main calls to interpret the Scheme command *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 645320c60..192dd027c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -11,7 +11,6 @@
open CErrors
open Util
-open Flags
open Pp
open Names
open Term
@@ -49,7 +48,7 @@ let retrieve_first_recthm uctx = function
(NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
| ConstRef cst ->
let cb = Global.lookup_constant cst in
- let (_, uctx) = UState.universe_context uctx in
+ let (_, uctx) = UState.universe_context ~names:[] ~extensible:true uctx in
let inst = Univ.UContext.instance uctx in
let map (c, ctx) = Vars.subst_instance_constr inst c in
(Option.map map (Global.body_of_constant_body cb), is_opaque cb)
@@ -137,7 +136,7 @@ let find_mutually_recursive_statements thms =
assert (List.is_empty rest);
(* One occ. of common coind ccls and no common inductive hyps *)
if not (List.is_empty common_same_indhyp) then
- if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
+ Flags.if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
flush_all ();
indccl, true, []
| [], _::_ ->
@@ -145,7 +144,7 @@ let find_mutually_recursive_statements thms =
| ind :: _ ->
if List.distinct_f ind_ord (List.map pi1 ind)
then
- if_verbose Feedback.msg_info
+ Flags.if_verbose Feedback.msg_info
(strbrk
("Coinductive statements do not follow the order of "^
"definition, assuming the proof to be by induction."));
@@ -210,11 +209,11 @@ let compute_proof_name locality = function
locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
then
user_err ?loc (pr_id id ++ str " already exists.");
- id, pl
+ id
| None ->
- next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ()), None
+ next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ())
-let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
+let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) =
let t_i = norm t_i in
match body with
| None ->
@@ -222,7 +221,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
| Discharge ->
let impl = false in (* copy values from Vernacentries *)
let k = IsAssumption Conjectural in
- let c = SectionLocalAssum ((t_i,ctx),p,impl) in
+ let c = SectionLocalAssum ((t_i,Univ.ContextSet.of_context ctx),p,impl) in
let _ = declare_variable id (Lib.cwd(),c,k) in
(Discharge, VarRef id,imps)
| Local | Global ->
@@ -232,7 +231,6 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
| Global -> false
| Discharge -> assert false
in
- let ctx = Univ.ContextSet.to_context ctx in
let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in
let kn = declare_constant id ~local decl in
(locality,ConstRef kn,imps))
@@ -250,12 +248,11 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
match locality with
| Discharge ->
let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p
- ~univs:(Univ.ContextSet.to_context ctx) body_i in
+ ~univs:ctx body_i in
let c = SectionLocalDef const in
let _ = declare_variable id (Lib.cwd(), c, k) in
(Discharge,VarRef id,imps)
| Local | Global ->
- let ctx = Univ.ContextSet.to_context ctx in
let local = match locality with
| Local -> true
| Global -> false
@@ -312,12 +309,6 @@ let get_proof proof do_guard hook opacity =
in
id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
-let check_exist =
- List.iter (fun (loc,id) ->
- if not (Nametab.exists_cci (Lib.make_path id)) then
- user_err ?loc (pr_id id ++ str " does not exist.")
- )
-
let universe_proof_terminator compute_guard hook =
let open Proof_global in
make_terminator begin function
@@ -325,17 +316,16 @@ let universe_proof_terminator compute_guard hook =
admit (id,k,pe) pl (hook (Some ctx)) ();
Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
- let is_opaque, export_seff, exports = match opaque with
- | Vernacexpr.Transparent -> false, true, []
- | Vernacexpr.Opaque None -> true, false, []
- | Vernacexpr.Opaque (Some l) -> true, true, l in
+ let is_opaque, export_seff = match opaque with
+ | Vernacexpr.Transparent -> false, true
+ | Vernacexpr.Opaque -> true, false
+ in
let proof = get_proof proof compute_guard
(hook (Some (fst proof.Proof_global.universes))) is_opaque in
begin match idopt with
| None -> save_named ~export_seff proof
| Some (_,id) -> save_anonymous ~export_seff proof id
- end;
- check_exist exports
+ end
end
let standard_proof_terminator compute_guard hook =
@@ -369,7 +359,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_
let rec_tac_initializer finite guard thms snl =
if finite then
- match List.map (fun ((id,_),(t,_)) -> (id,EConstr.of_constr t)) thms with
+ match List.map (fun (id,(t,_)) -> (id,EConstr.of_constr t)) thms with
| (id,_)::l -> Tactics.mutual_cofix id l 0
| _ -> assert false
else
@@ -377,11 +367,11 @@ let rec_tac_initializer finite guard thms snl =
let nl = match snl with
| None -> List.map succ (List.map List.last guard)
| Some nl -> nl
- in match List.map2 (fun ((id,_),(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with
+ in match List.map2 (fun (id,(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with
| (id,n,_)::l -> Tactics.mutual_fix id n l 0
| _ -> assert false
-let start_proof_with_initialization kind ctx recguard thms snl hook =
+let start_proof_with_initialization kind ctx decl recguard thms snl hook =
let intro_tac (_, (_, (ids, _))) =
Tacticals.New.tclMAP (function
| Name id -> Tactics.intro_mustbe_force id
@@ -406,7 +396,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
(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.")
- | ((id,pl),(t,(_,imps)))::other_thms ->
+ | (id,(t,(_,imps)))::other_thms ->
let hook ctx strength ref =
let ctx = match ctx with
| None -> Evd.empty_evar_universe_context
@@ -418,22 +408,24 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
let body,opaq = retrieve_first_recthm ctx ref in
let subst = Evd.evar_universe_context_subst ctx in
let norm c = Universes.subst_opt_univs_constr subst c in
- let ctx = UState.context_set (*FIXME*) ctx in
+ let binders, ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in
let body = Option.map norm body in
- List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
+ List.map_i (save_remaining_recthms kind norm ctx binders body opaq) 1 other_thms in
let thms_data = (strength,ref,imps)::other_thms_data in
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
call_hook (fun exn -> exn) hook strength ref) thms_data in
- start_proof_univs id ?pl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+ start_proof_univs id ~pl:decl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
let start_proof_com ?inference_hook kind thms hook =
let env0 = Global.env () in
- let levels = Option.map snd (fst (List.hd thms)) in
- let evdref = ref (match levels with
- | None -> Evd.from_env env0
- | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
- in
+ let decl = fst (List.hd thms) in
+ let evd, decl =
+ match decl with
+ | None -> Evd.from_env env0, Univdecls.default_univ_decl
+ | Some decl ->
+ Univdecls.interp_univ_decl_opt env0 (snd decl) in
+ let evdref = ref evd in
let thms = List.map (fun (sopt,(bl,t)) ->
let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
let t', imps' = interp_type_evars_impls ~impls env evdref t in
@@ -449,16 +441,16 @@ let start_proof_com ?inference_hook kind thms hook =
let evd, nf = Evarutil.nf_evars_and_universes !evdref in
let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
let () =
- match levels with
- | None -> ()
- | Some l -> ignore (Evd.universe_context evd ?names:l)
+ if not decl.Misctypes.univdecl_extensible_instance then
+ ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance ~extensible:false)
+ else ()
in
let evd =
if pi2 kind then evd
else (* We fix the variables to ensure they won't be lowered to Set *)
Evd.fix_undefined_variables evd
in
- start_proof_with_initialization kind evd recguard thms snl hook
+ start_proof_with_initialization kind evd decl recguard thms snl hook
(* Saving a proof *)
@@ -507,11 +499,13 @@ let save_proof ?proof = function
let ids_def = Environ.global_vars_set env pproof in
Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
| _ -> None in
- let names = Proof_global.get_universe_binders () in
+ let decl = Proof_global.get_universe_decl () in
let evd = Evd.from_ctx universes in
- let binders, ctx = Evd.universe_context ?names evd in
- Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
- (universes, Some binders))
+ let binders, ctx = Evd.check_univ_decl evd decl in
+ let poly = pi2 k in
+ let binders = if poly then Some binders else None in
+ Admitted(id,k,(sec_vars, poly, (typ, ctx), None),
+ (universes, binders))
in
Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
| Vernacexpr.Proved (is_opaque,idopt) ->
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index a8c09c0fe..1e23c7314 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -20,13 +20,13 @@ val call_hook :
(** A hook start_proof calls on the type of the definition being started *)
val set_start_hook : (EConstr.types -> unit) -> unit
-val start_proof : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map ->
+val start_proof : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map ->
?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val -> EConstr.types ->
?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
unit declaration_hook -> unit
-val start_proof_univs : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map ->
+val start_proof_univs : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map ->
?terminator:(Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val -> EConstr.types ->
?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
@@ -38,9 +38,9 @@ val start_proof_com :
unit declaration_hook -> unit
val start_proof_with_initialization :
- goal_kind -> Evd.evar_map ->
+ goal_kind -> Evd.evar_map -> Univdecls.universe_decl ->
(bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
- ((Id.t (* name of thm *) * Proof_global.universe_binders option) *
+ (Id.t (* name of thm *) *
(types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
-> int list option -> unit declaration_hook -> unit
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8b042a3ca..5298ef2e4 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Pp
-open Flags
open CErrors
open Util
open Names
@@ -98,102 +97,104 @@ let pr_grammar = function
quote (except a single quote alone) must be quoted) *)
let parse_format ((loc, str) : lstring) =
- let str = " "^str in
- let l = String.length str in
- let push_token a = function
- | cur::l -> (a::cur)::l
- | [] -> [[a]] in
- let push_white n l =
- if Int.equal n 0 then l else push_token (UnpTerminal (String.make n ' ')) l in
- let close_box i b = function
- | a::(_::_ as l) -> push_token (UnpBox (b,a)) l
- | _ -> user_err Pp.(str "Non terminated box in format.") in
- let close_quotation i =
- if i < String.length str && str.[i] == '\'' && (Int.equal (i+1) l || str.[i+1] == ' ')
- then i+1
- else user_err Pp.(str "Incorrectly terminated quoted expression.") in
+ let len = String.length str in
+ (* TODO: update the line of the location when the string contains newlines *)
+ let make_loc i j = Option.map (Loc.shift_loc (i+1) (j-len)) loc in
+ let push_token loc a = function
+ | (i,cur)::l -> (i,(loc,a)::cur)::l
+ | [] -> assert false in
+ let push_white i n l =
+ if Int.equal n 0 then l else push_token (make_loc i (i+n)) (UnpTerminal (String.make n ' ')) l in
+ let close_box start stop b = function
+ | (_,a)::(_::_ as l) -> push_token (make_loc start stop) (UnpBox (b,a)) l
+ | [a] -> user_err ?loc:(make_loc start stop) Pp.(str "Non terminated box in format.")
+ | [] -> assert false in
+ let close_quotation start i =
+ if i < len && str.[i] == '\'' then
+ if (Int.equal (i+1) len || str.[i+1] == ' ')
+ then i+1
+ else user_err ?loc:(make_loc (i+1) (i+1)) Pp.(str "Space expected after quoted expression.")
+ else
+ user_err ?loc:(make_loc start (i-1)) Pp.(str "Beginning of quoted expression expected to be ended by a quote.") in
let rec spaces n i =
- if i < String.length str && str.[i] == ' ' then spaces (n+1) (i+1)
+ if i < len && str.[i] == ' ' then spaces (n+1) (i+1)
else n in
let rec nonspaces quoted n i =
- if i < String.length str && str.[i] != ' ' then
+ if i < len && str.[i] != ' ' then
if str.[i] == '\'' && quoted &&
- (i+1 >= String.length str || str.[i+1] == ' ')
- then if Int.equal n 0 then user_err Pp.(str "Empty quoted token.") else n
+ (i+1 >= len || str.[i+1] == ' ')
+ then if Int.equal n 0 then user_err ?loc:(make_loc (i-1) i) Pp.(str "Empty quoted token.") else n
else nonspaces quoted (n+1) (i+1)
else
- if quoted then user_err Pp.(str "Spaces are not allowed in (quoted) symbols.")
+ if quoted then user_err ?loc:(make_loc i i) Pp.(str "Spaces are not allowed in (quoted) symbols.")
else n in
let rec parse_non_format i =
let n = nonspaces false 0 i in
- push_token (UnpTerminal (String.sub str i n)) (parse_token (i+n))
+ push_token (make_loc i (i+n-1)) (UnpTerminal (String.sub str i n)) (parse_token 1 (i+n))
and parse_quoted n i =
- if i < String.length str then match str.[i] with
+ if i < len then match str.[i] with
(* Parse " // " *)
- | '/' when i <= String.length str && str.[i+1] == '/' ->
- (* We forget the useless n spaces... *)
- push_token (UnpCut PpFnl)
- (parse_token (close_quotation (i+2)))
+ | '/' when i+1 < len && str.[i+1] == '/' ->
+ (* We discard the useless n spaces... *)
+ push_token (make_loc (i-n) (i+1)) (UnpCut PpFnl)
+ (parse_token 1 (close_quotation i (i+2)))
(* Parse " .. / .. " *)
- | '/' when i <= String.length str ->
+ | '/' when i+1 < len ->
let p = spaces 0 (i+1) in
- push_token (UnpCut (PpBrk (n,p)))
- (parse_token (close_quotation (i+p+1)))
+ push_token (make_loc (i-n) (i+p)) (UnpCut (PpBrk (n,p)))
+ (parse_token 1 (close_quotation i (i+p+1)))
| c ->
(* The spaces are real spaces *)
- push_white n (match c with
+ push_white i n (match c with
| '[' ->
- if i <= String.length str then match str.[i+1] with
+ if i+1 < len then match str.[i+1] with
(* Parse " [h .. ", *)
- | 'h' when i+1 <= String.length str && str.[i+2] == 'v' ->
- (parse_box (fun n -> PpHVB n) (i+3))
+ | 'h' when i+1 <= len && str.[i+2] == 'v' ->
+ (parse_box i (fun n -> PpHVB n) (i+3))
(* Parse " [v .. ", *)
| 'v' ->
- parse_box (fun n -> PpVB n) (i+2)
+ parse_box i (fun n -> PpVB n) (i+2)
(* Parse " [ .. ", *)
| ' ' | '\'' ->
- parse_box (fun n -> PpHOVB n) (i+1)
- | _ -> user_err Pp.(str "\"v\", \"hv\", \" \" expected after \"[\" in format.")
- else user_err Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.")
+ parse_box i (fun n -> PpHOVB n) (i+1)
+ | _ -> user_err ?loc:(make_loc i i) Pp.(str "\"v\", \"hv\", \" \" expected after \"[\" in format.")
+ else user_err ?loc:(make_loc i i) Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.")
(* Parse "]" *)
| ']' ->
- ([] :: parse_token (close_quotation (i+1)))
+ ((i,[]) :: parse_token 1 (close_quotation i (i+1)))
(* Parse a non formatting token *)
| c ->
let n = nonspaces true 0 i in
- push_token (UnpTerminal (String.sub str (i-1) (n+2)))
- (parse_token (close_quotation (i+n))))
+ push_token (make_loc i (i+n-1)) (UnpTerminal (String.sub str (i-1) (n+2)))
+ (parse_token 1 (close_quotation i (i+n))))
else
if Int.equal n 0 then []
- else user_err Pp.(str "Ending spaces non part of a format annotation.")
- and parse_box box i =
+ else user_err ?loc:(make_loc (len-n) len) Pp.(str "Ending spaces non part of a format annotation.")
+ and parse_box start box i =
let n = spaces 0 i in
- close_box i (box n) (parse_token (close_quotation (i+n)))
- and parse_token i =
+ close_box start (i+n-1) (box n) (parse_token 1 (close_quotation i (i+n)))
+ and parse_token k i =
let n = spaces 0 i in
let i = i+n in
- if i < l then match str.[i] with
+ if i < len then match str.[i] with
(* Parse a ' *)
- | '\'' when i+1 >= String.length str || str.[i+1] == ' ' ->
- push_white (n-1) (push_token (UnpTerminal "'") (parse_token (i+1)))
+ | '\'' when i+1 >= len || str.[i+1] == ' ' ->
+ push_white (i-n) (n-k) (push_token (make_loc i (i+1)) (UnpTerminal "'") (parse_token 1 (i+1)))
(* Parse the beginning of a quoted expression *)
| '\'' ->
- parse_quoted (n-1) (i+1)
+ parse_quoted (n-k) (i+1)
(* Otherwise *)
| _ ->
- push_white (n-1) (parse_non_format i)
- else push_white n [[]]
+ push_white (i-n) (n-k) (parse_non_format i)
+ else push_white (i-n) n [(len,[])]
in
- try
- if not (String.is_empty str) then match parse_token 0 with
- | [l] -> l
- | _ -> user_err Pp.(str "Box closed without being opened in format.")
- else
- user_err Pp.(str "Empty format.")
- with reraise ->
- let (e, info) = CErrors.push reraise in
- let info = Option.cata (Loc.add_loc info) info loc in
- iraise (e, info)
+ if not (String.is_empty str) then
+ match parse_token 0 0 with
+ | [_,l] -> l
+ | (i,_)::_ -> user_err ?loc:(make_loc i i) Pp.(str "Box closed without being opened.")
+ | [] -> assert false
+ else
+ []
(***********************)
(* Analyzing notations *)
@@ -384,11 +385,11 @@ let is_next_terminal = function Terminal _ :: _ -> true | _ -> false
let is_next_break = function Break _ :: _ -> true | _ -> false
-let add_break n l = UnpCut (PpBrk(n,0)) :: l
+let add_break n l = (None,UnpCut (PpBrk(n,0))) :: l
let add_break_if_none n = function
- | ((UnpCut (PpBrk _) :: _) | []) as l -> l
- | l -> UnpCut (PpBrk(n,0)) :: l
+ | (((_,UnpCut (PpBrk _)) :: _) | []) as l -> l
+ | l -> (None,UnpCut (PpBrk(n,0))) :: l
let check_open_binder isopen sl m =
let pr_token = function
@@ -414,30 +415,30 @@ let make_hunks etyps symbols from =
let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
let u = UnpMetaVar (i,prec) in
if is_next_non_terminal prods then
- u :: add_break_if_none 1 (make prods)
+ (None,u) :: add_break_if_none 1 (make prods)
else
- u :: make_with_space prods
+ (None,u) :: make_with_space prods
| Terminal s :: prods when List.exists is_non_terminal prods ->
if (is_comma s || is_operator s) then
(* Always a breakable space after comma or separator *)
- UnpTerminal s :: add_break_if_none 1 (make prods)
+ (None,UnpTerminal s) :: add_break_if_none 1 (make prods)
else if is_right_bracket s && is_next_terminal prods then
(* Always no space after right bracked, but possibly a break *)
- UnpTerminal s :: add_break_if_none 0 (make prods)
+ (None,UnpTerminal s) :: add_break_if_none 0 (make prods)
else if is_left_bracket s && is_next_non_terminal prods then
- UnpTerminal s :: make prods
+ (None,UnpTerminal s) :: make prods
else if not (is_next_break prods) then
(* Add rigid space, no break, unless user asked for something *)
- UnpTerminal (s^" ") :: make prods
+ (None,UnpTerminal (s^" ")) :: make prods
else
(* Rely on user spaces *)
- UnpTerminal s :: make prods
+ (None,UnpTerminal s) :: make prods
| Terminal s :: prods ->
(* Separate but do not cut a trailing sequence of terminal *)
(match prods with
- | Terminal _ :: _ -> UnpTerminal (s^" ") :: make prods
- | _ -> UnpTerminal s :: make prods)
+ | Terminal _ :: _ -> (None,UnpTerminal (s^" ")) :: make prods
+ | _ -> (None,UnpTerminal s) :: make prods)
| Break n :: prods ->
add_break n (make prods)
@@ -452,12 +453,12 @@ let make_hunks etyps symbols from =
(* We add NonTerminal for simulation but remove it afterwards *)
else snd (List.sep_last (make (sl@[NonTerminal m]))) in
let hunk = match typ with
- | ETConstr _ -> UnpListMetaVar (i,prec,sl')
+ | ETConstr _ -> UnpListMetaVar (i,prec,List.map snd sl')
| ETBinder isopen ->
check_open_binder isopen sl m;
- UnpBinderListMetaVar (i,isopen,sl')
+ UnpBinderListMetaVar (i,isopen,List.map snd sl')
| _ -> assert false in
- hunk :: make_with_space prods
+ (None,hunk) :: make_with_space prods
| [] -> []
@@ -466,7 +467,7 @@ let make_hunks etyps symbols from =
| Terminal s' :: prods'->
if is_operator s' then
(* A rigid space before operator and a breakable after *)
- UnpTerminal (" "^s') :: add_break_if_none 1 (make prods')
+ (None,UnpTerminal (" "^s')) :: add_break_if_none 1 (make prods')
else if is_comma s' then
(* No space whatsoever before comma *)
make prods
@@ -487,58 +488,63 @@ let make_hunks etyps symbols from =
(* Build default printing rules from explicit format *)
-let error_format () = user_err Pp.(str "The format does not match the notation.")
+let error_format ?loc () = user_err ?loc Pp.(str "The format does not match the notation.")
let rec split_format_at_ldots hd = function
- | UnpTerminal s :: fmt when String.equal s (Id.to_string ldots_var) -> List.rev hd, fmt
+ | (loc,UnpTerminal s) :: fmt when String.equal s (Id.to_string ldots_var) -> loc, List.rev hd, fmt
| u :: fmt ->
check_no_ldots_in_box u;
split_format_at_ldots (u::hd) fmt
| [] -> raise Exit
and check_no_ldots_in_box = function
- | UnpBox (_,fmt) ->
+ | (_,UnpBox (_,fmt)) ->
(try
- let _ = split_format_at_ldots [] fmt in
- user_err Pp.(str ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse."))
+ let loc,_,_ = split_format_at_ldots [] fmt in
+ user_err ?loc Pp.(str ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse."))
with Exit -> ())
| _ -> ()
+let error_not_same ?loc () =
+ user_err ?loc Pp.(str "The format is not the same on the right- and left-hand sides of the special token \"..\".")
+
let skip_var_in_recursive_format = function
- | UnpTerminal _ :: sl (* skip first var *) ->
+ | (_,UnpTerminal s) :: sl (* skip first var *) when not (List.for_all (fun c -> c = " ") (String.explode s)) ->
(* To do, though not so important: check that the names match
the names in the notation *)
sl
- | _ -> error_format ()
+ | (loc,_) :: _ -> error_not_same ?loc ()
+ | [] -> assert false
let read_recursive_format sl fmt =
let get_head fmt =
let sl = skip_var_in_recursive_format fmt in
- try split_format_at_ldots [] sl with Exit -> error_format () in
+ try split_format_at_ldots [] sl with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in
let rec get_tail = function
- | a :: sepfmt, b :: fmt when Pervasives.(=) a b -> get_tail (sepfmt, fmt) (* FIXME *)
+ | (loc,a) :: sepfmt, (_,b) :: fmt when Pervasives.(=) a b -> get_tail (sepfmt, fmt) (* FIXME *)
| [], tail -> skip_var_in_recursive_format tail
- | _ -> user_err Pp.(str "The format is not the same on the right and left hand side of the special token \"..\".") in
- let slfmt, fmt = get_head fmt in
+ | (loc,_) :: _, ([] | (_,UnpTerminal _) :: _)-> error_not_same ?loc ()
+ | _, (loc,_)::_ -> error_not_same ?loc () in
+ let loc, slfmt, fmt = get_head fmt in
slfmt, get_tail (slfmt, fmt)
let hunks_of_format (from,(vars,typs)) symfmt =
let rec aux = function
- | symbs, (UnpTerminal s' as u) :: fmt
+ | symbs, (_,(UnpTerminal s' as u)) :: fmt
when String.equal s' (String.make (String.length s') ' ') ->
let symbs, l = aux (symbs,fmt) in symbs, u :: l
- | Terminal s :: symbs, (UnpTerminal s') :: fmt
+ | Terminal s :: symbs, (_,UnpTerminal s') :: fmt
when String.equal s (String.drop_simple_quotes s') ->
let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
- | NonTerminal s :: symbs, UnpTerminal s' :: fmt when Id.equal s (Id.of_string s') ->
+ | NonTerminal s :: symbs, (_,UnpTerminal s') :: fmt when Id.equal s (Id.of_string s') ->
let i = index_id s vars in
let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
let symbs, l = aux (symbs,fmt) in symbs, UnpMetaVar (i,prec) :: l
- | symbs, UnpBox (a,b) :: fmt ->
+ | symbs, (_,UnpBox (a,b)) :: fmt ->
let symbs', b' = aux (symbs,b) in
let symbs', l = aux (symbs',fmt) in
- symbs', UnpBox (a,b') :: l
- | symbs, (UnpCut _ as u) :: fmt ->
+ symbs', UnpBox (a,List.map (fun x -> (None,x)) b') :: l
+ | symbs, (_,(UnpCut _ as u)) :: fmt ->
let symbs, l = aux (symbs,fmt) in symbs, u :: l
| SProdList (m,sl) :: symbs, fmt ->
let i = index_id m vars in
@@ -546,7 +552,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
let _,prec = precedence_of_entry_type from typ in
let slfmt,fmt = read_recursive_format sl fmt in
let sl, slfmt = aux (sl,slfmt) in
- if not (List.is_empty sl) then error_format ();
+ if not (List.is_empty sl) then error_format ?loc:(fst (List.last fmt)) ();
let symbs, l = aux (symbs,fmt) in
let hunk = match typ with
| ETConstr _ -> UnpListMetaVar (i,prec,slfmt)
@@ -556,7 +562,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
| _ -> assert false in
symbs, hunk :: l
| symbs, [] -> symbs, []
- | _, _ -> error_format ()
+ | _, fmt -> error_format ?loc:(fst (List.hd fmt)) ()
in
match aux symfmt with
| [], l -> l
@@ -795,7 +801,7 @@ type notation_modifier = {
(* common to syn_data below *)
only_parsing : bool;
only_printing : bool;
- compat : compat_version option;
+ compat : Flags.compat_version option;
format : string Loc.located option;
extra : (string * string) list;
}
@@ -1074,7 +1080,7 @@ module SynData = struct
(* Fields coming from the vernac-level modifiers *)
only_parsing : bool;
only_printing : bool;
- compat : compat_version option;
+ compat : Flags.compat_version option;
format : string Loc.located option;
extra : (string * string) list;
@@ -1390,7 +1396,7 @@ let add_notation_interpretation ((loc,df),c,sc) =
let set_notation_for_interpretation impls ((_,df),c,sc) =
(try ignore
- (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ());
+ (Flags.silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ());
with NoSyntaxRule ->
user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index e8a0ba3dd..1edbd1a85 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -9,7 +9,6 @@
open CErrors
open Util
open Pp
-open Flags
open Libobject
open System
@@ -365,7 +364,7 @@ let trigger_ml_object verb cache reinit ?path name =
else begin
let file = file_of_name (Option.default name path) in
let path =
- if_verbose_load (verb && not !quiet) load_ml_object name ?path file in
+ if_verbose_load (verb && not !Flags.quiet) load_ml_object name ?path file in
add_loaded_module name (Some path);
if cache then perform_cache_obj name
end
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index a4fe49020..81218308f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -304,7 +304,7 @@ type program_info_aux = {
prg_body: constr;
prg_type: constr;
prg_ctx: Evd.evar_universe_context;
- prg_pl: Id.t Loc.located list option;
+ prg_univdecl: Univdecls.universe_decl;
prg_obligations: obligations;
prg_deps : Id.t list;
prg_fixkind : fixpoint_kind option ;
@@ -474,8 +474,7 @@ let declare_definition prg =
(Evd.evar_universe_context_subst prg.prg_ctx) in
let opaque = prg.prg_opaque in
let fix_exn = Hook.get get_fix_exn () in
- let pl, ctx =
- Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in
+ let pl, ctx = Evd.check_univ_decl (Evd.from_ctx prg.prg_ctx) prg.prg_univdecl in
let ce =
definition_entry ~fix_exn
~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
@@ -658,7 +657,7 @@ let declare_obligation prg obl body ty uctx =
else
Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
-let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
+let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind
notations obls impls kind reduce hook =
let obls', b =
match b with
@@ -679,7 +678,7 @@ let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
obls, b
in
{ prg_name = n ; prg_body = b; prg_type = reduce t;
- prg_ctx = ctx; prg_pl = pl;
+ prg_ctx = ctx; prg_univdecl = udecl;
prg_obligations = (obls', Array.length obls');
prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
prg_implicits = impls; prg_kind = kind; prg_reduce = reduce;
@@ -847,9 +846,9 @@ let obligation_terminator name num guard hook auto pf =
let obl = obls.(num) in
let status =
match obl.obl_status, opq with
- | (_, Evar_kinds.Expand), Vernacexpr.Opaque _ -> err_not_transp ()
- | (true, _), Vernacexpr.Opaque _ -> err_not_transp ()
- | (false, _), Vernacexpr.Opaque _ -> Evar_kinds.Define true
+ | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp ()
+ | (true, _), Vernacexpr.Opaque -> err_not_transp ()
+ | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true
| (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false
| (_, status), Vernacexpr.Transparent -> status
in
@@ -889,7 +888,7 @@ in
let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
Univ.Instance.empty, Evd.evar_universe_context ctx'
else
- let (_, uctx) = UState.universe_context ctx' in
+ let (_, uctx) = UState.universe_context ~names:[] ~extensible:true ctx' in
Univ.UContext.instance uctx, ctx'
in
let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
@@ -1068,11 +1067,12 @@ let show_term n =
Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
-let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl)
+ ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
let sign = Decls.initialize_named_context_for_proof () in
let info = Id.print n ++ str " has type-checked" in
- let prg = init_prog_info sign ~opaque n pl term t ctx [] None [] obls implicits kind reduce hook in
+ let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in
let obls,_ = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
Flags.if_verbose Feedback.msg_info (info ++ str ".");
@@ -1087,13 +1087,14 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit
| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
| _ -> res)
-let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
+let add_mutual_definitions l ctx ?(univdecl=Univdecls.default_univ_decl) ?tactic
+ ?(kind=Global,false,Definition) ?(reduce=reduce)
?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
let sign = Decls.initialize_named_context_for_proof () in
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
List.iter
(fun (n, b, t, imps, obls) ->
- let prg = init_prog_info sign ~opaque n pl (Some b) t ctx deps (Some fixkind)
+ let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind)
notations obls imps kind reduce hook
in progmap_add n (CEphemeron.create prg)) l;
let _defined =
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 5614403ba..11c2553ae 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -53,7 +53,7 @@ val default_tactic : unit Proofview.tactic ref
val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types ->
Evd.evar_universe_context ->
- ?pl:(Id.t Loc.located list) -> (* Universe binders *)
+ ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
?kind:Decl_kinds.definition_kind ->
?tactic:unit Proofview.tactic ->
@@ -71,7 +71,7 @@ val add_mutual_definitions :
(Names.Id.t * Term.constr * Term.types *
(Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
Evd.evar_universe_context ->
- ?pl:(Id.t Loc.located list) -> (* Universe binders *)
+ ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
?tactic:unit Proofview.tactic ->
?kind:Decl_kinds.definition_kind ->
?reduce:(Term.constr -> Term.constr) ->
diff --git a/vernac/record.ml b/vernac/record.ml
index a2e443e5f..4fb607dec 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -95,8 +95,8 @@ let binders_of_decls = List.map binder_of_decl
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
+ let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in
+ let evars = ref evd in
let _ =
let error bk (loc, name) =
match bk, name with
@@ -165,9 +165,10 @@ let typecheck_params_and_fields finite def id pl t ps nots fs =
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
+ let univs = Evd.check_univ_decl evars decl in
List.iter (iter_constr ce) (List.rev newps);
List.iter (iter_constr ce) (List.rev newfs);
- Evd.universe_context ?names:pl evars, typ, template, imps, newps, impls, newfs
+ univs, typ, template, imps, newps, impls, newfs
let degenerate_decl decl =
let id = match RelDecl.get_name decl with
diff --git a/vernac/record.mli b/vernac/record.mli
index 9a0c9ef9d..aea474581 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -39,7 +39,7 @@ val declare_structure :
val definition_structure :
inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
- Decl_kinds.recursivity_kind * plident with_coercion * local_binder_expr list *
+ Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list *
(local_decl_expr with_instance with_priority with_notation) list *
Id.t * constr_expr option -> global_reference
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index e7b14309d..6a10eb43a 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -292,10 +292,11 @@ let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning
(* This is specific to the toplevel *)
let pr_loc loc =
let fname = loc.Loc.fname in
- if CString.equal fname "" then
+ match fname with
+ | Loc.ToplevelInput ->
Loc.(str"Toplevel input, characters " ++ int loc.bp ++
str"-" ++ int loc.ep ++ str":")
- else
+ | Loc.InFile fname ->
Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
str", line " ++ int loc.line_nb ++ str", characters " ++
int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 8738e58e8..ccae4359e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -11,7 +11,6 @@
open Pp
open CErrors
open Util
-open Flags
open Names
open Nameops
open Term
@@ -409,9 +408,10 @@ let dump_global r =
(**********)
(* Syntax *)
-let vernac_syntax_extension locality local =
+let vernac_syntax_extension locality local infix l =
let local = enforce_module_locality locality local in
- Metasyntax.add_syntax_extension local
+ if infix then Metasyntax.check_infix_modifiers (snd l);
+ Metasyntax.add_syntax_extension local l
let vernac_delimiters sc = function
| Some lr -> Metasyntax.add_delimiters sc lr
@@ -507,7 +507,7 @@ let vernac_exact_proof c =
(* spiwack: for simplicity I do not enforce that "Proof proof_term" is
called only at the begining of a proof. *)
let status = Pfedit.by (Tactics.exact_proof c) in
- save_proof (Vernacexpr.(Proved(Opaque None,None)));
+ save_proof (Vernacexpr.(Proved(Opaque,None)));
if not status then Feedback.feedback Feedback.AddedAxiom
let vernac_assumption locality poly (local, kind) l nl =
@@ -656,7 +656,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
id binders_ast (Enforce mty_ast) []
in
Dumpglob.dump_moddef ?loc mp "mod";
- if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared");
+ Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared");
Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export
let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
@@ -677,7 +677,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
export id binders_ast mty_ast_o
in
Dumpglob.dump_moddef ?loc mp "mod";
- if_verbose Feedback.msg_info
+ Flags.if_verbose Feedback.msg_info
(str "Interactive Module " ++ pr_id id ++ str " started");
List.iter
(fun (export,id) ->
@@ -695,7 +695,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
id binders_ast mty_ast_o mexpr_ast_l
in
Dumpglob.dump_moddef ?loc mp "mod";
- if_verbose Feedback.msg_info
+ Flags.if_verbose Feedback.msg_info
(str "Module " ++ pr_id id ++ str " is defined");
Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)])
export
@@ -703,7 +703,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
let vernac_end_module export (loc,id as lid) =
let mp = Declaremods.end_module () in
Dumpglob.dump_modref ?loc mp "mod";
- if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined");
+ Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined");
Option.iter (fun export -> vernac_import export [Ident lid]) export
let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
@@ -724,7 +724,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
id binders_ast mty_sign
in
Dumpglob.dump_moddef ?loc mp "modtype";
- if_verbose Feedback.msg_info
+ Flags.if_verbose Feedback.msg_info
(str "Interactive Module Type " ++ pr_id id ++ str " started");
List.iter
(fun (export,id) ->
@@ -743,13 +743,13 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
id binders_ast mty_sign mty_ast_l
in
Dumpglob.dump_moddef ?loc mp "modtype";
- if_verbose Feedback.msg_info
+ Flags.if_verbose Feedback.msg_info
(str "Module Type " ++ pr_id id ++ str " is defined")
let vernac_end_modtype (loc,id) =
let mp = Declaremods.end_modtype () in
Dumpglob.dump_modref ?loc mp "modtype";
- if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
+ Flags.if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
let vernac_include l =
Declaremods.declare_include Modintern.interp_module_ast l
@@ -817,7 +817,7 @@ let vernac_coercion locality poly local ref qids qidt =
let source = cl_of_qualid qids in
let ref' = smart_global ref in
Class.try_add_new_coercion_with_target ref' ~local poly ~source ~target;
- if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
+ Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
let vernac_identity_coercion locality poly local id qids qidt =
let local = enforce_locality locality local in
@@ -919,7 +919,7 @@ let vernac_chdir = function
so we make it an error. *)
user_err Pp.(str ("Cd failed: " ^ err))
end;
- if_verbose Feedback.msg_info (str (Sys.getcwd()))
+ Flags.if_verbose Feedback.msg_info (str (Sys.getcwd()))
(********************)
@@ -1230,7 +1230,7 @@ let vernac_reserve bl =
let env = Global.env() in
let sigma = Evd.from_env env in
let t,ctx = Constrintern.interp_type env sigma c in
- let t = Detyping.detype false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in
+ let t = Detyping.detype Detyping.Now false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in
let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
Reserve.declare_reserved_type idl t)
in List.iter sb_decl bl
@@ -1301,7 +1301,7 @@ let _ =
optname = "automatic introduction of variables";
optkey = ["Automatic";"Introduction"];
optread = Flags.is_auto_intros;
- optwrite = make_auto_intros }
+ optwrite = Flags.make_auto_intros }
let _ =
declare_bool_option
@@ -1555,7 +1555,7 @@ let vernac_check_may_eval ?loc redexp glopt rc =
let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in
Evarconv.check_problems_are_solved env sigma';
let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
- let pl, uctx = Evd.universe_context sigma' in
+ let pl, uctx = Evd.universe_context ~names:[] ~extensible:true sigma' in
let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in
let c = nf c in
let j =
@@ -1902,7 +1902,7 @@ let vernac_load interp fname =
let input =
let longfname = Loadpath.locate_file fname in
let in_chan = open_utf8_file_in longfname in
- Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in
+ Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
try while true do interp (snd (parse_sentence input)) done
with End_of_input -> ()
@@ -1923,7 +1923,6 @@ let interp ?proof ?loc locality poly c =
| VernacTime _ -> assert false
| VernacRedirect _ -> assert false
| VernacTimeout _ -> assert false
- | VernacStm _ -> assert false
(* The STM should handle that, but LOAD bypasses the STM... *)
| VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command")
@@ -1950,8 +1949,8 @@ let interp ?proof ?loc locality poly c =
| VernacLocal _ -> assert false
(* Syntax *)
- | VernacSyntaxExtension (local,sl) ->
- vernac_syntax_extension locality local sl
+ | VernacSyntaxExtension (infix, local,sl) ->
+ vernac_syntax_extension locality local infix sl
| VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
| VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
| VernacOpenCloseScope (local, s) -> vernac_open_close_scope locality local s
@@ -2049,7 +2048,7 @@ let interp ?proof ?loc locality poly c =
| VernacSearch (s,g,r) -> vernac_search ?loc s g r
| VernacLocate l -> vernac_locate l
| VernacRegister (id, r) -> vernac_register id r
- | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
+ | VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n")
(* Proof management *)
| VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)]
@@ -2175,7 +2174,7 @@ let with_fail b f =
| HasNotFailed ->
user_err ~hdr:"Fail" (str "The command has not failed!")
| HasFailed msg ->
- if not !Flags.quiet || !test_mode || !ide_slave then Feedback.msg_info
+ if not !Flags.quiet || !Flags.test_mode || !Flags.ide_slave then Feedback.msg_info
(str "The command has indeed failed with message:" ++ fnl () ++ msg)
| _ -> assert false
end
@@ -2184,10 +2183,6 @@ let interp ?(verbosely=true) ?proof (loc,c) =
let orig_program_mode = Flags.is_program_mode () in
let rec aux ?locality ?polymorphism isprogcmd = function
- (* This assert case will be removed when fake_ide can understand
- completion feedback *)
- | VernacStm _ -> assert false (* Done by Stm *)
-
| VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c
| VernacProgram _ -> user_err Pp.(str "Program mode specified twice")
| VernacLocal (b, c) when Option.is_empty locality ->
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index fc11bcf4a..3cff1f14c 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -17,8 +17,7 @@ let rec is_navigation_vernac = function
| VernacResetName _
| VernacBacktrack _
| VernacBackTo _
- | VernacBack _
- | VernacStm _ -> true
+ | VernacBack _ -> true
| VernacRedirect (_, (_,c))
| VernacTime (_,c) ->
is_navigation_vernac c (* Time Back* is harmless *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 04:07:16 +0000