aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml4
-rw-r--r--vernac/auto_ind_decl.ml139
-rw-r--r--vernac/class.ml9
-rw-r--r--vernac/classes.ml14
-rw-r--r--vernac/comAssumption.ml5
-rw-r--r--vernac/comDefinition.ml40
-rw-r--r--vernac/comFixpoint.ml35
-rw-r--r--vernac/comFixpoint.mli4
-rw-r--r--vernac/comInductive.ml45
-rw-r--r--vernac/comInductive.mli1
-rw-r--r--vernac/comProgramFixpoint.ml38
-rw-r--r--vernac/declareDef.ml14
-rw-r--r--vernac/declareDef.mli28
-rw-r--r--vernac/explainErr.ml4
-rw-r--r--vernac/g_vernac.mlg7
-rw-r--r--vernac/himsg.ml108
-rw-r--r--vernac/himsg.mli2
-rw-r--r--vernac/indschemes.ml16
-rw-r--r--vernac/lemmas.ml58
-rw-r--r--vernac/lemmas.mli38
-rw-r--r--vernac/obligations.ml78
-rw-r--r--vernac/obligations.mli29
-rw-r--r--vernac/ppvernac.ml129
-rw-r--r--vernac/record.ml71
-rw-r--r--vernac/topfmt.ml4
-rw-r--r--vernac/vernacentries.ml81
-rw-r--r--vernac/vernacentries.mli4
-rw-r--r--vernac/vernacexpr.ml12
-rw-r--r--vernac/vernacextend.ml4
-rw-r--r--vernac/vernacextend.mli2
30 files changed, 565 insertions, 458 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index b5cc74b594..445f10ecc1 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -21,6 +21,7 @@ open CErrors
open Util
open Names
open Constr
+open Context
open Declarations
open Mod_subst
open Globnames
@@ -238,8 +239,9 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
Array.fold_left (fun accu oib ->
let pspecif = Univ.in_punivs (mib, oib) in
let ind_type = Inductive.type_of_inductive global_env pspecif in
+ let indr = oib.mind_relevance in
let ind_name = Name oib.mind_typename in
- Context.Rel.add (Context.Rel.Declaration.LocalAssum (ind_name, ind_type)) accu)
+ Context.Rel.add (Context.Rel.Declaration.LocalAssum (make_annot ind_name indr, ind_type)) accu)
Context.Rel.empty mib.mind_packets
in
(* For each inductive, collects references in their arity and in the type
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 868a6ed3e9..528829f3a5 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -16,6 +16,7 @@ open Util
open Pp
open Term
open Constr
+open Context
open Vars
open Termops
open Declarations
@@ -144,7 +145,7 @@ let build_beq_scheme mode kn =
in
(* construct the "fun A B ... N, eqA eqB eqC ... N => fixpoint" part *)
let create_input c =
- let myArrow u v = mkArrow u (lift 1 v)
+ let myArrow u v = mkArrow u Sorts.Relevant (lift 1 v)
and eqName = function
| Name s -> Id.of_string ("eq_"^(Id.to_string s))
| Anonymous -> Id.of_string "eq_A"
@@ -161,14 +162,16 @@ let build_beq_scheme mode kn =
( fun a b decl -> (* mkLambda(n,b,a) ) *)
(* here I leave the Naming thingy so that the type of
the function is more readable for the user *)
- mkNamedLambda (eqName (RelDecl.get_name decl)) b a )
+ mkNamedLambda (map_annot eqName (RelDecl.get_annot decl)) b a )
c (List.rev eqs_typ) lnamesparrec
in
List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *)
- (* Same here , hoping the auto renaming will do something good ;) *)
- mkNamedLambda
- (match RelDecl.get_name decl with Name s -> s | Anonymous -> Id.of_string "A")
- (RelDecl.get_type decl) a) eq_input lnamesparrec
+ (* Same here , hoping the auto renaming will do something good ;) *)
+ let x = map_annot
+ (function Name s -> s | Anonymous -> Id.of_string "A")
+ (RelDecl.get_annot decl)
+ in
+ mkNamedLambda x (RelDecl.get_type decl) a) eq_input lnamesparrec
in
let make_one_eq cur =
let u = Univ.Instance.empty in
@@ -251,8 +254,8 @@ let build_beq_scheme mode kn =
in
(* construct the predicate for the Case part*)
let do_predicate rel_list n =
- List.fold_left (fun a b -> mkLambda(Anonymous,b,a))
- (mkLambda (Anonymous,
+ List.fold_left (fun a b -> mkLambda(make_annot Anonymous Sorts.Relevant,b,a))
+ (mkLambda (make_annot Anonymous Sorts.Relevant,
mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1),
(bb ())))
(List.rev rettyp_l) in
@@ -260,7 +263,8 @@ let build_beq_scheme mode kn =
(* do the [| C1 ... => match Y with ... end
...
Cn => match Y with ... end |] part *)
- let ci = make_case_info env (fst ind) MatchStyle in
+ let rci = Sorts.Relevant in (* TODO relevance *)
+ let ci = make_case_info env (fst ind) rci MatchStyle in
let constrs n = get_constructors env (make_ind_family (ind,
Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt)) in
let constrsi = constrs (3+nparrec) in
@@ -296,32 +300,32 @@ let build_beq_scheme mode kn =
(Array.sub eqs 1 (nb_cstr_args - 1))
)
in
- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) cc
+ (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) cc
(constrsj.(j).cs_args)
)
else ar2.(j) <- (List.fold_left (fun a decl ->
- mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (ff ()) (constrsj.(j).cs_args) )
- done;
+ mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) (ff ()) (constrsj.(j).cs_args) )
+ done;
- ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a))
+ ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a))
(mkCase (ci,do_predicate rel_list nb_cstr_args,
mkVar (Id.of_string "Y") ,ar2))
(constrsi.(i).cs_args))
- done;
- mkNamedLambda (Id.of_string "X") (mkFullInd ind (nb_ind-1+1)) (
- mkNamedLambda (Id.of_string "Y") (mkFullInd ind (nb_ind-1+2)) (
+ done;
+ mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1)) (
+ mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2)) (
mkCase (ci, do_predicate rel_list 0,mkVar (Id.of_string "X"),ar))),
!eff
in (* build_beq_scheme *)
- let names = Array.make nb_ind Anonymous and
+ let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
types = Array.make nb_ind mkSet and
cores = Array.make nb_ind mkSet in
let eff = ref Safe_typing.empty_private_constants in
let u = Univ.Instance.empty in
for i=0 to (nb_ind-1) do
- names.(i) <- Name (Id.of_string (rec_name i));
- types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0)
- (mkArrow (mkFullInd ((kn,i),u) 1) (bb ()));
+ names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant;
+ types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0) Sorts.Relevant
+ (mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ()));
let c, eff' = make_one_eq i in
cores.(i) <- c;
eff := Safe_typing.concat_private eff' !eff
@@ -562,34 +566,39 @@ let compute_bl_goal ind lnamesparrec nparrec =
let x = next_ident_away (Id.of_string "x") avoid and
y = next_ident_away (Id.of_string "y") avoid in
let bl_typ = List.map (fun (s,seq,_,_) ->
- mkNamedProd x (mkVar s) (
- mkNamedProd y (mkVar s) (
+ mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) (
+ mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) (
mkArrow
( mkApp(eq (),[|bb (); mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt () |]))
+ Sorts.Relevant
( mkApp(eq (),[|mkVar s;mkVar x;mkVar y|]))
))
) list_id in
let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b ->
- mkNamedProd sbl b a
+ mkNamedProd (make_annot sbl Sorts.Relevant) b a
) c (List.rev list_id) (List.rev bl_typ) in
let eqs_typ = List.map (fun (s,_,_,_) ->
- mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,(bb ())))
+ mkProd(make_annot Anonymous Sorts.Relevant,mkVar s,mkProd(make_annot Anonymous Sorts.Relevant,mkVar s,(bb ())))
) list_id in
let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
- mkNamedProd seq b a
+ mkNamedProd (make_annot seq Sorts.Relevant) b a
) bl_input (List.rev list_id) (List.rev eqs_typ) in
- List.fold_left (fun a decl -> mkNamedProd
- (match RelDecl.get_name decl with Name s -> s | Anonymous -> next_ident_away (Id.of_string "A") avoid)
- (RelDecl.get_type decl) a) eq_input lnamesparrec
+ List.fold_left (fun a decl ->
+ let x = map_annot
+ (function Name s -> s | Anonymous -> next_ident_away (Id.of_string "A") avoid)
+ (RelDecl.get_annot decl)
+ in
+ mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec
in
let n = next_ident_away (Id.of_string "x") avoid and
m = next_ident_away (Id.of_string "y") avoid in
let u = Univ.Instance.empty in
create_input (
- mkNamedProd n (mkFullInd (ind,u) nparrec) (
- mkNamedProd m (mkFullInd (ind,u) (nparrec+1)) (
+ mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd (ind,u) nparrec) (
+ mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) (
mkArrow
(mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar n;mkVar m|]);tt ()|]))
+ Sorts.Relevant
(mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
))), eff
@@ -706,34 +715,40 @@ let compute_lb_goal ind lnamesparrec nparrec =
let x = next_ident_away (Id.of_string "x") avoid and
y = next_ident_away (Id.of_string "y") avoid in
let lb_typ = List.map (fun (s,seq,_,_) ->
- mkNamedProd x (mkVar s) (
- mkNamedProd y (mkVar s) (
+ mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) (
+ mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) (
mkArrow
- ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
- ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
+ ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
+ Sorts.Relevant
+ ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
))
) list_id in
let lb_input = List.fold_left2 ( fun a (s,_,_,slb) b ->
- mkNamedProd slb b a
+ mkNamedProd (make_annot slb Sorts.Relevant) b a
) c (List.rev list_id) (List.rev lb_typ) in
let eqs_typ = List.map (fun (s,_,_,_) ->
- mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb))
+ mkProd(make_annot Anonymous Sorts.Relevant,mkVar s,
+ mkProd(make_annot Anonymous Sorts.Relevant,mkVar s,bb))
) list_id in
let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
- mkNamedProd seq b a
+ mkNamedProd (make_annot seq Sorts.Relevant) b a
) lb_input (List.rev list_id) (List.rev eqs_typ) in
- List.fold_left (fun a decl -> mkNamedProd
- (match (RelDecl.get_name decl) with Name s -> s | Anonymous -> Id.of_string "A")
- (RelDecl.get_type decl) a) eq_input lnamesparrec
+ List.fold_left (fun a decl ->
+ let x = map_annot
+ (function Name s -> s | Anonymous -> Id.of_string "A")
+ (RelDecl.get_annot decl)
+ in
+ mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec
in
let n = next_ident_away (Id.of_string "x") avoid and
m = next_ident_away (Id.of_string "y") avoid in
let u = Univ.Instance.empty in
create_input (
- mkNamedProd n (mkFullInd (ind,u) nparrec) (
- mkNamedProd m (mkFullInd (ind,u) (nparrec+1)) (
+ mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd (ind,u) nparrec) (
+ mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) (
mkArrow
(mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar n;mkVar m|]))
+ Sorts.Relevant
(mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
))), eff
@@ -835,45 +850,51 @@ let compute_dec_goal ind lnamesparrec nparrec =
let x = next_ident_away (Id.of_string "x") avoid and
y = next_ident_away (Id.of_string "y") avoid in
let lb_typ = List.map (fun (s,seq,_,_) ->
- mkNamedProd x (mkVar s) (
- mkNamedProd y (mkVar s) (
+ mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) (
+ mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) (
mkArrow
- ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
- ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
+ ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
+ Sorts.Relevant
+ ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
))
) list_id in
let bl_typ = List.map (fun (s,seq,_,_) ->
- mkNamedProd x (mkVar s) (
- mkNamedProd y (mkVar s) (
+ mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) (
+ mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) (
mkArrow
- ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
- ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
+ ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
+ Sorts.Relevant
+ ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
))
) list_id in
let lb_input = List.fold_left2 ( fun a (s,_,_,slb) b ->
- mkNamedProd slb b a
+ mkNamedProd (make_annot slb Sorts.Relevant) b a
) c (List.rev list_id) (List.rev lb_typ) in
let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b ->
- mkNamedProd sbl b a
+ mkNamedProd (make_annot sbl Sorts.Relevant) b a
) lb_input (List.rev list_id) (List.rev bl_typ) in
let eqs_typ = List.map (fun (s,_,_,_) ->
- mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb))
+ mkProd(make_annot Anonymous Sorts.Relevant,mkVar s,
+ mkProd(make_annot Anonymous Sorts.Relevant,mkVar s,bb))
) list_id in
let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
- mkNamedProd seq b a
+ mkNamedProd (make_annot seq Sorts.Relevant) b a
) bl_input (List.rev list_id) (List.rev eqs_typ) in
- List.fold_left (fun a decl -> mkNamedProd
- (match RelDecl.get_name decl with Name s -> s | Anonymous -> Id.of_string "A")
- (RelDecl.get_type decl) a) eq_input lnamesparrec
+ List.fold_left (fun a decl ->
+ let x = map_annot
+ (function Name s -> s | Anonymous -> Id.of_string "A")
+ (RelDecl.get_annot decl)
+ in
+ mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec
in
let n = next_ident_away (Id.of_string "x") avoid and
m = next_ident_away (Id.of_string "y") avoid in
let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar n;mkVar m|]) in
create_input (
- mkNamedProd n (mkFullInd ind (2*nparrec)) (
- mkNamedProd m (mkFullInd ind (2*nparrec+1)) (
+ mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd ind (2*nparrec)) (
+ mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd ind (2*nparrec+1)) (
mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|])
)
)
diff --git a/vernac/class.ml b/vernac/class.ml
index 823177d4d1..0837beccee 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -14,6 +14,7 @@ open Pp
open Names
open Term
open Constr
+open Context
open Vars
open Termops
open Entries
@@ -188,14 +189,14 @@ let build_id_coercion idf_opt source poly =
let lams,t = decompose_lam_assum c in
let val_f =
it_mkLambda_or_LetIn
- (mkLambda (Name Namegen.default_dependent_ident,
+ (mkLambda (make_annot (Name Namegen.default_dependent_ident) Sorts.Relevant,
applistc vs (Context.Rel.to_extended_list mkRel 0 lams),
mkRel 1))
lams
in
let typ_f =
List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d)
- (mkProd (Anonymous, applistc vs (Context.Rel.to_extended_list mkRel 0 lams), lift 1 t))
+ (mkProd (make_annot Anonymous Sorts.Relevant, applistc vs (Context.Rel.to_extended_list mkRel 0 lams), lift 1 t))
lams
in
(* juste pour verification *)
@@ -302,7 +303,7 @@ let try_add_new_identity_coercion id ~local poly ~source ~target =
let try_add_new_coercion_with_source ref ~local poly ~source =
try_add_new_coercion_core ref ~local poly (Some source) None false
-let add_coercion_hook poly local ref =
+let add_coercion_hook poly _uctx _trans local ref =
let local = match local with
| Discharge
| Local -> true
@@ -314,7 +315,7 @@ let add_coercion_hook poly local ref =
let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
-let add_subclass_hook poly local ref =
+let add_subclass_hook poly _uctx _trans local ref =
let stre = match local with
| Local -> true
| Global -> false
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 39c086eff5..1981e24ae4 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -149,7 +149,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
if program_mode then
let hook _ _ vis gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
- Impargs.declare_manual_implicits false gr [imps];
+ Impargs.declare_manual_implicits false gr imps;
let pri = intern_info pri in
Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
in
@@ -161,10 +161,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
in obls, Some constr, typ
| None -> [||], None, termtype
in
- let univ_hook = Obligations.mk_univ_hook hook in
+ let hook = Lemmas.mk_hook hook in
let ctx = Evd.evar_universe_context sigma in
ignore (Obligations.add_definition id ?term:constr
- ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~univ_hook obls)
+ ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls)
else
Flags.silently (fun () ->
(* spiwack: it is hard to reorder the actions to do
@@ -175,7 +175,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
let sigma = Evd.reset_future_goals sigma in
Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
~hook:(Lemmas.mk_hook
- (fun _ -> instance_hook k pri global imps ?hook));
+ (fun _ _ _ -> instance_hook k pri global imps ?hook));
(* spiwack: I don't know what to do with the status here. *)
if not (Option.is_empty term) then
let init_refine =
@@ -234,7 +234,7 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct
in
match rest with
| (n, _) :: _ ->
- unbound_method env' k.cl_impl (get_id n)
+ unbound_method env' sigma k.cl_impl (get_id n)
| _ ->
let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
let sigma, res = type_ctx_instance ~program_mode (push_rel_context ctx' env') sigma kcl_props props subst in
@@ -352,8 +352,8 @@ let named_of_rel_context l =
(fun decl (subst, ctx) ->
let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
let d = match decl with
- | LocalAssum (_,t) -> id, None, substl subst t
- | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
+ | LocalAssum (_,t) -> id, None, substl subst t
+ | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
(mkVar id :: subst, d :: ctx))
l ([], [])
in ctx
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 4fb06e4e09..37a33daf8f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -13,6 +13,7 @@ open Util
open Vars
open Declare
open Names
+open Context
open Globnames
open Constrexpr_ops
open Constrintern
@@ -57,6 +58,7 @@ match local with
strbrk " is not visible from current goals")
in
let r = VarRef ident in
+ let () = maybe_declare_manual_implicits true r imps in
let () = Typeclasses.declare_instance None true r in
let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
(r,Univ.Instance.empty,true)
@@ -147,8 +149,9 @@ let do_assumptions ~program_mode kind nl l =
(* We intepret all declarations in the same evar_map, i.e. as a telescope. *)
let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in
+ let r = Retyping.relevance_of_type env sigma t in
let env =
- EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in
+ EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (make_annot id r,t)) idl) env in
let ienv = List.fold_right (fun {CAst.v=id} ienv ->
let impls = compute_internalization_data env sigma Variable t imps in
Id.Map.add id impls ienv) idl ienv in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 5eb19eef54..28773a3965 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -94,22 +94,24 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
let (ce, evd, univdecl, imps as def) =
interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt
in
- if program_mode then
- let env = Global.env () in
- let (c,ctx), sideff = Future.force ce.const_entry_body in
- assert(Safe_typing.empty_private_constants = sideff);
- assert(Univ.ContextSet.is_empty ctx);
- let typ = match ce.const_entry_type with
- | Some t -> t
- | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
- in
- Obligations.check_evars env evd;
- let obls, _, c, cty =
- Obligations.eterm_obligations env ident evd 0 c typ
- in
- let ctx = Evd.evar_universe_context evd in
- let univ_hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook ?hook l r) in
- ignore(Obligations.add_definition
- ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~univ_hook obls)
- else let ce = check_definition ~program_mode def in
- ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps ?hook)
+ if program_mode then
+ let env = Global.env () in
+ let (c,ctx), sideff = Future.force ce.const_entry_body in
+ assert(Safe_typing.empty_private_constants = sideff);
+ assert(Univ.ContextSet.is_empty ctx);
+ let typ = match ce.const_entry_type with
+ | Some t -> t
+ | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
+ in
+ Obligations.check_evars env evd;
+ let obls, _, c, cty =
+ Obligations.eterm_obligations env ident evd 0 c typ
+ in
+ let ctx = Evd.evar_universe_context evd in
+ ignore(Obligations.add_definition
+ ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ?hook obls)
+ else
+ let ce = check_definition ~program_mode def in
+ let uctx = Evd.evar_universe_context evd in
+ let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+ ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps )
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 5229d9e8e8..2f00b41b7c 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -12,6 +12,7 @@ open Pp
open CErrors
open Util
open Constr
+open Context
open Vars
open Termops
open Declare
@@ -126,7 +127,9 @@ let interp_fix_context ~program_mode ~cofix env sigma fix =
sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
let interp_fix_ccl ~program_mode sigma impls (env,_) fix =
- interp_type_evars_impls ~program_mode ~impls env sigma fix.fix_type
+ let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.fix_type in
+ let r = Retyping.relevance_of_type env sigma c in
+ sigma, (c, r, impl)
let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl =
let open EConstr in
@@ -137,9 +140,9 @@ let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl =
let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx
-let prepare_recursive_declaration fixnames fixtypes fixdefs =
+let prepare_recursive_declaration fixnames fixrs fixtypes fixdefs =
let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
- let names = List.map (fun id -> Name id) fixnames in
+ let names = List.map2 (fun id r -> make_annot (Name id) r) fixnames fixrs in
(Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
(* Jump over let-bindings. *)
@@ -158,7 +161,7 @@ let compute_possible_guardness_evidences (ctx,_,recindex) =
List.interval 0 (Context.Rel.nhyps ctx - 1)
type recursive_preentry =
- Id.t list * constr option list * types list
+ Id.t list * Sorts.relevance list * constr option list * types list
(* Wellfounded definition *)
@@ -188,8 +191,8 @@ let interp_recursive ~program_mode ~cofix fixl notations =
on_snd List.split3 @@
List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma ~cofix) sigma fixl in
let fixctximpenvs, fixctximps = List.split fiximppairs in
- let sigma, (fixccls,fixcclimps) =
- on_snd List.split @@
+ let sigma, (fixccls,fixrs,fixcclimps) =
+ on_snd List.split3 @@
List.fold_left3_map (interp_fix_ccl ~program_mode) sigma fixctximpenvs fixctxs fixl in
let fixtypes = List.map2 build_fix_type fixctxs fixccls in
let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in
@@ -208,8 +211,8 @@ let interp_recursive ~program_mode ~cofix fixl notations =
Typing.solve_evars env sigma app
with e when CErrors.noncritical e -> sigma, t
in
- sigma, LocalAssum (id,fixprot) :: env'
- else sigma, LocalAssum (id,t) :: env')
+ sigma, LocalAssum (make_annot id Sorts.Relevant,fixprot) :: env'
+ else sigma, LocalAssum (make_annot id Sorts.Relevant,t) :: env')
(sigma,[]) fixnames fixtypes
in
let env_rec = push_named_context rec_sign env in
@@ -232,19 +235,19 @@ let interp_recursive ~program_mode ~cofix fixl notations =
let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
(* Build the fix declaration block *)
- (env,rec_sign,decl,sigma), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
+ (env,rec_sign,decl,sigma), (fixnames,fixrs,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
-let check_recursive isfix env evd (fixnames,fixdefs,_) =
+let check_recursive isfix env evd (fixnames,_,fixdefs,_) =
if List.for_all Option.has_some fixdefs then begin
let fixdefs = List.map Option.get fixdefs in
check_mutuality env evd isfix (List.combine fixnames fixdefs)
end
-let ground_fixpoint env evd (fixnames,fixdefs,fixtypes) =
+let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) =
check_evars_are_solved ~program_mode:false env evd;
let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in
let fixtypes = List.map EConstr.(to_constr evd) fixtypes in
- Evd.evar_universe_context evd, (fixnames,fixdefs,fixtypes)
+ Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes)
let interp_fixpoint ~cofix l ntns =
let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l ntns in
@@ -252,7 +255,7 @@ let interp_fixpoint ~cofix l ntns =
let uctx,fix = ground_fixpoint env evd fix in
(fix,pl,uctx,info)
-let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
@@ -267,7 +270,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
else begin
(* We shortcut the proof process *)
let fixdefs = List.map Option.get fixdefs in
- let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
+ let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
let env = Global.env() in
let indexes = search_guard env indexes fixdecls in
let fiximps = List.map (fun (n,r,p) -> r) fiximps in
@@ -287,7 +290,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
(* Declare notations *)
List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
-let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
@@ -302,7 +305,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
else begin
(* We shortcut the proof process *)
let fixdefs = List.map Option.get fixdefs in
- let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
+ let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
let vars = Vars.universes_of_constr (List.hd fixdecls) in
let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 338dfa5ef5..9bcb53697b 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -51,7 +51,7 @@ val interp_recursive :
(* env / signature / univs / evar_map *)
(Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) *
(* names / defs / types *)
- (Id.t list * EConstr.constr option list * EConstr.types list) *
+ (Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) *
(* ctx per mutual def / implicits / struct annotations *)
(EConstr.rel_context * Impargs.manual_explicitation list * int option) list
@@ -69,7 +69,7 @@ val extract_cofixpoint_components :
structured_fixpoint_expr list * decl_notation list
type recursive_preentry =
- Id.t list * constr option list * types list
+ Id.t list * Sorts.relevance list * constr option list * types list
val interp_fixpoint :
cofix:bool ->
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 9bbfb8eec6..977e804da2 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -13,6 +13,7 @@ open CErrors
open Sorts
open Util
open Constr
+open Context
open Environ
open Declare
open Names
@@ -70,9 +71,9 @@ let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
| c -> c
)
-let push_types env idl tl =
- List.fold_left2 (fun env id t -> EConstr.push_rel (LocalAssum (Name id,t)) env)
- env idl tl
+let push_types env idl rl tl =
+ List.fold_left3 (fun env id r t -> EConstr.push_rel (LocalAssum (make_annot (Name id) r,t)) env)
+ env idl rl tl
type structured_one_inductive_expr = {
ind_name : Id.t;
@@ -139,9 +140,6 @@ let make_conclusion_flexible sigma = function
| None -> sigma)
| _ -> sigma)
-let is_impredicative env u =
- u = Prop || (is_impredicative_set env && u = Set)
-
let interp_ind_arity env sigma ind =
let c = intern_gen IsType env sigma ind.ind_arity in
let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
@@ -152,7 +150,7 @@ let interp_ind_arity env sigma ind =
user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity")
| s ->
let concl = if pseudo_poly then Some s else None in
- sigma, (t, concl, impls)
+ sigma, (t, Retyping.relevance_of_sort s, concl, impls)
let interp_cstrs env sigma impls mldata arity ind =
let cnames,ctyps = List.split ind.ind_lc in
@@ -176,14 +174,14 @@ let sign_level env evd sign =
in
let u = univ_of_sort s in
(Univ.sup u lev, push_rel d env))
- sign (Univ.type0m_univ,env))
+ sign (Univ.Universe.sprop,env))
let sup_list min = List.fold_left Univ.sup min
let extract_level env evd min tys =
let sorts = List.map (fun ty ->
let ctx, concl = Reduction.dest_prod_assum env ty in
- sign_level env evd (LocalAssum (Anonymous, concl) :: ctx)) tys
+ sign_level env evd (LocalAssum (make_annot Anonymous Sorts.Relevant, concl) :: ctx)) tys
in sup_list min sorts
let is_flexible_sort evd u =
@@ -260,7 +258,7 @@ let solve_constraints_system levels level_bounds =
let inductive_levels env evd poly arities inds =
let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
let levels = List.map (fun (x,(ctx,a)) ->
- if a = Prop then None
+ if Sorts.is_prop a || Sorts.is_sprop a then None
else Some (univ_of_sort a)) destarities
in
let cstrs_levels, min_levels, sizes =
@@ -269,7 +267,7 @@ let inductive_levels env evd poly arities inds =
let len = List.length tys in
let minlev = Sorts.univ_of_sort du in
let minlev =
- if len > 1 && not (is_impredicative env du) then
+ if len > 1 && not (is_impredicative_sort env du) then
Univ.sup minlev Univ.type0_univ
else minlev
in
@@ -290,7 +288,7 @@ let inductive_levels env evd poly arities inds =
in
let evd, arities =
CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
- if is_impredicative env du then
+ if is_impredicative_sort env du then
(* Any product is allowed here. *)
evd, arity :: arities
else (* If in a predicative sort, or asked to infer the type,
@@ -313,16 +311,16 @@ let inductive_levels env evd poly arities inds =
(* "Polymorphic" type constraint and more than one constructor,
should not land in Prop. Add constraint only if it would
land in Prop directly (no informative arguments as well). *)
- Evd.set_leq_sort env evd Set du
+ Evd.set_leq_sort env evd Sorts.set du
else evd
in
let duu = Sorts.univ_of_sort du in
let evd =
if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then
if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then
- Evd.set_eq_sort env evd Prop du
+ Evd.set_eq_sort env evd Sorts.prop du
else evd
- else Evd.set_eq_sort env evd (Type cu) du
+ else Evd.set_eq_sort env evd (sort_of_univ cu) du
in
(evd, arity :: arities))
(evd,[]) (Array.to_list levels') destarities sizes
@@ -370,15 +368,15 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
(* Interpret the arities *)
let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in
+ let arities, relevances, arityconcl, indimpls = List.split4 arities in
- let fullarities = List.map (fun (c, _, _) -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in
- let env_ar = push_types env_uparams indnames fullarities in
+ let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in
+ let env_ar = push_types env_uparams indnames relevances fullarities in
let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
(* Compute interpretation metadatas *)
- let indimpls = List.map (fun (_, _, impls) -> userimpls @
- lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
- let arities = List.map pi1 arities and arityconcl = List.map pi2 arities in
+ let indimpls = List.map (fun impls -> userimpls @
+ lift_implicits (Context.Rel.nhyps ctx_params) impls) indimpls in
let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in
let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in
@@ -407,7 +405,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let userimpls = useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) userimpls) in
let indimpls = List.map (fun iimpl -> useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) iimpl)) indimpls in
let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_uparams) fullarities in
- let env_ar = push_types env0 indnames fullarities in
+ let env_ar = push_types env0 indnames relevances fullarities in
let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
(* Try further to solve evars, and instantiate them *)
@@ -529,7 +527,7 @@ let warn_non_primitive_record =
(hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (IndRef indsp) ++
strbrk" could not be defined as a primitive record")))
-let declare_mutual_inductive_with_eliminations mie pl impls =
+let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls =
(* spiwack: raises an error if the structure is supposed to be non-recursive,
but isn't *)
begin match mie.mind_entry_finite with
@@ -543,8 +541,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
let (_, kn), prim = declare_mind mie in
let mind = Global.mind_of_delta_kn kn in
- if match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false
- then warn_non_primitive_record (mind,0);
+ if primitive_expected && not prim then warn_non_primitive_record (mind,0);
Declare.declare_univ_binders (IndRef (mind,0)) pl;
List.iteri (fun i (indimpls, constrimpls) ->
let ind = (mind,i) in
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 1d6f652385..224cce67ad 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -43,6 +43,7 @@ type one_inductive_impls =
Impargs.manual_implicits list (* for constrs *)
val declare_mutual_inductive_with_eliminations :
+ ?primitive_expected:bool ->
mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
MutInd.t
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index a30313d37c..ad7c65b70c 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -12,6 +12,7 @@ open Pp
open CErrors
open Util
open Constr
+open Context
open Entries
open Vars
open Declare
@@ -41,7 +42,7 @@ let well_founded sigma = init_constant sigma (lib_ref "core.wf.well_founded")
let mkSubset sigma name typ prop =
let open EConstr in
let sigma, app_h = Evarutil.new_global sigma (delayed_force build_sigma).typ in
- sigma, mkApp (app_h, [| typ; mkLambda (name, typ, prop) |])
+ sigma, mkApp (app_h, [| typ; mkLambda (make_annot name Sorts.Relevant, typ, prop) |])
let make_qref s = qualid_of_string s
let lt_ref = make_qref "Init.Peano.lt"
@@ -58,7 +59,7 @@ let rec telescope sigma l =
List.fold_left
(fun (sigma, ty, tys, (k, constr)) decl ->
let t = RelDecl.get_type decl in
- let pred = mkLambda (RelDecl.get_name decl, t, ty) in
+ let pred = mkLambda (RelDecl.get_annot decl, t, ty) in
let sigma, ty = Evarutil.new_global sigma (lib_ref "core.sigT.type") in
let sigma, intro = Evarutil.new_global sigma (lib_ref "core.sigT.intro") in
let sigty = mkApp (ty, [|t; pred|]) in
@@ -73,7 +74,7 @@ let rec telescope sigma l =
let sigma, p2 = Evarutil.new_global sigma (lib_ref "core.sigT.proj2") in
let proj1 = applist (p1, [t; pred; prev]) in
let proj2 = applist (p2, [t; pred; prev]) in
- (sigma, lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
+ (sigma, lift 1 proj2, LocalDef (get_annot decl, proj1, t) :: subst))
(List.rev tys) tl (sigma, mkRel 1, [])
in sigma, ty, (LocalDef (n, last, t) :: subst), constr
@@ -98,7 +99,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
let sigma, argtyp, letbinders, make = telescope sigma binders_rel in
let argname = Id.of_string "recarg" in
- let arg = LocalAssum (Name argname, argtyp) in
+ let arg = LocalAssum (make_annot (Name argname) Sorts.Relevant, argtyp) in
let binders = letbinders @ [arg] in
let binders_env = push_rel_context binders_rel env in
let sigma, (rel, _) = interp_constr_evars_impls ~program_mode:true env sigma r in
@@ -135,7 +136,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let argid' = Id.of_string (Id.to_string argname ^ "'") in
let wfarg sigma len =
let sigma, ss_term = mkSubset sigma (Name argid') argtyp (wf_rel_fun (mkRel 1) (mkRel (len + 1))) in
- sigma, LocalAssum (Name argid', ss_term)
+ sigma, LocalAssum (make_annot (Name argid') Sorts.Relevant, ss_term)
in
let sigma, intern_bl =
let sigma, wfa = wfarg sigma 1 in
@@ -143,7 +144,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
in
let _intern_env = push_rel_context intern_bl env in
let sigma, proj = Evarutil.new_global sigma (delayed_force build_sigma).Coqlib.proj1 in
- let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
+ let wfargpred = mkLambda (make_annot (Name argid') Sorts.Relevant, argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
let projection = (* in wfarg :: arg :: before *)
mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
in
@@ -153,22 +154,23 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
now intern_arity is in wfarg :: arg *)
let sigma, wfa = wfarg sigma 1 in
let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfa] in
- let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in
+ let intern_fun_binder = LocalAssum (make_annot (Name (add_suffix recname "'")) Sorts.Relevant,
+ intern_fun_arity_prod) in
let sigma, curry_fun =
- let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
+ let wfpred = mkLambda (make_annot (Name argid') Sorts.Relevant, argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
let sigma, intro = Evarutil.new_global sigma (delayed_force build_sigma).Coqlib.intro in
let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
let rcurry = mkApp (rel, [| measure; lift len measure |]) in
- let lam = LocalAssum (Name (Id.of_string "recproof"), rcurry) in
+ let lam = LocalAssum (make_annot (Name (Id.of_string "recproof")) Sorts.Relevant, rcurry) in
let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in
let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
- sigma, LocalDef (Name recname, body, ty)
+ sigma, LocalDef (make_annot (Name recname) Sorts.Relevant, body, ty)
in
let fun_bl = intern_fun_binder :: [arg] in
let lift_lets = lift_rel_context 1 letbinders in
let sigma, intern_body =
- let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in
+ let ctx = LocalAssum (make_annot (Name recname) Sorts.Relevant, get_type curry_fun) :: binders_rel in
let (r, l, impls, scopes) =
Constrintern.compute_internalization_data env sigma
Constrintern.Recursive full_arity impls
@@ -180,7 +182,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
~impls:newimpls body (lift 1 top_arity)
in
let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
- let prop = mkLambda (Name argname, argtyp, top_arity_let) in
+ let prop = mkLambda (make_annot (Name argname) Sorts.Relevant, argtyp, top_arity_let) in
(* XXX: Previous code did parallel evdref update, so possible old
weak ordering semantics may bite here. *)
let sigma, def =
@@ -215,7 +217,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
if Impargs.is_implicit_args () || not (List.is_empty impls) then
- Impargs.declare_manual_implicits false gr [impls]
+ Impargs.declare_manual_implicits false gr impls
in
let typ = it_mkProd_or_LetIn top_arity binders in
hook, name, typ
@@ -223,11 +225,11 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let typ = it_mkProd_or_LetIn top_arity binders_rel in
let hook sigma _ _ l gr =
if Impargs.is_implicit_args () || not (List.is_empty impls) then
- Impargs.declare_manual_implicits false gr [impls]
+ Impargs.declare_manual_implicits false gr impls
in hook, recname, typ
in
(* XXX: Capturing sigma here... bad bad *)
- let univ_hook = Obligations.mk_univ_hook (hook sigma) in
+ let hook = Lemmas.mk_hook (hook sigma) in
(* XXX: Grounding non-ground terms here... bad bad *)
let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
let fullctyp = EConstr.to_constr sigma typ in
@@ -237,7 +239,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
in
let ctx = Evd.evar_universe_context sigma in
ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
- evars_typ ctx evars ~univ_hook)
+ evars_typ ctx evars ~hook)
let out_def = function
| Some def -> def
@@ -272,7 +274,7 @@ let do_program_recursive local poly fixkind fixl ntns =
(List.length rec_sign) def typ
in (id, def, typ, imps, evars)
in
- let (fixnames,fixdefs,fixtypes) = fix in
+ let (fixnames,fixrs,fixdefs,fixtypes) = fix in
let fiximps = List.map pi2 info in
let fixdefs = List.map out_def fixdefs in
let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in
@@ -281,7 +283,7 @@ let do_program_recursive local poly fixkind fixl ntns =
(* XXX: are we allowed to have evars here? *)
let fixtypes = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixtypes in
let fixdefs = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixdefs in
- let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
+ let fixdecls = Array.of_list (List.map2 (fun x r -> make_annot (Name x) r) fixnames fixrs),
Array.of_list fixtypes,
Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 361ed1a737..7dcd098183 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -33,7 +33,7 @@ let get_locality id ~kind = function
| Local -> true
| Global -> false
-let declare_definition ident (local, p, k) ?hook ce pl imps =
+let declare_definition ident (local, p, k) ?hook_data ce pl imps =
let fix_exn = Future.fix_exn_of ce.const_entry_body in
let gr = match local with
| Discharge when Lib.sections_are_opened () ->
@@ -49,11 +49,17 @@ let declare_definition ident (local, p, k) ?hook ce pl imps =
in
let () = maybe_declare_manual_implicits false gr imps in
let () = definition_message ident in
- Lemmas.call_hook ~fix_exn ?hook local gr; gr
+ begin
+ match hook_data with
+ | None -> ()
+ | Some (hook, uctx, extra_defs) ->
+ Lemmas.call_hook ~fix_exn ~hook uctx extra_defs local gr
+ end;
+ gr
-let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
- declare_definition f kind ce pl imps
+ declare_definition f kind ?hook_data ce pl imps
let check_definition_evars ~allow_evars sigma =
let env = Global.env () in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index e455b59ab2..3f95ec7107 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -13,16 +13,26 @@ open Decl_kinds
val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
-val declare_definition : Id.t -> definition_kind ->
- ?hook:Lemmas.declaration_hook ->
- Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits ->
- GlobRef.t
+val declare_definition
+ : Id.t
+ -> definition_kind
+ -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
+ -> Safe_typing.private_constants Entries.definition_entry
+ -> UnivNames.universe_binders
+ -> Impargs.manual_implicits
+ -> GlobRef.t
-val declare_fix : ?opaque:bool -> definition_kind ->
- UnivNames.universe_binders -> Entries.universes_entry ->
- Id.t -> Safe_typing.private_constants Entries.proof_output ->
- Constr.types -> Impargs.manual_implicits ->
- GlobRef.t
+val declare_fix
+ : ?opaque:bool
+ -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
+ -> definition_kind
+ -> UnivNames.universe_binders
+ -> Entries.universes_entry
+ -> Id.t
+ -> Safe_typing.private_constants Entries.proof_output
+ -> Constr.types
+ -> Impargs.manual_implicits
+ -> GlobRef.t
val prepare_definition : allow_evars:bool ->
?opaque:bool -> ?inline:bool -> poly:bool ->
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 06428b53f2..2bc95dbfcd 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -64,8 +64,8 @@ let process_vernac_interp_error exn = match fst exn with
wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
| Notation.PrimTokenNotationError(kind,ctx,sigma,te) ->
wrap_vernac_error exn (Himsg.explain_prim_token_notation_error kind ctx sigma te)
- | Typeclasses_errors.TypeClassError(env, te) ->
- wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
+ | Typeclasses_errors.TypeClassError(env, sigma, te) ->
+ wrap_vernac_error exn (Himsg.explain_typeclass_error env sigma te)
| Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) ->
wrap_vernac_error exn (Himsg.explain_mismatched_contexts e c l x)
| InductiveError e ->
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 42bee25da3..589b15fd41 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -16,6 +16,7 @@ open Util
open Names
open Glob_term
open Vernacexpr
+open Impargs
open Constrexpr
open Constrexpr_ops
open Extend
@@ -836,11 +837,11 @@ GRAMMAR EXTEND Gram
];
(* Same as [argument_spec_block], but with only implicit status and names *)
more_implicits_block: [
- [ name = name -> { [(name.CAst.v, Vernacexpr.NotImplicit)] }
+ [ name = name -> { [(name.CAst.v, NotImplicit)] }
| "["; items = LIST1 name; "]" ->
- { List.map (fun name -> (name.CAst.v, Vernacexpr.Implicit)) items }
+ { List.map (fun name -> (name.CAst.v, Impargs.Implicit)) items }
| "{"; items = LIST1 name; "}" ->
- { List.map (fun name -> (name.CAst.v, Vernacexpr.MaximallyImplicit)) items }
+ { List.map (fun name -> (name.CAst.v, MaximallyImplicit)) items }
]
];
strategy_level:
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 9dd321be51..32754478a5 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -14,6 +14,7 @@ open Names
open Nameops
open Namegen
open Constr
+open Context
open Termops
open Environ
open Pretype_errors
@@ -103,9 +104,9 @@ let canonize_constr sigma c =
let dn = Name.Anonymous in
let rec canonize_binders c =
match EConstr.kind sigma c with
- | Prod (_,t,b) -> mkProd(dn,t,b)
- | Lambda (_,t,b) -> mkLambda(dn,t,b)
- | LetIn (_,u,t,b) -> mkLetIn(dn,u,t,b)
+ | Prod (x,t,b) -> mkProd({x with binder_name=dn},t,b)
+ | Lambda (x,t,b) -> mkLambda({x with binder_name=dn},t,b)
+ | LetIn (x,u,t,b) -> mkLetIn({x with binder_name=dn},u,t,b)
| _ -> EConstr.map sigma canonize_binders c
in
canonize_binders c
@@ -125,7 +126,7 @@ let display_eq ~flags env sigma t1 t2 =
let rec pr_explicit_aux env sigma t1 t2 = function
| [] ->
(* no specified flags: default. *)
- (quote (Printer.pr_leconstr_env env sigma t1), quote (Printer.pr_leconstr_env env sigma t2))
+ Printer.pr_leconstr_env env sigma t1, Printer.pr_leconstr_env env sigma t2
| flags :: rem ->
let equal = display_eq ~flags env sigma t1 t2 in
if equal then
@@ -137,7 +138,7 @@ let rec pr_explicit_aux env sigma t1 t2 = function
in
let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) ()
in
- quote (Ppconstr.pr_lconstr_expr ct1), quote (Ppconstr.pr_lconstr_expr ct2)
+ Ppconstr.pr_lconstr_expr env sigma ct1, Ppconstr.pr_lconstr_expr env sigma ct2
let explicit_flags =
let open Constrextern in
@@ -148,8 +149,25 @@ let explicit_flags =
[print_implicits; print_coercions; print_no_symbol]; (* Then more! *)
[print_universes; print_implicits; print_coercions; print_no_symbol] (* and more! *) ]
+let with_diffs pm pn =
+ try
+ let tokenize_string = Proof_diffs.tokenize_string in
+ Pp_diff.diff_pp ~tokenize_string pm pn
+ with Pp_diff.Diff_Failure msg ->
+ begin
+ try ignore(Sys.getenv("HIDEDIFFFAILUREMSG"))
+ with Not_found ->
+ Feedback.msg_warning Pp.(
+ hov 0 (str ("Diff failure: " ^ msg) ++ spc () ++
+ hov 0 (str "Showing message without diff highlighting" ++ spc () ++
+ hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str "."))))
+ end;
+ pm, pn
+
let pr_explicit env sigma t1 t2 =
- pr_explicit_aux env sigma t1 t2 explicit_flags
+ let p1, p2 = pr_explicit_aux env sigma t1 t2 explicit_flags in
+ let p1, p2 = with_diffs p1 p2 in
+ quote p1, quote p2
let pr_db env i =
try
@@ -193,13 +211,13 @@ let rec pr_disjunction pr = function
| a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l
| [] -> assert false
-let explain_elim_arity env sigma ind sorts c pj okinds =
+let explain_elim_arity env sigma ind c pj okinds =
let open EConstr in
let env = make_all_name_different env sigma in
let pi = pr_inductive env (fst ind) in
let pc = pr_leconstr_env env sigma c in
let msg = match okinds with
- | Some(kp,ki,explanation) ->
+ | Some(sorts,kp,ki,explanation) ->
let pki = Sorts.pr_sort_family ki in
let pkp = Sorts.pr_sort_family kp in
let explanation = match explanation with
@@ -262,7 +280,7 @@ let explain_ill_formed_branch env sigma c ci actty expty =
let explain_generalization env sigma (name,var) j =
let pe = pr_ne_context_of (str "In environment") env sigma in
let pv = pr_letype_env env sigma var in
- let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) env) sigma j in
+ let (pc,pt) = pr_ljudge_env (push_rel_assum (make_annot name Sorts.Relevant,var) env) sigma j in
pe ++ str "Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
str "over" ++ brk(1,1) ++ pc ++ str "," ++ spc () ++
str "it has type" ++ spc () ++ pt ++
@@ -307,7 +325,7 @@ let explain_unification_error env sigma p1 p2 = function
| UnifUnivInconsistency p ->
if !Constrextern.print_universes then
[str "universe inconsistency: " ++
- Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes p]
+ Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p]
else
[str "universe inconsistency"]
| CannotSolveConstraint ((pb,env,t,u),e) ->
@@ -339,6 +357,20 @@ let explain_actual_type env sigma j t reason =
str "while it is expected to have type" ++ brk(1,1) ++ pt ++
ppreason ++ str ".")
+let explain_incorrect_primitive env sigma j exp =
+ let env = make_all_name_different env sigma in
+ let {uj_val=p;uj_type=t} = j in
+ let t = Reductionops.nf_betaiota env sigma t in
+ let exp = Reductionops.nf_betaiota env sigma exp in
+ (* Actually print *)
+ let pe = pr_ne_context_of (str "In environment") env sigma in
+ let (pt, pct) = pr_explicit env sigma exp t in
+ pe ++
+ hov 0 (
+ str "The primitive" ++ brk(1,1) ++ str (CPrimitives.op_or_type_to_string p) ++ spc () ++
+ str "has type" ++ brk(1,1) ++ pct ++ spc () ++
+ str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str ".")
+
let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
let randl = jv_nf_betaiotaevar env sigma randl in
let actualtyp = Reductionops.nf_betaiota env sigma actualtyp in
@@ -400,7 +432,7 @@ let explain_not_product env sigma c =
let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
let pr_lconstr_env env sigma c = pr_leconstr_env env sigma c in
let prt_name i =
- match names.(i) with
+ match names.(i).binder_name with
Name id -> str "Recursive definition of " ++ Id.print id
| Anonymous -> str "The " ++ pr_nth i ++ str " definition" in
@@ -415,7 +447,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
| RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) ->
let arg_env = make_all_name_different arg_env sigma in
let called =
- match names.(j) with
+ match names.(j).binder_name with
Name id -> Id.print id
| Anonymous -> str "the " ++ pr_nth i ++ str " definition" in
let pr_db x = quote (pr_db env x) in
@@ -435,7 +467,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
| NotEnoughArgumentsForFixCall j ->
let called =
- match names.(j) with
+ match names.(j).binder_name with
Name id -> Id.print id
| Anonymous -> str "the " ++ pr_nth i ++ str " definition" in
str "Recursive call to " ++ called ++ str " has not enough arguments"
@@ -474,6 +506,8 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
str "The return clause of the following pattern matching should be" ++
strbrk " a coinductive type:" ++
spc () ++ pr_lconstr_env env sigma c
+ | FixpointOnIrrelevantInductive ->
+ strbrk "Fixpoints on proof irrelevant inductive types should produce proof irrelevant values"
in
prt_name i ++ str " is ill-formed." ++ fnl () ++
pr_ne_context_of (str "In environment") env sigma ++
@@ -696,6 +730,12 @@ let explain_undeclared_universe env sigma l =
Termops.pr_evd_level sigma l ++
spc () ++ str "(maybe a bugged tactic)."
+let explain_disallowed_sprop () =
+ Pp.(str "SProp not allowed, you need to use -allow-sprop.")
+
+let explain_bad_relevance env =
+ strbrk "Bad relevance (maybe a bugged tactic)."
+
let explain_type_error env sigma err =
let env = make_all_name_different env sigma in
match err with
@@ -709,8 +749,8 @@ let explain_type_error env sigma err =
explain_bad_assumption env sigma c
| ReferenceVariables (id,c) ->
explain_reference_variables sigma id c
- | ElimArity (ind, aritylst, c, pj, okinds) ->
- explain_elim_arity env sigma ind aritylst c pj okinds
+ | ElimArity (ind, c, pj, okinds) ->
+ explain_elim_arity env sigma ind c pj okinds
| CaseNotInductive cj ->
explain_case_not_inductive env sigma cj
| NumberBranches (cj, n) ->
@@ -720,7 +760,9 @@ let explain_type_error env sigma err =
| Generalization (nvar, c) ->
explain_generalization env sigma nvar c
| ActualType (j, pt) ->
- explain_actual_type env sigma j pt None
+ explain_actual_type env sigma j pt None
+ | IncorrectPrimitive (j, t) ->
+ explain_incorrect_primitive env sigma j t
| CantApplyBadType (t, rator, randl) ->
explain_cant_apply_bad_type env sigma t rator randl
| CantApplyNonFunctional (rator, randl) ->
@@ -735,6 +777,8 @@ let explain_type_error env sigma err =
explain_unsatisfied_constraints env sigma cst
| UndeclaredUniverse l ->
explain_undeclared_universe env sigma l
+ | DisallowedSProp -> explain_disallowed_sprop ()
+ | BadRelevance -> explain_bad_relevance env
let pr_position (cl,pos) =
let clpos = match cl with
@@ -848,6 +892,7 @@ let explain_pretype_error env sigma err =
| TypingError t -> explain_type_error env sigma t
| CannotUnifyOccurrences (b,c1,c2,e) -> explain_cannot_unify_occurrences env sigma b c1 c2 e
| UnsatisfiableConstraints (c,comp) -> explain_unsatisfiable_constraints env sigma c comp
+ | DisallowedSProp -> explain_disallowed_sprop ()
(* Module errors *)
@@ -1039,37 +1084,38 @@ let explain_module_internalization_error = function
(* Typeclass errors *)
-let explain_not_a_class env c =
- let sigma = Evd.from_env env in
- let c = EConstr.to_constr sigma c in
- pr_constr_env env sigma c ++ str" is not a declared type class."
+let explain_not_a_class env sigma c =
+ pr_econstr_env env sigma c ++ str" is not a declared type class."
-let explain_unbound_method env cid { CAst.v = id } =
+let explain_unbound_method env sigma cid { CAst.v = id } =
str "Unbound method name " ++ Id.print (id) ++ spc () ++
str"of class" ++ spc () ++ pr_global cid ++ str "."
-let pr_constr_exprs exprs =
+let pr_constr_exprs env sigma exprs =
hv 0 (List.fold_right
- (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr d ++ pps)
+ (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr env sigma d ++ pps)
exprs (mt ()))
let explain_mismatched_contexts env c i j =
+ let sigma = Evd.from_env env in
+ let pm, pn = with_diffs (pr_rel_context env sigma j) (pr_constr_exprs env sigma i) in
str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
- hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env (Evd.from_env env) j) ++
+ hov 1 (str"Expected:" ++ brk (1, 1) ++ pm) ++
fnl () ++ brk (1,1) ++
- hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i)
+ hov 1 (str"Found:" ++ brk (1, 1) ++ pn)
-let explain_typeclass_error env = function
- | NotAClass c -> explain_not_a_class env c
- | UnboundMethod (cid, id) -> explain_unbound_method env cid id
+let explain_typeclass_error env sigma = function
+ | NotAClass c -> explain_not_a_class env sigma c
+ | UnboundMethod (cid, id) -> explain_unbound_method env sigma cid id
(* Refiner errors *)
let explain_refiner_bad_type env sigma arg ty conclty =
+ let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_lconstr_env env sigma conclty) in
str "Refiner was given an argument" ++ brk(1,1) ++
pr_lconstr_env env sigma arg ++ spc () ++
- str "of type" ++ brk(1,1) ++ pr_lconstr_env env sigma ty ++ spc () ++
- str "instead of" ++ brk(1,1) ++ pr_lconstr_env env sigma conclty ++ str "."
+ str "of type" ++ brk(1,1) ++ pm ++ spc () ++
+ str "instead of" ++ brk(1,1) ++ pn ++ str "."
let explain_refiner_unresolved_bindings l =
str "Unable to find an instance for the " ++
@@ -1181,7 +1227,7 @@ let error_large_non_prop_inductive_not_in_type () =
str "Large non-propositional inductive types must be in Type."
let error_inductive_bad_univs () =
- str "Incorrect universe constrains declared for inductive type."
+ str "Incorrect universe constraints declared for inductive type."
(* Recursion schemes errors *)
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index f22354cdbf..d0f42ea16b 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -26,7 +26,7 @@ val explain_inductive_error : inductive_error -> Pp.t
val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t
-val explain_typeclass_error : env -> typeclass_error -> Pp.t
+val explain_typeclass_error : env -> Evd.evar_map -> typeclass_error -> Pp.t
val explain_recursion_scheme_error : env -> recursion_scheme_error -> Pp.t
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index caafd6ac2f..1e733acc59 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -228,17 +228,20 @@ let declare_one_case_analysis_scheme ind =
let kinds_from_prop =
[InType,rect_scheme_kind_from_prop;
InProp,ind_scheme_kind_from_prop;
- InSet,rec_scheme_kind_from_prop]
+ InSet,rec_scheme_kind_from_prop;
+ InSProp,sind_scheme_kind_from_prop]
let kinds_from_type =
[InType,rect_dep_scheme_kind_from_type;
InProp,ind_dep_scheme_kind_from_type;
- InSet,rec_dep_scheme_kind_from_type]
+ InSet,rec_dep_scheme_kind_from_type;
+ InSProp,sind_dep_scheme_kind_from_type]
let nondep_kinds_from_type =
[InType,rect_scheme_kind_from_type;
InProp,ind_scheme_kind_from_type;
- InSet,rec_scheme_kind_from_type]
+ InSet,rec_scheme_kind_from_type;
+ InSProp,sind_scheme_kind_from_type]
let declare_one_induction_scheme ind =
let (mib,mip) = Global.lookup_inductive ind in
@@ -246,6 +249,9 @@ let declare_one_induction_scheme ind =
let from_prop = kind == InProp in
let depelim = Inductiveops.has_dependent_elim mib in
let kelim = elim_sorts (mib,mip) in
+ let kelim = if Global.sprop_allowed () then kelim
+ else List.filter (fun s -> s <> InSProp) kelim
+ in
let elims =
List.map_filter (fun (sort,kind) ->
if Sorts.List.mem sort kelim then Some kind else None)
@@ -347,19 +353,23 @@ requested
match sort_of_ind with
| InProp ->
if isdep then (match z with
+ | InSProp -> inds ^ "s_dep"
| InProp -> inds ^ "_dep"
| InSet -> recs ^ "_dep"
| InType -> recs ^ "t_dep")
else ( match z with
+ | InSProp -> inds ^ "s"
| InProp -> inds
| InSet -> recs
| InType -> recs ^ "t" )
| _ ->
if isdep then (match z with
+ | InSProp -> inds ^ "s"
| InProp -> inds
| InSet -> recs
| InType -> recs ^ "t" )
else (match z with
+ | InSProp -> inds ^ "s_nodep"
| InProp -> inds ^ "_nodep"
| InSet -> recs ^ "_nodep"
| InType -> recs ^ "t_nodep")
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 83dd1aa8e4..0d0732cbb4 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -34,10 +34,13 @@ open Impargs
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
-type declaration_hook = Decl_kinds.locality -> GlobRef.t -> unit
+type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
+type declaration_hook = hook_type
+
let mk_hook hook = hook
-let call_hook ?hook ?fix_exn l c =
- try Option.iter (fun hook -> hook l c) hook
+
+let call_hook ?hook ?fix_exn uctx trans l c =
+ try Option.iter (fun hook -> hook uctx trans l c) hook
with e when CErrors.noncritical e ->
let e = CErrors.push e in
let e = Option.cata (fun fix -> fix e) e fix_exn in
@@ -174,7 +177,7 @@ let look_for_possibly_mutual_statements sigma = function
(* Saving a goal *)
-let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
+let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes =
let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
try
let const = adjust_guardness_conditions const do_guard in
@@ -203,7 +206,7 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
gr
in
definition_message id;
- call_hook ?hook locality r
+ call_hook ?hook universes [] locality r
with e when CErrors.noncritical e ->
let e = CErrors.push e in
iraise (fix_exn e)
@@ -289,7 +292,7 @@ let warn_let_as_axiom =
(fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++
spc () ++ strbrk "declared as an axiom.")
-let admit ?hook (id,k,e) pl () =
+let admit ?hook ctx (id,k,e) pl () =
let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
let () = match k with
| Global, _, _ -> ()
@@ -297,16 +300,15 @@ let admit ?hook (id,k,e) pl () =
in
let () = assumption_message id in
Declare.declare_univ_binders (ConstRef kn) pl;
- call_hook ?hook Global (ConstRef kn)
+ call_hook ?hook ctx [] Global (ConstRef kn)
(* Starting a goal *)
-let universe_proof_terminator ?univ_hook compute_guard =
+let standard_proof_terminator ?(hook : declaration_hook option) compute_guard =
let open Proof_global in
make_terminator begin function
| Admitted (id,k,pe,ctx) ->
- let hook = Option.map (fun univ_hook -> univ_hook (Some ctx)) univ_hook in
- admit ?hook (id,k,pe) (UState.universe_binders ctx) ();
+ let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in
Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) ->
let is_opaque, export_seff = match opaque with
@@ -317,25 +319,21 @@ let universe_proof_terminator ?univ_hook compute_guard =
let id = match idopt with
| None -> id
| Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
- let hook = Option.map (fun univ_hook -> univ_hook (Some universes)) univ_hook in
- save ~export_seff id const universes compute_guard persistence hook
+ let () = save ~export_seff id const universes compute_guard persistence hook universes in
+ ()
| Proved (opaque,idopt, _ ) ->
CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term")
end
-let standard_proof_terminator ?hook compute_guard =
- let univ_hook = Option.map (fun hook _ -> hook) hook in
- universe_proof_terminator ?univ_hook compute_guard
-
let initialize_named_context_for_proof () =
let sign = Global.named_context () in
List.fold_right
(fun d signv ->
let id = NamedDecl.get_id d in
- let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
+ let d = if variable_opacity id then NamedDecl.drop_body d else d in
Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
-let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
+let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?(hook : declaration_hook option) c =
let terminator = match terminator with
| None -> standard_proof_terminator ?hook compute_guard
| Some terminator -> terminator ?hook compute_guard
@@ -348,20 +346,6 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
let goals = [ Global.env_of_context sign , c ] in
Proof_global.start_proof sigma id ?pl kind goals terminator
-let start_proof_univs id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?univ_hook c =
- let terminator = match terminator with
- | None ->
- universe_proof_terminator ?univ_hook compute_guard
- | Some terminator -> terminator ?univ_hook compute_guard
- in
- let sign =
- match sign with
- | Some sign -> sign
- | None -> initialize_named_context_for_proof ()
- in
- let goals = [ Global.env_of_context sign , c ] in
- Proof_global.start_proof sigma id ?pl kind goals terminator
-
let rec_tac_initializer finite guard thms snl =
if finite then
match List.map (fun (id,(t,_)) -> (id,t)) thms with
@@ -394,11 +378,7 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
match thms with
| [] -> anomaly (Pp.str "No proof to start.")
| (id,(t,(_,imps)))::other_thms ->
- let hook ctx strength ref =
- let ctx = match ctx with
- | None -> UState.empty
- | Some ctx -> ctx
- in
+ let hook ctx _ strength ref =
let other_thms_data =
if List.is_empty other_thms then [] else
(* there are several theorems defined mutually *)
@@ -410,8 +390,8 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
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 ?hook strength ref) thms_data in
- start_proof_univs id ~pl:decl kind sigma t ~univ_hook:(fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard;
+ call_hook ?hook ctx [] strength ref) thms_data in
+ start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard;
ignore (Proof_global.with_current_proof (fun _ p ->
match init_tac with
| None -> p,(true,[])
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index a9a10a6e38..72c666e903 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -13,10 +13,29 @@ open Decl_kinds
type declaration_hook
-val mk_hook : (Decl_kinds.locality -> GlobRef.t -> unit) -> declaration_hook
-val call_hook :
- ?hook:declaration_hook -> ?fix_exn:Future.fix_exn ->
- Decl_kinds.locality -> GlobRef.t -> unit
+(* Hooks allow users of the API to perform arbitrary actions at
+ * proof/definition saving time. For example, to register a constant
+ * as a Coercion, perform some cleanup, update the search database,
+ * etc...
+ *
+ * Here, we use an extended hook type suitable for obligations /
+ * equations.
+ *)
+(** [hook_type] passes to the client:
+ - [ustate]: universe constraints obtained when the term was closed
+ - [(n1,t1),...(nm,tm)]: association list between obligation
+ name and the corresponding defined term (might be a constant,
+ but also an arbitrary term in the Expand case of obligations)
+ - [locality]: Locality of the original declaration
+ - [ref]: identifier of the origianl declaration
+ *)
+type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
+
+val mk_hook : hook_type -> declaration_hook
+val call_hook
+ : ?hook:declaration_hook
+ -> ?fix_exn:Future.fix_exn
+ -> hook_type
val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
@@ -24,12 +43,6 @@ val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map
?compute_guard:Proof_global.lemma_possible_guards ->
?hook:declaration_hook -> EConstr.types -> unit
-val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
- ?terminator:(?univ_hook:(UState.t option -> declaration_hook) -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
- ?sign:Environ.named_context_val ->
- ?compute_guard:Proof_global.lemma_possible_guards ->
- ?univ_hook:(UState.t option -> declaration_hook) -> EConstr.types -> unit
-
val start_proof_com :
program_mode:bool -> ?inference_hook:Pretyping.inference_hook ->
?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list ->
@@ -43,11 +56,6 @@ val start_proof_with_initialization :
(EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list ->
int list option -> unit
-val universe_proof_terminator :
- ?univ_hook:(UState.t option -> declaration_hook) ->
- Proof_global.lemma_possible_guards ->
- Proof_global.proof_terminator
-
val standard_proof_terminator :
?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
Proof_global.proof_terminator
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index ba78c73131..9aca48f529 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -13,6 +13,7 @@ open Declare
open Term
open Constr
+open Context
open Vars
open Names
open Evd
@@ -20,15 +21,6 @@ open Pp
open CErrors
open Util
-type univ_declaration_hook = UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit
-let mk_univ_hook f = f
-let call_univ_hook ?univ_hook ?fix_exn uctx trans l c =
- try Option.iter (fun hook -> hook uctx trans l c) univ_hook
- with e when CErrors.noncritical e ->
- let e = CErrors.push e in
- let e = Option.cata (fun fix -> fix e) e fix_exn in
- iraise e
-
module NamedDecl = Context.Named.Declaration
let get_fix_exn, stm_get_fix_exn = Hook.make ()
@@ -133,11 +125,11 @@ let etype_of_evar evs hyps concl =
| LocalDef (id,c,_) ->
let c', s'', trans'' = subst_evar_constr evs n mkVar c in
let c' = subst_vars acc 0 c' in
- mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
+ mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
Int.Set.union s'' s',
Id.Set.union trans'' trans'
- | LocalAssum (id,_) ->
- mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
+ | LocalAssum (id,_) ->
+ mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
| [] ->
let t', s, trans = subst_evar_constr evs n mkVar concl in
subst_vars acc 0 t', s, trans
@@ -321,7 +313,7 @@ type program_info_aux = {
prg_notations : notations ;
prg_kind : definition_kind;
prg_reduce : constr -> constr;
- prg_hook : univ_declaration_hook option;
+ prg_hook : Lemmas.declaration_hook option;
prg_opaque : bool;
prg_sign: named_context_val;
}
@@ -482,13 +474,13 @@ let declare_definition prg =
let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
let () = progmap_remove prg in
let ubinders = UState.universe_binders uctx in
- let hook = Lemmas.mk_hook (fun l r -> call_univ_hook ?univ_hook:prg.prg_hook ~fix_exn uctx obls l r; ()) in
+ let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
DeclareDef.declare_definition prg.prg_name
- prg.prg_kind ce ubinders prg.prg_implicits ~hook
+ prg.prg_kind ce ubinders prg.prg_implicits ?hook_data
let rec lam_index n t acc =
match Constr.kind t with
- | Lambda (Name n', _, _) when Id.equal n n' ->
+ | Lambda ({binder_name=Name n'}, _, _) when Id.equal n n' ->
acc
| Lambda (_, _, b) ->
lam_index n b (succ acc)
@@ -517,11 +509,12 @@ let declare_mutual_definition l =
let subs, typ = subst_prog oblsubst x in
let env = Global.env () in
let sigma = Evd.from_ctx x.prg_ctx in
+ let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in
let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
let term = EConstr.to_constr sigma term in
let typ = EConstr.to_constr sigma typ in
- let def = (x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) in
+ let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in
let oblsubst = List.map (fun (id, (_, c)) -> id, c) oblsubst in
def, oblsubst
in
@@ -531,10 +524,12 @@ let declare_mutual_definition l =
(xdef :: defs, xobls @ obls)) l ([], [])
in
(* let fixdefs = List.map reduce_fix fixdefs in *)
- let fixdefs, fixtypes, fiximps = List.split3 defs in
+ let fixdefs, fixrs, fixtypes, fiximps = List.split4 defs in
let fixkind = Option.get first.prg_fixkind in
let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
- let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
+ let rvec = Array.of_list fixrs in
+ let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in
+ let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in
let (local,poly,kind) = first.prg_kind in
let fixnames = first.prg_deps in
let opaque = first.prg_opaque in
@@ -559,14 +554,16 @@ let declare_mutual_definition l =
(* Declare the recursive definitions *)
let univs = UState.univ_entry ~poly first.prg_ctx in
let fix_exn = Hook.get get_fix_exn () in
- let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
- fixnames fixdecls fixtypes fiximps in
- (* Declare notations *)
- List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
- Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
- let gr = List.hd kns in
- call_univ_hook ?univ_hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
- List.iter progmap_remove l; gr
+ let kns = List.map4
+ (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
+ fixnames fixdecls fixtypes fiximps
+ in
+ (* Declare notations *)
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
+ Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
+ let gr = List.hd kns in
+ Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
+ List.iter progmap_remove l; gr
let decompose_lam_prod c ty =
let open Context.Rel.Declaration in
@@ -663,7 +660,7 @@ let declare_obligation prg obl body ty uctx =
in
true, { obl with obl_body = body }
-let init_prog_info ?(opaque = false) ?univ_hook sign n udecl b t ctx deps fixkind
+let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind
notations obls impls kind reduce =
let obls', b =
match b with
@@ -689,7 +686,7 @@ let init_prog_info ?(opaque = false) ?univ_hook sign n udecl b t ctx deps fixkin
prg_obligations = (obls', Array.length obls');
prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
prg_implicits = impls; prg_kind = kind; prg_reduce = reduce;
- prg_hook = univ_hook; prg_opaque = opaque;
+ prg_hook = hook; prg_opaque = opaque;
prg_sign = sign }
let map_cardinal m =
@@ -844,9 +841,9 @@ let solve_by_tac ?loc name evi t poly ctx =
warn_solve_errored ?loc err;
None
-let obligation_terminator ?univ_hook name num guard auto pf =
+let obligation_terminator ?hook name num guard auto pf =
let open Proof_global in
- let term = Lemmas.universe_proof_terminator ?univ_hook guard in
+ let term = Lemmas.standard_proof_terminator ?hook guard in
match pf with
| Admitted _ -> apply_terminator term pf
| Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
@@ -912,7 +909,7 @@ let obligation_terminator ?univ_hook name num guard auto pf =
| Proved (_, _, _ ) ->
CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term")
-let obligation_hook prg obl num auto ctx' _ gr =
+let obligation_hook prg obl num auto ctx' _ _ gr =
let obls, rem = prg.prg_obligations in
let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in
let transparent = evaluable_constant cst (Global.env ()) in
@@ -922,7 +919,6 @@ let obligation_hook prg obl num auto ctx' _ gr =
if not transparent then err_not_transp ()
| _ -> ()
in
- let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
let inst, ctx' =
if not (pi2 prg.prg_kind) (* Not polymorphic *) then
(* The universe context was declared globally, we continue
@@ -969,11 +965,11 @@ let rec solve_obligation prg num tac =
let evd = Evd.from_ctx prg.prg_ctx in
let evd = Evd.update_sigma_env evd (Global.env ()) in
let auto n tac oblset = auto_solve_obligations n ~oblset tac in
- let terminator ?univ_hook guard =
+ let terminator ?hook guard =
Proof_global.make_terminator
- (obligation_terminator ?univ_hook prg.prg_name num guard auto) in
- let univ_hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
- let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~univ_hook in
+ (obligation_terminator ?hook prg.prg_name num guard auto) in
+ let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
+ let () = Lemmas.start_proof ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
let _ = Pfedit.by !default_tactic in
Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac
@@ -1110,10 +1106,10 @@ let show_term n =
let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
- ?(reduce=reduce) ?univ_hook ?(opaque = false) obls =
+ ?(reduce=reduce) ?hook ?(opaque = false) obls =
let sign = Lemmas.initialize_named_context_for_proof () in
let info = Id.print n ++ str " has type-checked" in
- let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?univ_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 ".");
@@ -1130,13 +1126,13 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
?(kind=Global,false,Definition) ?(reduce=reduce)
- ?univ_hook ?(opaque = false) notations fixkind =
+ ?hook ?(opaque = false) notations fixkind =
let sign = Lemmas.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 univdecl (Some b) t ctx deps (Some fixkind)
- notations obls imps kind reduce ?univ_hook
+ notations obls imps kind reduce ?hook
in progmap_add n (CEphemeron.create prg)) l;
let _defined =
List.fold_left (fun finished x ->
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 4eef668f56..c5720363b4 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -13,12 +13,6 @@ open Constr
open Evd
open Names
-type univ_declaration_hook
-val mk_univ_hook : (UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit) ->
- univ_declaration_hook
-val call_univ_hook : ?univ_hook:univ_declaration_hook -> ?fix_exn:Future.fix_exn ->
- UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit
-
(* This is a hack to make it possible for Obligations to craft a Qed
* behind the scenes. The fix_exn the Stm attaches to the Future proof
* is not available here, so we provide a side channel to get it *)
@@ -58,14 +52,19 @@ type progress = (* Resolution status of a program *)
val default_tactic : unit Proofview.tactic ref
-val add_definition : Names.Id.t -> ?term:constr -> types ->
- UState.t ->
- ?univdecl:UState.universe_decl -> (* Universe binders and constraints *)
- ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
- ?kind:Decl_kinds.definition_kind ->
- ?tactic:unit Proofview.tactic ->
- ?reduce:(constr -> constr) ->
- ?univ_hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress
+val add_definition
+ : Names.Id.t
+ -> ?term:constr -> types
+ -> UState.t
+ -> ?univdecl:UState.universe_decl (* Universe binders and constraints *)
+ -> ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list
+ -> ?kind:Decl_kinds.definition_kind
+ -> ?tactic:unit Proofview.tactic
+ -> ?reduce:(constr -> constr)
+ -> ?hook:Lemmas.declaration_hook
+ -> ?opaque:bool
+ -> obligation_info
+ -> progress
type notations =
(lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -82,7 +81,7 @@ val add_mutual_definitions :
?tactic:unit Proofview.tactic ->
?kind:Decl_kinds.definition_kind ->
?reduce:(constr -> constr) ->
- ?univ_hook:univ_declaration_hook -> ?opaque:bool ->
+ ?hook:Lemmas.declaration_hook -> ?opaque:bool ->
notations ->
fixpoint_kind -> unit
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index d22e52e960..506c3f9f49 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -33,7 +33,10 @@ open Pputils
let pr_constr = pr_constr_expr
let pr_lconstr = pr_lconstr_expr
- let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
+ let pr_spc_lconstr =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ pr_sep_com spc @@ pr_lconstr_expr env sigma
let pr_uconstraint (l, d, r) =
pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
@@ -92,7 +95,10 @@ open Pputils
| VernacEndSubproof -> str""
| _ -> str"."
- let pr_gen t = Pputils.pr_raw_generic (Global.env ()) t
+ let pr_gen t =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Pputils.pr_raw_generic env sigma t
let sep = fun _ -> spc()
let sep_v2 = fun _ -> str"," ++ spc()
@@ -142,7 +148,10 @@ open Pputils
let pr_search_about (b,c) =
(if b then str "-" else mt()) ++
match c with
- | SearchSubPattern p -> pr_constr_pattern_expr p
+ | SearchSubPattern p ->
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ pr_constr_pattern_expr env sigma p
| SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
let pr_search a gopt b pr_p =
@@ -225,8 +234,10 @@ open Pputils
++ spc() ++ prlist_with_sep spc pr_qualid c
| HintsExtern (n,c,tac) ->
let pat = match c with None -> mt () | Some pat -> pr_pat pat in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
- spc() ++ Pputils.pr_raw_generic (Global.env ()) tac
+ spc() ++ Pputils.pr_raw_generic env sigma tac
in
hov 2 (keyword "Hint "++ pph ++ opth)
@@ -298,7 +309,9 @@ open Pputils
pr_opt (fun sc -> str ": " ++ str sc) scopt
let pr_binders_arg =
- pr_non_empty_arg pr_binders
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ pr_non_empty_arg @@ pr_binders env sigma
let pr_and_type_binders_arg bl =
pr_binders_arg bl
@@ -402,25 +415,35 @@ open Pputils
hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
let pr_rec_definition ((iddecl,ro,bl,type_,def),ntn) =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
- let annot = pr_guard_annot pr_lconstr_expr bl ro in
+ let annot = pr_guard_annot (pr_lconstr_expr env sigma) bl ro in
pr_ident_decl iddecl ++ 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_pure_lconstr def) def
- ++ prlist (pr_decl_notation pr_constr) ntn
+ ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) type_
+ ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) def
+ ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
let pr_statement head (idpl,(bl,c)) =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
hov 2
(head ++ spc() ++ pr_ident_decl idpl ++ spc() ++
- (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
+ (match bl with [] -> mt() | _ -> pr_binders env sigma bl ++ spc()) ++
str":" ++ pr_spc_lconstr c)
(**************************************)
(* Pretty printer for vernac commands *)
(**************************************)
- let pr_constrarg c = spc () ++ pr_constr c
- let pr_lconstrarg c = spc () ++ pr_lconstr c
+ let pr_constrarg c =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ spc () ++ pr_constr env sigma c
+ let pr_lconstrarg c =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ spc () ++ pr_lconstr env sigma c
let pr_intarg n = spc () ++ int n
let pr_oc = function
@@ -429,21 +452,23 @@ open Pputils
| Some false -> str" :>>"
let pr_record_field ((x, pri), ntn) =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
let prx = match x with
| (oc,AssumExpr (id,t)) ->
hov 1 (pr_lname id ++
pr_oc oc ++ spc() ++
- pr_lconstr_expr t)
+ pr_lconstr_expr env sigma t)
| (oc,DefExpr(id,b,opt)) -> (match opt with
| Some t ->
hov 1 (pr_lname id ++
pr_oc oc ++ spc() ++
- pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
+ pr_lconstr_expr env sigma t ++ str" :=" ++ pr_lconstr env sigma b)
| None ->
hov 1 (pr_lname id ++ str" :=" ++ spc() ++
- pr_lconstr b)) in
+ pr_lconstr env sigma b)) in
let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
- prx ++ prpri ++ prlist (pr_decl_notation pr_constr) ntn
+ prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
let pr_record_decl b c fs =
pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++
@@ -566,6 +591,8 @@ open Pputils
let pr_vernac_expr v =
let return = tag_vernac v in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
match v with
| VernacLoad (f,s) ->
return (
@@ -700,7 +727,7 @@ open Pputils
| None -> mt()
| Some r ->
keyword "Eval" ++ spc() ++
- Ppred.pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
+ Ppred.pr_red_expr_env env sigma (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
keyword " in" ++ spc()
in
let pr_def_body = function
@@ -709,7 +736,7 @@ open Pputils
| None -> mt()
| Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty
in
- (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
+ (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr env sigma body))
| ProveBody (bl,t) ->
let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in
(pr_binders_arg bl, typ (pr_spc_lconstr t), None) in
@@ -746,7 +773,7 @@ open Pputils
let n = List.length (List.flatten (List.map fst (List.map snd l))) in
let pr_params (c, (xl, t)) =
hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++
- (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) in
+ (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr env sigma t)) in
let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
return (hov 2 (pr_assumption_token (n > 1) discharge kind ++
pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
@@ -771,9 +798,9 @@ open Pputils
str key ++ spc() ++
(if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
pr_and_type_binders_arg indpar ++
- pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++
+ pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++
str" :=") ++ pr_constructor_list k lc ++
- prlist (pr_decl_notation pr_constr) ntn
+ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
in
let key =
let (_,_,_,k,_),_ = List.hd l in
@@ -814,10 +841,10 @@ open Pputils
| NoDischarge -> str ""
in
let pr_onecorec ((iddecl,bl,c,def),ntn) =
- pr_ident_decl iddecl ++ 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
+ pr_ident_decl iddecl ++ spc() ++ pr_binders env sigma bl ++ spc() ++ str":" ++
+ spc() ++ pr_lconstr_expr env sigma c ++
+ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) def ++
+ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
in
return (
hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++
@@ -897,11 +924,11 @@ open Pputils
pr_and_type_binders_arg sup ++
str":" ++ spc () ++
(match bk with Implicit -> str "! " | Explicit -> mt ()) ++
- pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++
+ pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info ++
(match props with
| Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
| Some (true,_) -> assert false
- | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p
+ | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr env sigma p
| None -> mt()))
)
@@ -912,7 +939,7 @@ open Pputils
pr_and_type_binders_arg sup ++
str":" ++ spc () ++
(match bk with Implicit -> str "! " | Explicit -> mt ()) ++
- pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info)
+ pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info)
)
| VernacContext l ->
@@ -922,8 +949,8 @@ open Pputils
)
| VernacExistingInstance insts ->
- let pr_inst (id, info) =
- pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info
+ let pr_inst (id, info) =
+ pr_qualid id ++ pr_hint_info (pr_constr_pattern_expr env sigma) info
in
return (
hov 1 (keyword "Existing" ++ spc () ++
@@ -938,25 +965,25 @@ open Pputils
(* Modules and Module Types *)
| VernacDefineModule (export,m,bl,tys,bd) ->
- let b = pr_module_binders bl pr_lconstr in
+ let b = pr_module_binders bl (pr_lconstr env sigma) in
return (
hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++
pr_lident m ++ b ++
- pr_of_module_type pr_lconstr tys ++
+ pr_of_module_type (pr_lconstr env sigma) tys ++
(if List.is_empty bd then mt () else str ":= ") ++
prlist_with_sep (fun () -> str " <+")
- (pr_module_ast_inl true pr_lconstr) bd)
+ (pr_module_ast_inl true (pr_lconstr env sigma)) bd)
)
| VernacDeclareModule (export,id,bl,m1) ->
- let b = pr_module_binders bl pr_lconstr in
+ let b = pr_module_binders bl (pr_lconstr env sigma) in
return (
hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++
pr_lident id ++ b ++ str " :" ++
- pr_module_ast_inl true pr_lconstr m1)
+ pr_module_ast_inl true (pr_lconstr env sigma) m1)
)
| VernacDeclareModuleType (id,bl,tyl,m) ->
- let b = pr_module_binders bl pr_lconstr in
- let pr_mt = pr_module_ast_inl true pr_lconstr in
+ let b = pr_module_binders bl (pr_lconstr env sigma) in
+ let pr_mt = pr_module_ast_inl true (pr_lconstr env sigma) in
return (
hov 2 (keyword "Module Type " ++ pr_lident id ++ b ++
prlist_strict (fun m -> str " <:" ++ pr_mt m) tyl ++
@@ -964,7 +991,7 @@ open Pputils
prlist_with_sep (fun () -> str " <+ ") pr_mt m)
)
| VernacInclude (mexprs) ->
- let pr_m = pr_module_ast_inl false pr_lconstr in
+ let pr_m = pr_module_ast_inl false (pr_lconstr env sigma) in
return (
hov 2 (keyword "Include" ++ spc() ++
prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
@@ -1013,7 +1040,7 @@ open Pputils
pr_opt_hintbases dbnames)
)
| VernacHints (dbnames,h) ->
- return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
+ return (pr_hints dbnames h (pr_constr env sigma) (pr_constr_pattern_expr env sigma))
| VernacSyntacticDefinition (id,(ids,c),compat) ->
return (
hov 2
@@ -1033,9 +1060,9 @@ open Pputils
let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in
let pr_if b x = if b then x else str "" in
let pr_br imp x = match imp with
- | Vernacexpr.Implicit -> str "[" ++ x ++ str "]"
- | Vernacexpr.MaximallyImplicit -> str "{" ++ x ++ str "}"
- | Vernacexpr.NotImplicit -> x in
+ | Impargs.Implicit -> str "[" ++ x ++ str "]"
+ | Impargs.MaximallyImplicit -> str "{" ++ x ++ str "}"
+ | Impargs.NotImplicit -> x in
let rec print_arguments n l =
match n, l with
| Some 0, l -> spc () ++ str"/" ++ print_arguments None l
@@ -1071,7 +1098,7 @@ open Pputils
let n = List.length (List.flatten (List.map fst bl)) in
return (
hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " "))
- ++ pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl))
+ ++ pr_ne_params_list (pr_lconstr_expr env sigma) (List.map (fun sb -> false,sb) bl))
)
| VernacGeneralizable g ->
return (
@@ -1143,9 +1170,9 @@ open Pputils
let pr_mayeval r c = match r with
| Some r0 ->
hov 2 (keyword "Eval" ++ spc() ++
- Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++
- spc() ++ keyword "in" ++ spc () ++ pr_lconstr c)
- | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
+ Ppred.pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++
+ spc() ++ keyword "in" ++ spc () ++ pr_lconstr env sigma c)
+ | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr env sigma c)
in
let pr_i = match io with None -> mt ()
| Some i -> Goal_select.pr_goal_selector i ++ str ": " in
@@ -1155,12 +1182,12 @@ open Pputils
| VernacDeclareReduction (s,r) ->
return (
keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++
- Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r
+ Ppred.pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r
)
| VernacPrint p ->
return (pr_printable p)
| VernacSearch (sea,g,sea_r) ->
- return (pr_search sea g sea_r pr_constr_pattern_expr)
+ return (pr_search sea g sea_r @@ pr_constr_pattern_expr env sigma)
| VernacLocate loc ->
let pr_locate =function
| LocateAny qid -> pr_smart_global qid
@@ -1192,7 +1219,7 @@ open Pputils
return (
hov 2
(keyword "Comments" ++ spc()
- ++ prlist_with_sep sep (pr_comment pr_constr) l)
+ ++ prlist_with_sep sep (pr_comment (pr_constr env sigma)) l)
)
(* For extension *)
@@ -1204,12 +1231,12 @@ open Pputils
return (keyword "Proof " ++ spc () ++
keyword "using" ++ spc() ++ pr_using e)
| VernacProof (Some te, None) ->
- return (keyword "Proof with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te)
+ return (keyword "Proof with" ++ spc() ++ Pputils.pr_raw_generic env sigma te)
| VernacProof (Some te, Some e) ->
return (
keyword "Proof" ++ spc () ++
keyword "using" ++ spc() ++ pr_using e ++ spc() ++
- keyword "with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te
+ keyword "with" ++ spc() ++ Pputils.pr_raw_generic env sigma te
)
| VernacProofMode s ->
return (keyword "Proof Mode" ++ str s)
diff --git a/vernac/record.ml b/vernac/record.ml
index 0bd15e203b..23274040b0 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -17,6 +17,7 @@ open Names
open Globnames
open Nameops
open Constr
+open Context
open Vars
open Environ
open Declarations
@@ -66,6 +67,7 @@ let interp_fields_evars env sigma impls_env nots l =
List.fold_left2
(fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) ->
let sigma, (t', impl) = interp_type_evars_impls ~program_mode:false env sigma ~impls t in
+ let r = Retyping.relevance_of_type env sigma t' in
let sigma, b' =
Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@
interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in
@@ -75,8 +77,8 @@ let interp_fields_evars env sigma impls_env nots l =
| Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls
in
let d = match b' with
- | None -> LocalAssum (i,t')
- | Some b' -> LocalDef (i,b',t')
+ | None -> LocalAssum (make_annot i r,t')
+ | Some b' -> LocalDef (make_annot i r,b',t')
in
List.iter (Metasyntax.set_notation_for_interpretation env impls) no;
(EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls))
@@ -90,7 +92,7 @@ let compute_constructor_level evars env l =
Univ.sup (univ_of_sort s) univ
else univ
in (EConstr.push_rel d env, univ))
- l (env, Univ.type0m_univ)
+ l (env, Univ.Universe.sprop)
let binder_of_decl = function
| Vernacexpr.AssumExpr(n,t) -> (n,None,t)
@@ -144,8 +146,10 @@ let typecheck_params_and_fields finite def poly pl ps records =
in
let (sigma, template), typs = List.fold_left_map fold (sigma, true) records in
let arities = List.map (fun (typ, _) -> EConstr.it_mkProd_or_LetIn typ newps) typs in
- let fold accu (id, _, _, _) arity = EConstr.push_rel (LocalAssum (Name id,arity)) accu in
- let env_ar = EConstr.push_rel_context newps (List.fold_left2 fold env0 records arities) in
+ let relevances = List.map (fun (_,s) -> Sorts.relevance_of_sort s) typs in
+ let fold accu (id, _, _, _) arity r =
+ EConstr.push_rel (LocalAssum (make_annot (Name id) r,arity)) accu in
+ let env_ar = EConstr.push_rel_context newps (List.fold_left3 fold env0 records arities relevances) in
let assums = List.filter is_local_assum newps in
let impls_env =
let params = List.map (RelDecl.get_name %> Name.get_id) assums in
@@ -163,16 +167,16 @@ let typecheck_params_and_fields finite def poly pl ps records =
Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma in
let fold sigma (typ, sort) (_, newfs) =
let _, univ = compute_constructor_level sigma env_ar newfs in
- if not def && (Sorts.is_prop sort ||
- (Sorts.is_set sort && is_impredicative_set env0)) then
+ let univ = if Sorts.is_sprop sort then univ else Univ.Universe.sup univ Univ.type0m_univ in
+ if not def && is_impredicative_sort env0 sort then
sigma, typ
else
- let sigma = Evd.set_leq_sort env_ar sigma (Type univ) sort in
- if Univ.is_small_univ univ &&
+ let sigma = Evd.set_leq_sort env_ar sigma (Sorts.sort_of_univ univ) sort in
+ if Univ.is_small_univ univ &&
Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then
(* We can assume that the level in aritysort is not constrained
and clear it, if it is flexible *)
- Evd.set_eq_sort env_ar sigma Set sort, EConstr.mkSort (Sorts.sort_of_univ univ)
+ Evd.set_eq_sort env_ar sigma Sorts.set sort, EConstr.mkSort (Sorts.sort_of_univ univ)
else sigma, typ
in
let (sigma, typs) = List.fold_left2_map fold sigma typs data in
@@ -213,12 +217,12 @@ let warning_or_error coe indsp err =
strbrk " not defined.")
| BadTypedProj (fi,ctx,te) ->
match te with
- | ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) ->
+ | ElimArity (_,_,_,Some (_,_,_,NonInformativeToInformative)) ->
(Id.print fi ++
strbrk" cannot be defined because it is informative and " ++
Printer.pr_inductive (Global.env()) indsp ++
strbrk " is not.")
- | ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) ->
+ | ElimArity (_,_,_,Some (_,_,_,StrongEliminationOnNonSmallType)) ->
(Id.print fi ++
strbrk" cannot be defined because it is large and " ++
Printer.pr_inductive (Global.env()) indsp ++
@@ -284,7 +288,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
let r = mkIndU (indsp,u) in
let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*)
- let x = Name binder_name in
+ let x = make_annot (Name binder_name) mip.mind_relevance in
let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in
let lifted_fields = Termops.lift_rel_context 1 fields in
let primitive =
@@ -316,18 +320,19 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
else
let ccl = subst_projection fid subst ti in
let body = match decl with
- | LocalDef (_,ci,_) -> subst_projection fid subst ci
- | LocalAssum _ ->
+ | LocalDef (_,ci,_) -> subst_projection fid subst ci
+ | LocalAssum ({binder_relevance=rci},_) ->
(* [ccl] is defined in context [params;x:rp] *)
(* [ccl'] is defined in context [params;x:rp;x:rp] *)
let ccl' = liftn 1 2 ccl in
- let p = mkLambda (x, lift 1 rp, ccl') in
+ let p = mkLambda (x, lift 1 rp, ccl') in
let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
- let ci = Inductiveops.make_case_info env indsp LetStyle in
- mkCase (ci, p, mkRel 1, [|branch|])
- in
+ let ci = Inductiveops.make_case_info env indsp rci LetStyle in
+ (* Record projections have no is *)
+ mkCase (ci, p, mkRel 1, [|branch|])
+ in
let proj =
- it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
+ it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
let projtyp =
it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
try
@@ -416,8 +421,6 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
let primitive =
!primitive_flag &&
List.for_all (fun (_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data
- (* will warn_non_primitive_record in declare_projections if we try
- to declare a 0-field record *)
in
let mie =
{ mind_entry_params = params;
@@ -431,7 +434,9 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
in
let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
let impls = List.map (fun _ -> paramimpls, []) record_data in
- let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls in
+ let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls
+ ~primitive_expected:!primitive_flag
+ in
let map i (_, _, _, fieldimpls, fields, is_coe, coers) =
let rsp = (kn, i) in (* This is ind path of idstruc *)
let cstr = (rsp, 1) in
@@ -463,7 +468,9 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in
let data =
match fields with
- | [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def ->
+ | [LocalAssum ({binder_name=Name proj_name} as binder, field)
+ | LocalDef ({binder_name=Name proj_name} as binder, _, field)] when def ->
+ let binder = {binder with binder_name=Name binder_name} in
let class_body = it_mkLambda_or_LetIn field params in
let class_type = it_mkProd_or_LetIn arity params in
let class_entry =
@@ -477,18 +484,18 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
in
let cstu = (cst, inst) in
let inst_type = appvectc (mkConstU cstu)
- (Termops.rel_vect 0 (List.length params)) in
+ (Termops.rel_vect 0 (List.length params)) in
let proj_type =
- it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in
+ it_mkProd_or_LetIn (mkProd(binder, inst_type, lift 1 field)) params in
let proj_body =
- it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in
+ it_mkLambda_or_LetIn (mkLambda (binder, inst_type, mkRel 1)) params in
let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in
let proj_cst = Declare.declare_constant proj_name
(DefinitionEntry proj_entry, IsDefinition Definition)
in
let cref = ConstRef cst in
- Impargs.declare_manual_implicits false cref [paramimpls];
- Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
+ Impargs.declare_manual_implicits false cref paramimpls;
+ Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
Classes.set_typeclass_transparency (EvalConstRef cst) false false;
let sub = match List.hd coers with
| Some b -> Some ((if b then Backward else Forward), List.hd priorities)
@@ -548,12 +555,13 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
let add_constant_class env cst =
let ty, univs = Typeops.type_of_global_in_context env (ConstRef cst) in
+ let r = (Environ.lookup_constant cst env).const_relevance in
let ctx, arity = decompose_prod_assum ty in
let tc =
{ cl_univs = univs;
cl_impl = ConstRef cst;
cl_context = (List.map (const None) ctx, ctx);
- cl_props = [LocalAssum (Anonymous, arity)];
+ cl_props = [LocalAssum (make_annot Anonymous r, arity)];
cl_projs = [];
cl_strict = !typeclasses_strict;
cl_unique = !typeclasses_unique
@@ -570,10 +578,11 @@ let add_inductive_class env ind =
let env = push_rel_context ctx env in
let inst = Univ.make_abstract_instance univs in
let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in
+ let r = Inductive.relevance_of_inductive env ind in
{ cl_univs = univs;
cl_impl = IndRef ind;
cl_context = List.map (const None) ctx, ctx;
- cl_props = [LocalAssum (Anonymous, ty)];
+ cl_props = [LocalAssum (make_annot Anonymous r, ty)];
cl_projs = [];
cl_strict = !typeclasses_strict;
cl_unique = !typeclasses_unique }
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index ed93267665..60b0bdc7e7 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -196,8 +196,8 @@ let init_tag_map styles =
let default_styles () =
init_tag_map (default_tag_map ())
-let parse_color_config file =
- let styles = Terminal.parse file in
+let parse_color_config str =
+ let styles = Terminal.parse str in
init_tag_map styles
let dump_tags () = CString.Map.bindings !tag_map
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d511bcd4fd..4250ddb02c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -16,7 +16,6 @@ open CAst
open Util
open Names
open Nameops
-open Term
open Tacmach
open Constrintern
open Prettyp
@@ -32,6 +31,7 @@ open Lemmas
open Locality
open Attributes
+module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
(** TODO: make this function independent of Ltac *)
@@ -133,22 +133,23 @@ let show_intro all =
*)
let make_cases_aux glob_ref =
+ let open Declarations in
match glob_ref with
| Globnames.IndRef ind ->
- let {Declarations.mind_nparams = np} , {Declarations.mind_nf_lc = tarr} = Global.lookup_inductive ind in
+ let mib, mip = Global.lookup_inductive ind in
Util.Array.fold_right_i
- (fun i typ l ->
- let al = List.rev (fst (decompose_prod typ)) in
- let al = Util.List.skipn np al in
+ (fun i (ctx, _) l ->
+ let al = Util.List.skipn (List.length mib.mind_params_ctxt) (List.rev ctx) in
let rec rename avoid = function
| [] -> []
- | (n,_)::l ->
- let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in
- Id.to_string n' :: rename (Id.Set.add n' avoid) l in
+ | RelDecl.LocalDef _ :: l -> "_" :: rename avoid l
+ | RelDecl.LocalAssum (n, _)::l ->
+ let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n.Context.binder_name avoid in
+ Id.to_string n' :: rename (Id.Set.add n' avoid) l in
let al' = rename Id.Set.empty al in
let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
(Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
- tarr []
+ mip.mind_nf_lc []
| _ -> raise Not_found
let make_cases s =
@@ -542,7 +543,7 @@ let vernac_definition_hook p = function
| Coercion ->
Some (Class.add_coercion_hook p)
| CanonicalStructure ->
- Some (Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure))
+ Some (Lemmas.mk_hook (fun _ _ _ -> Recordops.declare_canonical_structure))
| SubClass ->
Some (Class.add_subclass_hook p)
| _ -> None
@@ -1173,14 +1174,6 @@ let vernac_syntactic_definition ~module_local lid x y =
Dumpglob.dump_definition lid false "syndef";
Metasyntax.add_syntactic_definition (Global.env()) lid.v x module_local y
-let vernac_declare_implicits ~section_local r l =
- match l with
- | [] ->
- Impargs.declare_implicits section_local (smart_global r)
- | _::_ as imps ->
- Impargs.declare_manual_implicits section_local (smart_global r) ~enriching:false
- (List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
-
let warn_arguments_assert =
CWarnings.create ~name:"arguments-assert" ~category:"vernacular"
(fun sr ->
@@ -1336,43 +1329,15 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
user_err (strbrk "Some argument names are duplicated: " ++ duplicates)
end;
- (* Parts of this code are overly complicated because the implicit arguments
- API is completely crazy: positions (ExplByPos) are elaborated to
- names. This is broken by design, since not all arguments have names. So
- even though we eventually want to map only positions to implicit statuses,
- we have to check whether the corresponding arguments have names, not to
- trigger an error in the impargs code. Even better, the names we have to
- check are not the current ones (after previous renamings), but the original
- ones (inferred from the type). *)
-
let implicits =
List.map (fun { name; implicit_status = i } -> (name,i)) args
in
let implicits = implicits :: more_implicits in
- let open Vernacexpr in
- let rec build_implicits inf_names implicits =
- match inf_names, implicits with
- | _, [] -> []
- | _ :: inf_names, (_, NotImplicit) :: implicits ->
- build_implicits inf_names implicits
-
- (* With the current impargs API, it is impossible to make an originally
- anonymous argument implicit *)
- | Anonymous :: _, (name, _) :: _ ->
- user_err ~hdr:"vernac_declare_arguments"
- (strbrk"Argument "++ Name.print name ++
- strbrk " cannot be declared implicit.")
-
- | Name id :: inf_names, (name, impl) :: implicits ->
- let max = impl = MaximallyImplicit in
- (ExplByName id,max,false) :: build_implicits inf_names implicits
-
- | _ -> assert false (* already checked in [names_union] *)
- in
-
- let implicits = List.map (build_implicits inf_names) implicits in
- let implicits_specified = match implicits with [[]] -> false | _ -> true in
+ let implicits = List.map (List.map snd) implicits in
+ let implicits_specified = match implicits with
+ | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l
+ | _ -> true in
if implicits_specified && clear_implicits_flag then
user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations");
@@ -1415,10 +1380,10 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
end;
if implicits_specified || clear_implicits_flag then
- vernac_declare_implicits ~section_local reference implicits;
+ Impargs.set_implicits section_local (smart_global reference) implicits;
if default_implicits_flag then
- vernac_declare_implicits ~section_local reference [];
+ Impargs.declare_implicits section_local (smart_global reference);
if red_modifiers_specified then begin
match sr with
@@ -1459,6 +1424,14 @@ let vernac_generalizable ~local =
let () =
declare_bool_option
{ optdepr = false;
+ optname = "allow sprop";
+ optkey = ["Allow";"StrictProp"];
+ optread = (fun () -> Global.sprop_allowed());
+ optwrite = Global.set_allow_sprop }
+
+let () =
+ declare_bool_option
+ { optdepr = false;
optname = "silent";
optkey = ["Silent"];
optread = (fun () -> !Flags.quiet);
@@ -2377,6 +2350,8 @@ let locate_if_not_already ?loc (e, info) =
exception HasNotFailed
exception HasFailed of Pp.t
+let test_mode = ref false
+
(* XXX STATE: this type hints that restoring the state should be the
caller's responsibility *)
let with_fail st b f =
@@ -2402,7 +2377,7 @@ let with_fail st b f =
| HasNotFailed ->
user_err ~hdr:"Fail" (str "The command has not failed!")
| HasFailed msg ->
- if not !Flags.quiet || !Flags.test_mode then Feedback.msg_info
+ if not !Flags.quiet || !test_mode then Feedback.msg_info
(str "The command has indeed failed with message:" ++ fnl () ++ msg)
| _ -> assert false
end
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 4fbd3849b0..f43cec48e9 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -41,3 +41,7 @@ val command_focus : unit Proof.focus_kind
val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
Evd.evar_map * Redexpr.red_expr) Hook.t
+
+(* Flag set when the test-suite is called. Its only effect to display
+ verbose information for `Fail` *)
+val test_mode : bool ref
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 2eb901890b..d1da7c0602 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -237,13 +237,11 @@ type vernac_cumulative = VernacCumulative | VernacNonCumulative
(** {6 The type of vernacular expressions} *)
-type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
-
type vernac_argument_status = {
name : Name.t;
recarg_like : bool;
notation_scope : string CAst.t option;
- implicit_status : vernac_implicit_status;
+ implicit_status : Impargs.implicit_kind;
}
type extend_name =
@@ -355,7 +353,7 @@ type nonrec vernac_expr =
onlyparsing_flag
| VernacArguments of qualid or_by_notation *
vernac_argument_status list (* Main arguments status list *) *
- (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) *
+ (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
int option (* Number of args to trigger reduction *) *
[ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
`ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
@@ -409,3 +407,9 @@ type vernac_control =
| VernacRedirect of string * vernac_control CAst.t
| VernacTimeout of int * vernac_control
| VernacFail of vernac_control
+
+(** Deprecated *)
+
+type vernac_implicit_status = Impargs.implicit_kind =
+ | Implicit [@ocaml.deprecated] | MaximallyImplicit [@ocaml.deprecated] | NotImplicit [@ocaml.deprecated]
+[@@ocaml.deprecated "Use [Impargs.implicit_kind]"]
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index f5cf3401d0..4bfe5c66b5 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -235,7 +235,7 @@ type 'a argument_rule =
| Arg_rules of 'a Extend.production_rule list
type 'a vernac_argument = {
- arg_printer : 'a -> Pp.t;
+ arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
arg_parsing : 'a argument_rule;
}
@@ -251,6 +251,6 @@ let vernac_argument_extend ~name arg =
e
in
let pr = arg.arg_printer in
- let pr x = Genprint.PrinterBasic (fun () -> pr x) in
+ let pr x = Genprint.PrinterBasic (fun env sigma -> pr env sigma x) in
let () = Genprint.register_vernac_print0 wit pr in
(wit, entry)
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 118907c31b..4d89eaffd9 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -109,7 +109,7 @@ type 'a argument_rule =
entries instead of ty_user_symbol and thus arguments as roots. *)
type 'a vernac_argument = {
- arg_printer : 'a -> Pp.t;
+ arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
arg_parsing : 'a argument_rule;
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 06:04:17 +0000