aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.build1
-rw-r--r--intf/vernacexpr.mli15
-rw-r--r--parsing/g_vernac.ml423
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/indfun.ml26
-rw-r--r--plugins/funind/merge.ml2
-rw-r--r--plugins/funind/recdef.ml8
-rw-r--r--pretyping/evd.ml76
-rw-r--r--pretyping/evd.mli9
-rw-r--r--printing/ppvernac.ml32
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--stm/lemmas.ml8
-rw-r--r--stm/stm.ml4
-rw-r--r--stm/texmacspp.ml12
-rw-r--r--stm/vernac_classifier.ml14
-rw-r--r--tactics/elimschemes.ml4
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/rewrite.ml4
-rw-r--r--toplevel/command.ml53
-rw-r--r--toplevel/command.mli6
-rw-r--r--toplevel/obligations.ml2
-rw-r--r--toplevel/record.ml9
-rw-r--r--toplevel/record.mli2
-rw-r--r--toplevel/vernacentries.ml18
24 files changed, 202 insertions, 132 deletions
diff --git a/Makefile.build b/Makefile.build
index 6ceff2de9..0057b7168 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -94,6 +94,7 @@ HIDE := $(if $(VERBOSE),,@)
LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
+CAMLFLAGS:= $(CAMLFLAGS) -w +a-3-4-6-7-9-27-29-32..39-41..42-44-45-48
OCAMLC := $(OCAMLC) $(CAMLFLAGS)
OCAMLOPT := $(OCAMLOPT) $(CAMLFLAGS)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index bb0331fcc..37218fbf9 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -160,6 +160,9 @@ type option_ref_value =
| StringRefValue of string
| QualidRefValue of reference
+(** Identifier and optional list of bound universes. *)
+type plident = lident * lident list option
+
type sort_expr = glob_sort
type definition_expr =
@@ -168,10 +171,10 @@ type definition_expr =
* constr_expr option
type fixpoint_expr =
- Id.t located * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option
+ plident * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option
type cofixpoint_expr =
- Id.t located * local_binder list * constr_expr * constr_expr option
+ plident * local_binder list * constr_expr * constr_expr option
type local_decl_expr =
| AssumExpr of lname * constr_expr
@@ -190,14 +193,14 @@ type constructor_list_or_record_decl_expr =
| Constructors of constructor_expr list
| RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
type inductive_expr =
- lident with_coercion * local_binder list * constr_expr option * inductive_kind *
+ plident with_coercion * local_binder list * constr_expr option * inductive_kind *
constructor_list_or_record_decl_expr
type one_inductive_expr =
- lident * local_binder list * constr_expr option * constructor_expr list
+ plident * local_binder list * constr_expr option * constructor_expr list
type proof_expr =
- lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)
+ plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)
type grammar_tactic_prod_item_expr =
| TacTerm of string
@@ -305,7 +308,7 @@ type vernac_expr =
(* Gallina *)
| VernacDefinition of
- (locality option * definition_object_kind) * lident * definition_expr
+ (locality option * definition_object_kind) * plident * definition_expr
| VernacStartTheoremProof of theorem_kind * proof_expr list * bool
| VernacEndProof of proof_end
| VernacExactProof of constr_expr
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 11f78c708..63850713f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -196,9 +196,9 @@ GEXTEND Gram
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
- [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr;
+ [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr;
l = LIST0
- [ "with"; id = identref; bl = binders; ":"; c = lconstr ->
+ [ "with"; id = pidentref; bl = binders; ":"; c = lconstr ->
(Some id,(bl,c,None)) ] ->
VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false)
| stre = assumption_token; nl = inline; bl = assum_list ->
@@ -206,10 +206,10 @@ GEXTEND Gram
| stre = assumptions_token; nl = inline; bl = assum_list ->
test_plurial_form bl;
VernacAssumption (stre, nl, bl)
- | d = def_token; id = identref; b = def_body ->
+ | d = def_token; id = pidentref; b = def_body ->
VernacDefinition (d, id, b)
| IDENT "Let"; id = identref; b = def_body ->
- VernacDefinition ((Some Discharge, Definition), id, b)
+ VernacDefinition ((Some Discharge, Definition), (id, None), b)
(* Gallina inductive declarations *)
| priv = private_token; f = finite_token;
indl = LIST1 inductive_definition SEP "with" ->
@@ -268,6 +268,9 @@ GEXTEND Gram
| IDENT "Inline" -> DefaultInline
| -> NoInline] ]
;
+ pidentref:
+ [ [ i = identref; l = OPT [ "@{" ; l = LIST1 identref; "}" -> l ] -> (i,l) ] ]
+ ;
univ_constraint:
[ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ];
r = identref -> (l, ord, r) ] ]
@@ -312,7 +315,7 @@ GEXTEND Gram
| -> RecordDecl (None, []) ] ]
;
inductive_definition:
- [ [ oc = opt_coercion; id = identref; indpar = binders;
+ [ [ oc = opt_coercion; id = pidentref; indpar = binders;
c = OPT [ ":"; c = lconstr -> c ];
lc=opt_constructors_or_fields; ntn = decl_notation ->
(((oc,id),indpar,c,lc),ntn) ] ]
@@ -338,14 +341,14 @@ GEXTEND Gram
;
(* (co)-fixpoints *)
rec_definition:
- [ [ id = identref;
+ [ [ id = pidentref;
bl = binders_fixannot;
ty = type_cstr;
def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ]
;
corec_definition:
- [ [ id = identref; bl = binders; ty = type_cstr;
+ [ [ id = pidentref; bl = binders; ty = type_cstr;
def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
((id,bl,ty,def),ntn) ] ]
;
@@ -605,15 +608,15 @@ GEXTEND Gram
d = def_body ->
let s = coerce_reference_to_id qid in
VernacDefinition
- ((Some Global,CanonicalStructure),(Loc.ghost,s),d)
+ ((Some Global,CanonicalStructure),((Loc.ghost,s),None),d)
(* Coercions *)
| IDENT "Coercion"; qid = global; d = def_body ->
let s = coerce_reference_to_id qid in
- VernacDefinition ((None,Coercion),(Loc.ghost,s),d)
+ VernacDefinition ((None,Coercion),((Loc.ghost,s),None),d)
| IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
let s = coerce_reference_to_id qid in
- VernacDefinition ((Some Decl_kinds.Local,Coercion),(Loc.ghost,s),d)
+ VernacDefinition ((Some Decl_kinds.Local,Coercion),((Loc.ghost,s),None),d)
| IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacIdentityCoercion (true, f, s, t)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 065c12a2d..07efaae27 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1395,7 +1395,7 @@ let do_build_inductive
(rel_constructors)
in
let rel_ind i ext_rel_constructors =
- ((Loc.ghost,relnames.(i)),
+ (((Loc.ghost,relnames.(i)), None),
rel_params,
Some rel_arities.(i),
ext_rel_constructors),[]
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 5dcb0c043..d9d059f8f 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -150,7 +150,7 @@ let build_newrecursive
in
let (rec_sign,rec_impls) =
List.fold_left
- (fun (env,impls) ((_,recname),bl,arityc,_) ->
+ (fun (env,impls) (((_,recname),_),bl,arityc,_) ->
let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
let arity,ctx = Constrintern.interp_type env0 sigma arityc in
let evdref = ref (Evd.from_env env0) in
@@ -323,7 +323,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof
(continue_proof : int -> Names.constant array -> Term.constr array -> int ->
Tacmach.tactic) : unit =
- let names = List.map (function ((_, name),_,_,_,_),_ -> name) fix_rec_l in
+ let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in
let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
let funs_args = List.map fst fun_bodies in
let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in
@@ -343,7 +343,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
locate_ind
f_R_mut)
in
- let fname_kn ((fname,_,_,_,_),_) =
+ let fname_kn (((fname,_),_,_,_,_),_) =
let f_ref = Ident fname in
locate_with_msg
(pr_reference f_ref++str ": Not an inductive type!")
@@ -380,15 +380,15 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
match fixpoint_exprl with
- | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
+ | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in
Command.do_definition
fname
- (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition)
+ (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
let evd,rev_pconstants =
List.fold_left
- (fun (evd,l) (((_,fname),_,_,_,_),_) ->
+ (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
let evd,c =
Evd.fresh_global
(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
@@ -402,7 +402,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
let evd,rev_pconstants =
List.fold_left
- (fun (evd,l) (((_,fname),_,_,_,_),_) ->
+ (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
let evd,c =
Evd.fresh_global
(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
@@ -614,7 +614,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
let _is_struct =
match fixpoint_exprl with
| [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] ->
- let ((((_,name),_,args,types,body)),_) as fixpoint_expr =
+ let (((((_,name),pl),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -638,7 +638,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook;
false
|[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] ->
- let ((((_,name),_,args,types,body)),_) as fixpoint_expr =
+ let (((((_,name),_),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -672,7 +672,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
fixpoint_exprl;
let fixpoint_exprl = recompute_binder_list fixpoint_exprl in
let fix_names =
- List.map (function (((_,name),_,_,_,_),_) -> name) fixpoint_exprl
+ List.map (function ((((_,name),_),_,_,_,_),_) -> name) fixpoint_exprl
in
(* ok all the expressions are structural *)
let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
@@ -867,20 +867,20 @@ let make_graph (f_ref:global_reference) =
)
in
let b' = add_args (snd id) new_args b in
- (((id, ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+ ((((id,None), ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
)
fixexprl
in
l
| _ ->
let id = Label.to_id (con_label c) in
- [((Loc.ghost,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
+ [(((Loc.ghost,id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
in
let mp,dp,_ = repr_con c in
do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list;
(* We register the infos *)
List.iter
- (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
+ (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
expr_list);
Dumpglob.continue ()
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ea699580b..69e055c23 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -841,7 +841,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
FIXME: params et cstr_expr (arity) *)
let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
(rawlist:(Id.t * glob_constr) list) =
- let lident = Loc.ghost, shift.ident in
+ let lident = (Loc.ghost, shift.ident), None in
let bindlist , cstr_expr = (* params , arities *)
merge_rec_params_and_arity prms1 prms2 shift mkSet in
let lcstor_expr : (bool * (lident * constr_expr)) list =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d3979748e..9de15e407 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1398,9 +1398,7 @@ let com_terminate
start_proof ctx tclIDTAC tclIDTAC;
try
let sigma, new_goal_type = build_new_goal_type () in
- let sigma =
- Evd.from_env ~ctx:(Evd.evar_universe_context sigma) Environ.empty_env
- in
+ let sigma = Evd.from_ctx (Evd.evar_universe_context sigma) in
open_new_goal start_proof sigma
using_lemmas tcc_lemma_ref
(Some tcc_lemma_name)
@@ -1437,9 +1435,7 @@ let (com_eqn : int -> Id.t ->
| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant")
in
let (evmap, env) = Lemmas.get_current_context() in
- let evmap =
- Evd.from_env ~ctx:(Evd.evar_universe_context evmap) Environ.empty_env
- in
+ let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in
let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
(Lemmas.start_proof eq_name (Global, false, Proof Lemma)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 168a10df9..fc4f5e040 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -277,15 +277,15 @@ end
type evar_universe_context =
{ uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t;
uctx_local : Univ.universe_context_set; (** The local context of variables *)
- uctx_univ_variables : Universes.universe_opt_subst;
- (** The local universes that are unification variables *)
- uctx_univ_algebraic : Univ.universe_set;
- (** The subset of unification variables that
+ uctx_univ_variables : Universes.universe_opt_subst;
+ (** The local universes that are unification variables *)
+ uctx_univ_algebraic : Univ.universe_set;
+ (** The subset of unification variables that
can be instantiated with algebraic universes as they appear in types
and universe instances only. *)
- uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
- uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
- }
+ uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
+ uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
+ }
let empty_evar_universe_context =
{ uctx_names = UNameMap.empty, Univ.LMap.empty;
@@ -769,10 +769,10 @@ let empty = {
extras = Store.empty;
}
-let from_env ?ctx e =
- match ctx with
- | None -> { empty with universes = evar_universe_context_from e }
- | Some ctx -> { empty with universes = ctx }
+let from_env e =
+ { empty with universes = evar_universe_context_from e }
+
+let from_ctx ctx = { empty with universes = ctx }
let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
@@ -982,9 +982,43 @@ let evar_universe_context d = d.universes
let universe_context_set d = d.universes.uctx_local
-let universe_context evd =
- Univ.ContextSet.to_context evd.universes.uctx_local
+let pr_uctx_level uctx =
+ let map, map_rev = uctx.uctx_names in
+ fun l ->
+ try str(Univ.LMap.find l map_rev)
+ with Not_found ->
+ Universes.pr_with_global_universes l
+let universe_context ?names evd =
+ match names with
+ | None -> Univ.ContextSet.to_context evd.universes.uctx_local
+ | Some pl ->
+ let levels = Univ.ContextSet.levels evd.universes.uctx_local in
+ let newinst, left =
+ List.fold_right
+ (fun (loc,id) (newinst, acc) ->
+ let l =
+ try UNameMap.find (Id.to_string id) (fst evd.universes.uctx_names)
+ with Not_found ->
+ user_err_loc (loc, "universe_context",
+ str"Universe " ++ pr_id id ++ str" is not bound anymore.")
+ in (l :: newinst, Univ.LSet.remove l acc))
+ pl ([], levels)
+ in
+ if not (Univ.LSet.is_empty left) then
+ let n = Univ.LSet.cardinal left in
+ errorlabstrm "universe_context"
+ (str(CString.plural n "Universe") ++ spc () ++
+ Univ.LSet.pr (pr_uctx_level evd.universes) left ++
+ spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")
+ else Univ.UContext.make (Univ.Instance.of_array (Array.of_list newinst),
+ Univ.ContextSet.constraints evd.universes.uctx_local)
+
+let restrict_universe_context evd vars =
+ let uctx = evd.universes in
+ let uctx' = Universes.restrict_universe_context uctx.uctx_local vars in
+ { evd with universes = { uctx with uctx_local = uctx' } }
+
let universe_subst evd =
evd.universes.uctx_univ_variables
@@ -1072,6 +1106,15 @@ let make_flexible_variable evd b u =
{evd with universes = {ctx with uctx_univ_variables = uvars';
uctx_univ_algebraic = avars'}}
+let make_evar_universe_context e l =
+ let uctx = evar_universe_context_from e in
+ match l with
+ | None -> uctx
+ | Some us ->
+ List.fold_left (fun uctx (loc,id) ->
+ fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) uctx))
+ uctx us
+
(****************************************)
(* Operations on constants *)
(****************************************)
@@ -1703,13 +1746,6 @@ let evar_dependency_closure n sigma =
let has_no_evar sigma =
EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars
-let pr_uctx_level uctx =
- let map, map_rev = uctx.uctx_names in
- fun l ->
- try str(Univ.LMap.find l map_rev)
- with Not_found ->
- Universes.pr_with_global_universes l
-
let pr_evd_level evd = pr_uctx_level evd.universes
let pr_evar_universe_context ctx =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index f2d8a8335..94d9d5f66 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -129,10 +129,13 @@ type evar_map
val empty : evar_map
(** The empty evar map. *)
-val from_env : ?ctx:evar_universe_context -> env -> evar_map
+val from_env : env -> evar_map
(** The empty evar map with given universe context, taking its initial
universes from env. *)
+val from_ctx : evar_universe_context -> evar_map
+(** The empty evar map with given universe context *)
+
val is_empty : evar_map -> bool
(** Whether an evarmap is empty. *)
@@ -484,6 +487,8 @@ val union_evar_universe_context : evar_universe_context -> evar_universe_context
evar_universe_context
val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst
+val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context
+val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map
(** Raises Not_found if not a name for a universe in this map. *)
val universe_of_name : evar_map -> string -> Univ.universe_level
val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map
@@ -527,7 +532,7 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool
val evar_universe_context : evar_map -> evar_universe_context
val universe_context_set : evar_map -> Univ.universe_context_set
-val universe_context : evar_map -> Univ.universe_context
+val universe_context : ?names:(Id.t located) list -> evar_map -> Univ.universe_context
val universe_subst : evar_map -> Universes.universe_opt_subst
val universes : evar_map -> Univ.universes
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 4e889e55f..71dcd15cc 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -43,6 +43,12 @@ module Make
else
pr_id id
+ let pr_plident (lid, l) =
+ pr_lident lid ++
+ (match l with
+ | Some l -> prlist_with_sep spc pr_lident l
+ | None -> mt())
+
let string_of_fqid fqid =
String.concat "." (List.map Id.to_string fqid)
@@ -387,10 +393,16 @@ module Make
hov 0 (prlist_with_sep sep pr_production_item pil ++
spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
- let pr_statement head (id,(bl,c,guard)) =
- assert (not (Option.is_empty id));
+ let pr_univs pl =
+ match pl with
+ | None -> mt ()
+ | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}"
+
+ let pr_statement head (idpl,(bl,c,guard)) =
+ assert (not (Option.is_empty idpl));
+ let id, pl = Option.get idpl in
hov 2
- (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++
+ (head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++
(match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
str":" ++ pr_spc_lconstr c)
@@ -729,7 +741,7 @@ module Make
return (
hov 2 (
pr_def_token d ++ spc()
- ++ pr_lident id ++ binds ++ typ
+ ++ pr_plident id ++ binds ++ typ
++ (match c with
| None -> mt()
| Some cc -> str" :=" ++ spc() ++ cc))
@@ -781,10 +793,10 @@ module Make
| RecordDecl (c,fs) ->
pr_record_decl b c fs
in
- let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
+ let pr_oneind key (((coe,(id,pl)),indpar,s,k,lc),ntn) =
hov 0 (
str key ++ spc() ++
- (if coe then str"> " else str"") ++ pr_lident id ++
+ (if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++
pr_and_type_binders_arg indpar ++ spc() ++
Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
str" :=") ++ pr_constructor_list k lc ++
@@ -808,9 +820,9 @@ module Make
| None | Some Global -> ""
in
let pr_onerec = function
- | ((loc,id),ro,bl,type_,def),ntn ->
+ | (((loc,id),pl),ro,bl,type_,def),ntn ->
let annot = pr_guard_annot pr_lconstr_expr bl ro in
- pr_id id ++ pr_binders_arg bl ++ annot
+ pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot
++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
prlist (pr_decl_notation pr_constr) ntn
@@ -826,8 +838,8 @@ module Make
| Some Local -> keyword "Local" ++ spc ()
| None | Some Global -> str ""
in
- let pr_onecorec (((loc,id),bl,c,def),ntn) =
- pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
+ let pr_onecorec ((((loc,id),pl),bl,c,def),ntn) =
+ pr_id id ++ pr_univs pl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
spc() ++ pr_lconstr_expr c ++
pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
prlist (pr_decl_notation pr_constr) ntn
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d024c01ba..c77ab06b9 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -133,7 +133,7 @@ open Decl_kinds
let next = let n = ref 0 in fun () -> incr n; !n
let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
- let evd = Evd.from_env ~ctx Environ.empty_env in
+ let evd = Evd.from_ctx ctx in
start_proof id goal_kind evd sign typ (fun _ -> ());
try
let status = by tac in
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index a7ef96c66..7679b1a66 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -212,7 +212,7 @@ let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
let default_thm_id = Id.of_string "Unnamed_thm"
let compute_proof_name locality = function
- | Some (loc,id) ->
+ | Some ((loc,id),pl) ->
(* We check existence here: it's a bit late at Qed time *)
if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
@@ -431,7 +431,11 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
let start_proof_com kind thms hook =
let env0 = Global.env () in
- let evdref = ref (Evd.from_env env0) 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 thms = List.map (fun (sopt,(bl,t,guard)) ->
let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
let t', imps' = interp_type_evars_impls ~impls env evdref t in
diff --git a/stm/stm.ml b/stm/stm.ml
index e6271f608..4a303f036 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -424,8 +424,8 @@ end = struct (* {{{ *)
let reachable id = reachable !vcs id
let mk_branch_name { expr = x } = Branch.make
(match x with
- | VernacDefinition (_,(_,i),_) -> string_of_id i
- | VernacStartTheoremProof (_,[Some (_,i),_],_) -> string_of_id i
+ | VernacDefinition (_,((_,i),_),_) -> string_of_id i
+ | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> string_of_id i
| _ -> "branch")
let edit_branch = Branch.make "edit"
let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index aaa6c2c07..fb41bb7be 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -244,7 +244,7 @@ and pp_local_decl_expr lde = (* don't know what it is for now *)
match lde with
| AssumExpr (_, ce) -> pp_expr ce
| DefExpr (_, ce, _) -> pp_expr ce
-and pp_inductive_expr ((_, (l, id)), lbl, ceo, _, cl_or_rdexpr) =
+and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
(* inductive_expr *)
let b,e = Loc.unloc l in
let location = ["begin", string_of_int b; "end", string_of_int e] in
@@ -273,7 +273,7 @@ and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
| CMeasureRec (e, None) -> "mesrec", [pp_expr e]
| CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
Element ("recursion_order", ["kind", kind] @ attrs, expr)
-and pp_fixpoint_expr ((loc, id), (optid, roe), lbl, ce, ceo) =
+and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
(* fixpoint_expr *)
let start, stop = unlock loc in
let id = Id.to_string id in
@@ -286,7 +286,7 @@ and pp_fixpoint_expr ((loc, id), (optid, roe), lbl, ce, ceo) =
| Some ce -> [pp_expr ce]
| None -> []
end
-and pp_cofixpoint_expr ((loc, id), lbl, ce, ceo) = (* cofixpoint_expr *)
+and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
(* Nota: it is like fixpoint_expr without (optid, roe)
* so could be merged if there is no more differences *)
let start, stop = unlock loc in
@@ -473,7 +473,7 @@ and pp_expr ?(attr=[]) e =
xmlApply loc
(xmlOperator "fix" loc ::
List.flatten (List.map
- (fun (a,b,cl,c,d) -> pp_fixpoint_expr (a,b,cl,c,Some d))
+ (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
fel))
let pp_comment (c) =
@@ -540,7 +540,7 @@ let rec tmpp v loc =
| VernacConstraint _
| VernacPolymorphic (_, _) as x -> xmlTODO loc x
(* Gallina *)
- | VernacDefinition (ldk, (_,id), de) ->
+ | VernacDefinition (ldk, ((_,id),_), de) ->
let l, dk =
match ldk with
| Some l, dk -> (l, dk)
@@ -555,7 +555,7 @@ let rec tmpp v loc =
let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
let str_id = Id.to_string id in
(xmlDef str_dk str_id loc [pp_expr e])
- | VernacStartTheoremProof (tk, [ Some (_,id), ([], statement, None) ], b) ->
+ | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
let str_tk = Kindops.string_of_theorem_kind tk in
let str_id = Id.to_string id in
(xmlThm str_tk str_id loc [pp_expr statement])
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 2b5eb8683..a2b779516 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -116,25 +116,25 @@ let rec classify_vernac e =
| VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
(* StartProof *)
| VernacDefinition (
- (Some Decl_kinds.Discharge,Decl_kinds.Definition),(_,i),ProveBody _) ->
+ (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) ->
VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater
- | VernacDefinition (_,(_,i),ProveBody _) ->
+ | VernacDefinition (_,((_,i),_),ProveBody _) ->
VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
| VernacStartTheoremProof (_,l,_) ->
let ids =
- CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
+ CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
| VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
| VernacFixpoint (_,l) ->
let ids, open_proof =
- List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) ->
+ List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
else VtSideff ids, VtLater
| VernacCoFixpoint (_,l) ->
let ids, open_proof =
- List.fold_left (fun (l,b) (((_,id),_,_,p),_) ->
+ List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
@@ -143,9 +143,9 @@ let rec classify_vernac e =
| VernacAssumption (_,_,l) ->
let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in
VtSideff ids, VtLater
- | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater
+ | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater
| VernacInductive (_,_,l) ->
- let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with
+ let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with
| Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
| RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
CList.map_filter (function
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 749e0d2b5..e1c9c2de5 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -51,7 +51,7 @@ let optimize_non_type_induction_scheme kind dep sort ind =
let u = Univ.UContext.instance ctx in
let ctxset = Univ.ContextSet.of_context ctx in
let ectx = Evd.evar_universe_context_of ctxset in
- let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ectx env) (ind,u) dep sort in
+ let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
(c, Evd.evar_universe_context sigma), Declareops.no_seff
let build_induction_scheme_in_type dep sort ind =
@@ -63,7 +63,7 @@ let build_induction_scheme_in_type dep sort ind =
let u = Univ.UContext.instance ctx in
let ctxset = Univ.ContextSet.of_context ctx in
let ectx = Evd.evar_universe_context_of ctxset in
- let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ectx env) (ind,u) dep sort in
+ let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
c, Evd.evar_universe_context sigma
let rect_scheme_kind_from_type =
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 9a64b03fd..efd6ded44 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -194,7 +194,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
errorlabstrm "lemma_inversion"
(str"Computed inversion goal was not closed in initial signature.");
*)
- let pf = Proof.start (Evd.from_env ~ctx:(evar_universe_context sigma) invEnv) [invEnv,invGoal] in
+ let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
let pf =
fst (Proof.run_tactic env (
tclTHEN intro (onLastHypId inv_op)) pf)
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 719cc7c98..aa057a3e8 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1824,8 +1824,8 @@ let declare_projection n instance_id r =
let build_morphism_signature m =
let env = Global.env () in
- let m,ctx = Constrintern.interp_constr env Evd.empty m in
- let sigma = Evd.from_env ~ctx env in
+ let m,ctx = Constrintern.interp_constr env (Evd.from_env env) m in
+ let sigma = Evd.from_ctx ctx in
let t = Typing.unsafe_type_of env sigma m in
let cstrs =
let rec aux t =
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 04238da2b..e2e5d8704 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -77,9 +77,10 @@ let red_constant_entry n ce = function
(under_binders env
(fst (reduction_of_red_expr env red)) n body,ctx),eff) }
-let interp_definition bl p red_option c ctypopt =
+let interp_definition pl bl p red_option c ctypopt =
let env = Global.env() in
- let evdref = ref (Evd.from_env env) in
+ let ctx = Evd.make_evar_universe_context env pl in
+ let evdref = ref (Evd.from_ctx ctx) in
let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
let nb_args = List.length ctx in
let imps,ce =
@@ -92,10 +93,10 @@ let interp_definition bl p red_option c ctypopt =
let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
let body = nf (it_mkLambda_or_LetIn c ctx) in
let vars = Universes.universes_of_constr body in
- let ctx = Universes.restrict_universe_context
- (Evd.universe_context_set !evdref) vars in
+ let evd = Evd.restrict_universe_context !evdref vars in
+ let uctx = Evd.universe_context ?names:pl evd in
imps1@(Impargs.lift_implicits nb_args imps2),
- definition_entry ~univs:(Univ.ContextSet.to_context ctx) ~poly:p body
+ definition_entry ~univs:uctx ~poly:p body
| Some ctyp ->
let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
let subst = evd_comb0 Evd.nf_univ_variables evdref in
@@ -118,11 +119,11 @@ let interp_definition bl p red_option c ctypopt =
strbrk "The term declares more implicits than the type here.");
let vars = Univ.LSet.union (Universes.universes_of_constr body)
(Universes.universes_of_constr typ) in
- let ctx = Universes.restrict_universe_context
- (Evd.universe_context_set !evdref) vars in
+ let ctx = Evd.restrict_universe_context !evdref vars in
+ let uctx = Evd.universe_context ?names:pl ctx in
imps1@(Impargs.lift_implicits nb_args impsty),
definition_entry ~types:typ ~poly:p
- ~univs:(Univ.ContextSet.to_context ctx) body
+ ~univs:uctx body
in
red_constant_entry (rel_context_length ctx) ce red_option, !evdref, imps
@@ -172,8 +173,8 @@ let declare_definition ident (local, p, k) ce imps hook =
let _ = Obligations.declare_definition_ref := declare_definition
-let do_definition ident k bl red_option c ctypopt hook =
- let (ce, evd, imps as def) = interp_definition bl (pi2 k) red_option c ctypopt in
+let do_definition ident k pl bl red_option c ctypopt hook =
+ let (ce, evd, imps as def) = interp_definition pl bl (pi2 k) red_option c ctypopt in
if Flags.is_program_mode () then
let env = Global.env () in
let (c,ctx), sideff = Future.force ce.const_entry_body in
@@ -290,6 +291,7 @@ let push_types env idl tl =
type structured_one_inductive_expr = {
ind_name : Id.t;
+ ind_univs : lident list option;
ind_arity : constr_expr;
ind_lc : (Id.t * constr_expr) list
}
@@ -499,7 +501,8 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
interp_context_evars env0 evdref paramsl
in
let indnames = List.map (fun ind -> ind.ind_name) indl in
-
+ let pl = (List.hd indl).ind_univs in
+
(* Names of parameters as arguments of the inductive type (defs removed) *)
let assums = List.filter(fun (_,b,_) -> Option.is_empty b) ctx_params in
let params = List.map (fun (na,_,_) -> out_name na) assums in
@@ -541,6 +544,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
let ctx_params = map_rel_context nf ctx_params in
let evd = !evdref in
+ let uctx = Evd.universe_context ?names:pl evd in
List.iter (check_evars env_params Evd.empty evd) arities;
iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;
List.iter (fun (_,ctyps,_) ->
@@ -568,7 +572,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
mind_entry_inds = entries;
mind_entry_polymorphic = poly;
mind_entry_private = if prv then Some false else None;
- mind_entry_universes = Evd.universe_context evd },
+ mind_entry_universes = uctx },
impls
(* Very syntactical equality *)
@@ -590,8 +594,8 @@ let extract_params indl =
params
let extract_inductive indl =
- List.map (fun ((_,indname),_,ar,lc) -> {
- ind_name = indname;
+ List.map (fun (((_,indname),pl),_,ar,lc) -> {
+ ind_name = indname; ind_univs = pl;
ind_arity = Option.cata (fun x -> x) (CSort (Loc.ghost,GType [])) ar;
ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
}) indl
@@ -739,6 +743,7 @@ let check_mutuality env isfix fixl =
type structured_fixpoint_expr = {
fix_name : Id.t;
+ fix_univs : lident list option;
fix_annot : Id.t Loc.located option;
fix_binders : local_binder list;
fix_body : constr_expr option;
@@ -1066,7 +1071,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
let init_tac =
Option.map (List.map Proofview.V82.tactic) init_tac
in
- let evd = Evd.from_env ~ctx Environ.empty_env 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 _ _ -> ()))
else begin
@@ -1102,8 +1107,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns
let init_tac =
Option.map (List.map Proofview.V82.tactic) init_tac
in
- let evd = Evd.from_env ~ctx Environ.empty_env in
- Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
+ 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 _ _ -> ()))
else begin
(* We shortcut the proof process *)
@@ -1130,15 +1135,17 @@ let extract_decreasing_argument limit = function
let extract_fixpoint_components limit l =
let fixl, ntnl = List.split l in
- let fixl = List.map (fun ((_,id),ann,bl,typ,def) ->
+ let fixl = List.map (fun (((_,id),pl),ann,bl,typ,def) ->
let ann = extract_decreasing_argument limit ann in
- {fix_name = id; fix_annot = ann; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
+ {fix_name = id; fix_annot = ann; fix_univs = pl;
+ fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
fixl, List.flatten ntnl
let extract_cofixpoint_components l =
let fixl, ntnl = List.split l in
- List.map (fun ((_,id),bl,typ,def) ->
- {fix_name = id; fix_annot = None; fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
+ List.map (fun (((_,id),pl),bl,typ,def) ->
+ {fix_name = id; fix_annot = None; fix_univs = pl;
+ fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
List.flatten ntnl
let out_def = function
@@ -1191,7 +1198,7 @@ let do_program_recursive local p fixkind fixl ntns =
let do_program_fixpoint local poly l =
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
match g, l with
- | [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
+ | [(n, CWfRec r)], [((((_,id),_),_,bl,typ,def),ntn)] ->
let recarg =
match n with
| Some n -> mkIdentC (snd n)
@@ -1200,7 +1207,7 @@ let do_program_fixpoint local poly l =
(str "Recursive argument required for well-founded fixpoints")
in build_wellfounded (id, n, bl, typ, out_def def) r recarg ntn
- | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
+ | [(n, CMeasureRec (m, r))], [((((_,id),_),_,bl,typ,def),ntn)] ->
build_wellfounded (id, n, bl, typ, out_def def)
(Option.default (CRef (lt_ref,None)) r) m ntn
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 3a38e52ce..f4d43ec53 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -31,14 +31,14 @@ val get_declare_definition_hook : unit -> (definition_entry -> unit)
(** {6 Definitions/Let} *)
val interp_definition :
- local_binder list -> polymorphic -> red_expr option -> constr_expr ->
+ lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr ->
constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
val declare_definition : Id.t -> definition_kind ->
definition_entry -> Impargs.manual_implicits ->
Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
-val do_definition : Id.t -> definition_kind ->
+val do_definition : Id.t -> definition_kind -> lident list option ->
local_binder list -> red_expr option -> constr_expr ->
constr_expr option -> unit Lemmas.declaration_hook -> unit
@@ -70,6 +70,7 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
type structured_one_inductive_expr = {
ind_name : Id.t;
+ ind_univs : lident list option;
ind_arity : constr_expr;
ind_lc : (Id.t * constr_expr) list
}
@@ -109,6 +110,7 @@ val do_mutual_inductive :
type structured_fixpoint_expr = {
fix_name : Id.t;
+ fix_univs : lident list option;
fix_annot : Id.t Loc.located option;
fix_binders : local_binder list;
fix_body : constr_expr option;
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 11857b572..3c0977784 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -847,7 +847,7 @@ let rec solve_obligation prg num tac =
in
let obl = subst_deps_obl obls obl in
let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
- let evd = Evd.from_env ~ctx:prg.prg_ctx Environ.empty_env in
+ let evd = Evd.from_ctx prg.prg_ctx in
let auto n tac oblset = auto_solve_obligations n ~oblset tac in
let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
let () = Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type hook in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 15ad18d9c..484fd081d 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -90,9 +90,10 @@ let binder_of_decl = function
let binders_of_decls = List.map binder_of_decl
-let typecheck_params_and_fields def id t ps nots fs =
+let typecheck_params_and_fields def id pl t ps nots fs =
let env0 = Global.env () in
- let evars = ref (Evd.from_env env0) in
+ let ctx = Evd.make_evar_universe_context env0 pl in
+ let evars = ref (Evd.from_ctx ctx) in
let _ =
let error bk (loc, name) =
match bk, name with
@@ -502,7 +503,7 @@ open Vernacexpr
(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
list telling if the corresponding fields must me declared as coercions
or subinstances *)
-let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
+let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
let cfs,notations = List.split cfs in
let cfs,priorities = List.split cfs in
let coers,fs = List.split cfs in
@@ -519,7 +520,7 @@ let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild
(* Now, younger decl in params and fields is on top *)
let ctx, arity, template, implpars, params, implfs, fields =
States.with_state_protection (fun () ->
- typecheck_params_and_fields (kind = Class true) idstruc s ps notations fs) () in
+ typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in
let sign = structure_signature (fields@params) in
match kind with
| Class def ->
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 91dccb96e..eccb5d29d 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -38,7 +38,7 @@ val declare_structure : Decl_kinds.recursivity_kind ->
inductive
val definition_structure :
- inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * lident with_coercion * local_binder list *
+ inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * plident with_coercion * local_binder list *
(local_decl_expr with_instance with_priority with_notation) list *
Id.t * constr_expr option -> global_reference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index cfbdaccec..8efcccaaa 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -461,7 +461,7 @@ let vernac_definition_hook p = function
| SubClass -> Class.add_subclass_hook p
| _ -> no_hook
-let vernac_definition locality p (local,k) (loc,id as lid) def =
+let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
let local = enforce_locality_exp locality local in
let hook = vernac_definition_hook p k in
let () = match local with
@@ -471,20 +471,20 @@ let vernac_definition locality p (local,k) (loc,id as lid) def =
(match def with
| ProveBody (bl,t) -> (* local binders, typ *)
start_proof_and_print (local,p,DefinitionBody Definition)
- [Some lid, (bl,t,None)] no_hook
+ [Some (lid,pl), (bl,t,None)] no_hook
| DefineBody (bl,red_option,c,typ_opt) ->
let red_option = match red_option with
| None -> None
| Some r ->
let (evc,env)= get_current_context () in
Some (snd (interp_redexp env evc r)) in
- do_definition id (local,p,k) bl red_option c typ_opt hook)
+ do_definition id (local,p,k) pl bl red_option c typ_opt hook)
let vernac_start_proof p kind l lettop =
if Dumpglob.dump () then
List.iter (fun (id, _) ->
match id with
- | Some lid -> Dumpglob.dump_definition lid false "prf"
+ | Some (lid,_) -> Dumpglob.dump_definition lid false "prf"
| None -> ()) l;
if not(refining ()) then
if lettop then
@@ -525,11 +525,11 @@ let vernac_assumption locality poly (local, kind) l nl =
let vernac_record k poly finite struc binders sort nameopt cfs =
let const = match nameopt with
- | None -> add_prefix "Build_" (snd (snd struc))
+ | None -> add_prefix "Build_" (snd (fst (snd struc)))
| Some (_,id as lid) ->
Dumpglob.dump_definition lid false "constr"; id in
if Dumpglob.dump () then (
- Dumpglob.dump_definition (snd struc) false "rec";
+ Dumpglob.dump_definition (fst (snd struc)) false "rec";
List.iter (fun (((_, x), _), _) ->
match x with
| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
@@ -538,7 +538,7 @@ let vernac_record k poly finite struc binders sort nameopt cfs =
let vernac_inductive poly lo finite indl =
if Dumpglob.dump () then
- List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
+ List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
match cstrs with
| Constructors cstrs ->
Dumpglob.dump_definition lid false "ind";
@@ -578,13 +578,13 @@ let vernac_inductive poly lo finite indl =
let vernac_fixpoint locality poly local l =
let local = enforce_locality_exp locality local in
if Dumpglob.dump () then
- List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
+ List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
do_fixpoint local poly l
let vernac_cofixpoint locality poly local l =
let local = enforce_locality_exp locality local in
if Dumpglob.dump () then
- List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
+ List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
do_cofixpoint local poly l
let vernac_scheme l =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 18:03:45 +0000