aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml18
-rw-r--r--vernac/attributes.ml2
-rw-r--r--vernac/auto_ind_decl.ml6
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/comArguments.ml2
-rw-r--r--vernac/comArguments.mli2
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/comCoercion.ml7
-rw-r--r--vernac/comInductive.ml34
-rw-r--r--vernac/comInductive.mli8
-rw-r--r--vernac/comProgramFixpoint.ml2
-rw-r--r--vernac/declareObl.ml3
-rw-r--r--vernac/egramcoq.ml83
-rw-r--r--vernac/g_vernac.mlg55
-rw-r--r--vernac/himsg.ml14
-rw-r--r--vernac/indschemes.ml6
-rw-r--r--vernac/lemmas.ml1
-rw-r--r--vernac/metasyntax.ml127
-rw-r--r--vernac/mltop.ml27
-rw-r--r--vernac/ppvernac.ml42
-rw-r--r--vernac/prettyp.ml14
-rw-r--r--vernac/proof_using.ml2
-rw-r--r--vernac/record.ml8
-rw-r--r--vernac/vernacentries.ml119
-rw-r--r--vernac/vernacexpr.ml16
-rw-r--r--vernac/vernacinterp.ml2
26 files changed, 313 insertions, 291 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index dacef1cb18..46f616c4ff 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -239,10 +239,17 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
in
(* Build the context of all arities *)
let arities_ctx =
- let global_env = Global.env () in
+ let instance =
+ let open Univ in
+ Instance.of_array
+ (Array.init
+ (AUContext.size
+ (Declareops.inductive_polymorphic_context mib))
+ Level.var)
+ in
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 pspecif = ((mib, oib), instance) in
+ let ind_type = Inductive.type_of_inductive pspecif in
let indr = oib.mind_relevance in
let ind_name = Name oib.mind_typename in
Context.Rel.add (Context.Rel.Declaration.LocalAssum (make_annot ind_name indr, ind_type)) accu)
@@ -356,8 +363,5 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu
in
- if not mind.mind_typing_flags.check_template then
- let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
- ContextObjectMap.add (Axiom (TemplatePolymorphic m, l)) Constr.mkProp accu
- else accu
+ accu
in GlobRef.Map_env.fold fold graph ContextObjectMap.empty
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 68d2c3a00d..194308b77f 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -154,7 +154,6 @@ let program_mode = ref false
let () = let open Goptions in
declare_bool_option
{ optdepr = false;
- optname = "use of the program extension";
optkey = program_mode_option_name;
optread = (fun () -> !program_mode);
optwrite = (fun b -> program_mode:=b) }
@@ -188,7 +187,6 @@ let is_universe_polymorphism =
let () = let open Goptions in
declare_bool_option
{ optdepr = false;
- optname = "universe polymorphism";
optkey = universe_polymorphism_option_name;
optread = (fun () -> !b);
optwrite = ((:=) b) }
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f954915cf8..bdf8511cce 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -178,7 +178,7 @@ let build_beq_scheme mode kn =
(* current inductive we are working on *)
let cur_packet = mib.mind_packets.(snd (fst ind)) in
(* Inductive toto : [rettyp] := *)
- let rettyp = Inductive.type_of_inductive env ((mib,cur_packet),u) in
+ let rettyp = Inductive.type_of_inductive ((mib,cur_packet),u) in
(* split rettyp in a list without the non rec params and the last ->
e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *)
let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in
@@ -395,7 +395,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
in
Proofview.Goal.enter begin fun gl ->
- let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in
+ let type_of_pq = Tacmach.New.pf_get_type_of gl p in
let sigma = Tacmach.New.project gl in
let env = Tacmach.New.pf_env gl in
let u,v = destruct_ind env sigma type_of_pq
@@ -458,11 +458,11 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
match (l1,l2) with
| (t1::q1,t2::q2) ->
Proofview.Goal.enter begin fun gl ->
- let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
let sigma = Tacmach.New.project gl in
let env = Tacmach.New.pf_env gl in
if EConstr.eq_constr sigma t1 t2 then aux q1 q2
else (
+ let tt1 = Tacmach.New.pf_get_type_of gl t1 in
let u,v = try destruct_ind env sigma tt1
(* trick so that the good sequence is returned*)
with e when CErrors.noncritical e -> indu,[||]
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 77bc4e4f8a..b92c9e9b71 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -510,7 +510,7 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri
let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
let tclass =
- if generalize then CAst.make @@ CGeneralization (Glob_term.Implicit, Some AbsPi, tclass)
+ if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass)
else tclass
in
let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
index 15077298aa..9d43debb77 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -228,7 +228,7 @@ let vernac_arguments ~section_local reference args more_implicits flags =
let implicits = List.map (List.map snd) implicits in
let implicits_specified = match implicits with
- | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l
+ | [l] -> List.exists (function Glob_term.Explicit -> false | _ -> true) l
| _ -> true in
if implicits_specified && clear_implicits_flag then
diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli
index 71effddf67..cbc5fc15e2 100644
--- a/vernac/comArguments.mli
+++ b/vernac/comArguments.mli
@@ -12,6 +12,6 @@ val vernac_arguments
: section_local:bool
-> Libnames.qualid Constrexpr.or_by_notation
-> Vernacexpr.vernac_argument_status list
- -> (Names.Name.t * Impargs.implicit_kind) list list
+ -> (Names.Name.t * Glob_term.binding_kind) list list
-> Vernacexpr.arguments_modifier list
-> unit
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 625ffb5a06..d97bf6724c 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -270,7 +270,7 @@ let context ~poly l =
| Some (Name id',_) -> Id.equal name id'
| _ -> false
in
- let impl = Glob_term.(if List.exists test impls then Implicit else Explicit) in
+ let impl = Glob_term.(if List.exists test impls then MaxImplicit else Explicit) in (* ??? *)
name,b,t,impl)
ctx
in
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index 56ab6f289d..2c582da495 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -198,10 +198,9 @@ let build_id_coercion idf_opt source poly =
lams
in
(* juste pour verification *)
- let _ =
- if not
- (Reductionops.is_conv_leq env sigma
- (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f)) (EConstr.of_constr typ_f))
+ let sigma, val_t = Typing.type_of env sigma (EConstr.of_constr val_f) in
+ let () =
+ if not (Reductionops.is_conv_leq env sigma val_t (EConstr.of_constr typ_f))
then
user_err (strbrk
"Cannot be defined as coercion (maybe a bad number of arguments).")
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 8de1c69424..85f2bf3708 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -42,7 +42,6 @@ let should_auto_template =
let auto = ref true in
let () = declare_bool_option
{ optdepr = false;
- optname = "Automatically make some inductive types template polymorphic";
optkey = ["Auto";"Template";"Polymorphism"];
optread = (fun () -> !auto);
optwrite = (fun b -> auto := b); }
@@ -323,16 +322,15 @@ let check_named {CAst.loc;v=na} = match na with
let msg = str "Parameters must be named." in
user_err ?loc msg
-let template_polymorphism_candidate ~template_check ~ctor_levels uctx params concl =
+let template_polymorphism_candidate ~ctor_levels uctx params concl =
match uctx with
| Entries.Monomorphic_entry uctx ->
let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in
if not concltemplate then false
- else if not template_check then true
else
let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in
let params, conclunivs =
- IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu
+ IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu
in
not (Univ.LSet.is_empty conclunivs)
| Entries.Polymorphic_entry _ -> false
@@ -385,7 +383,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames
List.fold_left (fun levels c -> add_levels c levels)
param_levels ctypes
in
- template_polymorphism_candidate ~template_check:(Environ.check_template env_ar_params) ~ctor_levels uctx ctx_params concl
+ template_polymorphism_candidate ~ctor_levels uctx ctx_params concl
in
let template = match template with
| Some template ->
@@ -458,9 +456,19 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities 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 lift1_ctx ctx =
+ let t = EConstr.it_mkProd_or_LetIn EConstr.mkProp ctx in
+ let t = EConstr.Vars.lift 1 t in
+ let ctx, _ = EConstr.decompose_prod_assum sigma t in
+ ctx
+ in
+ let ctx_params_lifted, fullarities = CList.fold_left_map
+ (fun ctx_params c -> lift1_ctx ctx_params, EConstr.it_mkProd_or_LetIn c ctx_params)
+ 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
+ let env_ar_params = EConstr.push_rel_context ctx_params_lifted env_ar in
(* Compute interpretation metadatas *)
let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in
@@ -511,6 +519,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let eq_local_binders bl1 bl2 =
List.equal local_binder_eq bl1 bl2
+let eq_params (up1,p1) (up2,p2) =
+ eq_local_binders up1 up2 && Option.equal eq_local_binders p1 p2
+
let extract_coercions indl =
let mkqid (_,({CAst.v=id},_)) = qualid_of_ident id in
let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in
@@ -521,7 +532,7 @@ let extract_params indl =
match paramsl with
| [] -> anomaly (Pp.str "empty list of inductive types.")
| params::paramsl ->
- if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str
+ if not (List.for_all (eq_params params) paramsl) then user_err Pp.(str
"Parameters should be syntactically the same for each inductive type.");
params
@@ -546,7 +557,12 @@ type uniform_inductive_flag =
let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite =
let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
(* Interpret the types *)
- let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in
+ let indl = match params with
+ | uparams, Some params -> (uparams, params, indl)
+ | params, None -> match uniform with
+ | UniformParameters -> (params, [], indl)
+ | NonUniformParameters -> ([], params, indl)
+ in
let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in
(* Declare the mutual inductive block with its associated schemes *)
ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls);
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index cc104b3762..1286e4a5c3 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -76,17 +76,15 @@ val should_auto_template : Id.t -> bool -> bool
inductive under consideration. *)
val template_polymorphism_candidate
- : template_check:bool
- -> ctor_levels:Univ.LSet.t
+ : ctor_levels:Univ.LSet.t
-> Entries.universes_entry
-> Constr.rel_context
-> Sorts.t option
-> bool
-(** [template_polymorphism_candidate ~template_check ~ctor_levels uctx params
+(** [template_polymorphism_candidate ~ctor_levels uctx params
conclsort] is [true] iff an inductive with params [params],
conclusion [conclsort] and universe levels appearing in the
constructor arguments [ctor_levels] would be definable as template
polymorphic. It should have at least one universe in its
monomorphic universe context that can be made parametric in its
- conclusion sort, if one is given. If the [template_check] flag is
- false we just check that the conclusion sort is not small. *)
+ conclusion sort, if one is given. *)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index d48e2139d1..84f8578ad4 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -127,7 +127,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
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
- let relty = Typing.unsafe_type_of env sigma rel in
+ let relty = Retyping.get_type_of env sigma rel in
let relargty =
let error () =
user_err ?loc:(constr_loc r)
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index b56b9c8ce2..dcb28b898f 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -56,7 +56,7 @@ type program_info =
let get_shrink_obligations =
Goptions.declare_bool_option_and_ref ~depr:true (* remove in 8.8 *)
- ~name:"Shrinking of Program obligations" ~key:["Shrink"; "Obligations"]
+ ~key:["Shrink"; "Obligations"]
~value:true
(* XXX: Is this the right place for this? *)
@@ -133,7 +133,6 @@ let add_hint local prg cst =
let get_hide_obligations =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"Hidding of Program obligations"
~key:["Hide"; "Obligations"]
~value:false
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 07656f9715..3181bcc4bc 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -200,41 +200,44 @@ let assoc_eq al ar =
| LeftA, LeftA -> true
| _, _ -> false
-(* [adjust_level assoc from prod] where [assoc] and [from] are the name
+(** [adjust_level assoc from prod] where [assoc] and [from] are the name
and associativity of the level where to add the rule; the meaning of
the result is
- None = SELF
- Some None = NEXT
- Some (Some (n,cur)) = constr LEVEL n
- s.t. if [cur] is set then [n] is the same as the [from] level *)
-let adjust_level assoc from = let open Gramlib.Gramext in function
+ DefaultLevel = entry name
+ NextLevel = NEXT
+ NumLevel n = constr LEVEL n *)
+let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in match p with
+(* If a level in a different grammar, no other choice than denoting it by absolute level *)
+ | (NumLevel n,_) when not (Notation.notation_entry_eq custom custom') -> NumLevel n
+(* If a default level in a different grammar, the entry name is ok *)
+ | (DefaultLevel,InternalProd) ->
+ if Notation.notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel
+ | (DefaultLevel,BorderProd _) when not (Notation.notation_entry_eq custom custom') ->
+ if Notation.notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel
(* Associativity is None means force the level *)
- | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true))
+ | (NumLevel n,BorderProd (_,None)) -> NumLevel n
+ | (DefaultLevel,BorderProd (_,None)) -> assert false
(* Compute production name on the right side *)
(* If NonA or LeftA on the right-hand side, set to NEXT *)
- | (NumLevel n,BorderProd (Right,Some (NonA|LeftA))) ->
- Some None
+ | ((NumLevel _ | DefaultLevel),BorderProd (Right,Some (NonA|LeftA))) -> NextLevel
(* If RightA on the right-hand side, set to the explicit (current) level *)
- | (NumLevel n,BorderProd (Right,Some RightA)) ->
- Some (Some (n,true))
+ | (NumLevel n,BorderProd (Right,Some RightA)) -> NumLevel n
+ | (DefaultLevel,BorderProd (Right,Some RightA)) -> NumLevel from
(* Compute production name on the left side *)
(* If NonA on the left-hand side, adopt the current assoc ?? *)
- | (NumLevel n,BorderProd (Left,Some NonA)) -> None
+ | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some NonA)) -> DefaultLevel
(* If the expected assoc is the current one, set to SELF *)
- | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) ->
- None
+ | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) ->
+ DefaultLevel
(* Otherwise, force the level, n or n-1, according to expected assoc *)
- | (NumLevel n,BorderProd (Left,Some a)) ->
- begin match a with
- | LeftA -> Some (Some (n, true))
- | _ -> Some None
- end
+ | (NumLevel n,BorderProd (Left,Some LeftA)) -> NumLevel n
+ | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some _)) -> NextLevel
(* None means NEXT *)
- | (NextLevel,_) -> Some None
+ | (NextLevel,_) -> assert (Notation.notation_entry_eq custom custom'); NextLevel
(* Compute production name elsewhere *)
| (NumLevel n,InternalProd) ->
- if from = n + 1 then Some None else Some (Some (n, Int.equal n from))
+ if from = n + 1 then NextLevel else NumLevel n
type _ target =
| ForConstr : constr_expr target
@@ -311,13 +314,14 @@ let target_entry : type s. notation_entry -> s target -> s Entry.t = function
| ForConstr -> entry_for_constr
| ForPattern -> entry_for_patttern
-let is_self from e = match e with
+let is_self custom (custom',from) e = Notation.notation_entry_eq custom custom' && match e with
| (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false
| (NumLevel n, BorderProd (Left, _)) -> Int.equal from n
| _ -> false
-let is_binder_level from e = match e with
-| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) -> from = 200
+let is_binder_level custom (custom',from) e = match e with
+| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) ->
+ custom = InConstrEntry && custom' = InConstrEntry && from = 200
| _ -> false
let make_sep_rules = function
@@ -338,15 +342,15 @@ type ('s, 'a) mayrec_symbol =
| MayRecMay : ('s, mayrec, 'a) symbol -> ('s, 'a) mayrec_symbol
let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat ->
- if custom = InConstrEntry && is_binder_level from p then MayRecNo (Aentryl (target_entry InConstrEntry forpat, "200"))
- else if is_self from p then MayRecMay Aself
+ if is_binder_level custom from p then (* Prevent self *) MayRecNo (Aentryl (target_entry custom forpat, "200"))
+ else if is_self custom from p then MayRecMay Aself
else
let g = target_entry custom forpat in
- let lev = adjust_level assoc from p in
+ let lev = adjust_level custom assoc from p in
begin match lev with
- | None -> MayRecNo (Aentry g)
- | Some None -> MayRecMay Anext
- | Some (Some (lev, cur)) -> MayRecNo (Aentryl (g, string_of_int lev))
+ | DefaultLevel -> MayRecNo (Aentry g)
+ | NextLevel -> MayRecMay Anext
+ | NumLevel lev -> MayRecNo (Aentryl (g, string_of_int lev))
end
let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with
@@ -503,19 +507,24 @@ let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
let empty = (pos, [(name, p4assoc, [])]) in
ExtendRule (target_entry where forpat, reinit, empty)
-let rec pure_sublevels' custom assoc from forpat level = function
+let different_levels (custom,opt_level) (custom',string_level) =
+ match opt_level with
+ | None -> true
+ | Some level -> not (Notation.notation_entry_eq custom custom') || level <> int_of_string string_level
+
+let rec pure_sublevels' assoc from forpat level = function
| [] -> []
| GramConstrNonTerminal (e,_) :: rem ->
- let rem = pure_sublevels' custom assoc from forpat level rem in
+ let rem = pure_sublevels' assoc from forpat level rem in
let push where p rem =
- match symbol_of_target custom p assoc from forpat with
- | MayRecNo (Aentryl (_,i)) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem
+ match symbol_of_target where p assoc from forpat with
+ | MayRecNo (Aentryl (_,i)) when different_levels (fst from,level) (where,i) -> (where,int_of_string i) :: rem
| _ -> rem in
(match e with
| ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem
| ETProdConstr (s,p) -> push s p rem
| _ -> rem)
-| (GramConstrTerminal _ | GramConstrListMark _) :: rem -> pure_sublevels' custom assoc from forpat level rem
+| (GramConstrTerminal _ | GramConstrListMark _) :: rem -> pure_sublevels' assoc from forpat level rem
let make_act : type r. r target -> _ -> r gen_eval = function
| ForConstr -> fun notation loc env ->
@@ -530,8 +539,8 @@ let extend_constr state forpat ng =
let assoc = ng.notgram_assoc in
let (entry, level) = interp_constr_entry_key custom forpat n in
let fold (accu, state) pt =
- let AnyTyRule r = make_ty_rule assoc n forpat pt in
- let pure_sublevels = pure_sublevels' custom assoc n forpat level pt in
+ let AnyTyRule r = make_ty_rule assoc (custom,n) forpat pt in
+ let pure_sublevels = pure_sublevels' assoc (custom,n) forpat level pt in
let isforpat = target_to_bool forpat in
let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
let (pos,p4assoc,name,reinit), state = find_position state custom isforpat assoc level in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3302231fd1..d597707d12 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -16,13 +16,11 @@ open Util
open Names
open Glob_term
open Vernacexpr
-open Impargs
open Constrexpr
open Constrexpr_ops
open Extend
open Decls
open Declaremods
-open Declarations
open Namegen
open Tok (* necessary for camlp5 *)
@@ -201,9 +199,7 @@ GRAMMAR EXTEND Gram
(* Gallina inductive declarations *)
| cum = OPT cumulativity_token; priv = private_token; f = finite_token;
indl = LIST1 inductive_definition SEP "with" ->
- { let (k,f) = f in
- let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
- VernacInductive (cum, priv,f,indl) }
+ { VernacInductive (cum, priv, f, indl) }
| "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
{ VernacFixpoint (NoDischarge, recs) }
| IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
@@ -338,12 +334,12 @@ GRAMMAR EXTEND Gram
] ]
;
finite_token:
- [ [ IDENT "Inductive" -> { (Inductive_kw,Finite) }
- | IDENT "CoInductive" -> { (CoInductive,CoFinite) }
- | IDENT "Variant" -> { (Variant,BiFinite) }
- | IDENT "Record" -> { (Record,BiFinite) }
- | IDENT "Structure" -> { (Structure,BiFinite) }
- | IDENT "Class" -> { (Class true,BiFinite) } ] ]
+ [ [ IDENT "Inductive" -> { Inductive_kw }
+ | IDENT "CoInductive" -> { CoInductive }
+ | IDENT "Variant" -> { Variant }
+ | IDENT "Record" -> { Record }
+ | IDENT "Structure" -> { Structure }
+ | IDENT "Class" -> { Class true } ] ]
;
cumulativity_token:
[ [ IDENT "Cumulative" -> { VernacCumulative }
@@ -399,9 +395,10 @@ GRAMMAR EXTEND Gram
;
inductive_definition:
[ [ oc = opt_coercion; id = ident_decl; indpar = binders;
+ extrapar = OPT [ "|"; p = binders -> { p } ];
c = OPT [ ":"; c = lconstr -> { c } ];
lc=opt_constructors_or_fields; ntn = decl_notation ->
- { (((oc,id),indpar,c,lc),ntn) } ] ]
+ { (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ]
;
constructor_list_or_record_decl:
[ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l }
@@ -817,7 +814,7 @@ GRAMMAR EXTEND Gram
{ let name, recarg_like, notation_scope = item in
[RealArg { name=name; recarg_like=recarg_like;
notation_scope=notation_scope;
- implicit_status = NotImplicit}] }
+ implicit_status = Explicit}] }
| "/" -> { [VolatileArg] }
| "&" -> { [BidiArg] }
| "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter ->
@@ -827,7 +824,7 @@ GRAMMAR EXTEND Gram
List.map (fun (name,recarg_like,notation_scope) ->
RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
- implicit_status = NotImplicit}) items }
+ implicit_status = Explicit}) items }
| "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter ->
{ let f x = match sc, x with
| None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
@@ -835,7 +832,7 @@ GRAMMAR EXTEND Gram
List.map (fun (name,recarg_like,notation_scope) ->
RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
- implicit_status = Implicit}) items }
+ implicit_status = NonMaxImplicit}) items }
| "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter ->
{ let f x = match sc, x with
| None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
@@ -843,16 +840,16 @@ GRAMMAR EXTEND Gram
List.map (fun (name,recarg_like,notation_scope) ->
RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
- implicit_status = MaximallyImplicit}) items }
+ implicit_status = MaxImplicit}) items }
]
];
(* Same as [argument_spec_block], but with only implicit status and names *)
more_implicits_block: [
- [ name = name -> { [(name.CAst.v, NotImplicit)] }
+ [ name = name -> { [(name.CAst.v, Explicit)] }
| "["; items = LIST1 name; "]" ->
- { List.map (fun name -> (name.CAst.v, Impargs.Implicit)) items }
+ { List.map (fun name -> (name.CAst.v, NonMaxImplicit)) items }
| "{"; items = LIST1 name; "}" ->
- { List.map (fun name -> (name.CAst.v, MaximallyImplicit)) items }
+ { List.map (fun name -> (name.CAst.v, MaxImplicit)) items }
]
];
strategy_level:
@@ -1228,11 +1225,10 @@ GRAMMAR EXTEND Gram
| { CAst.v = k }, Some s -> SetFormat(k,s)
| s, None -> SetFormat ("text",s) end }
| x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at";
- lev = level -> { SetItemLevel (x::l,None,Some lev) }
- | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],None,Some lev) }
- | x = IDENT; "at"; lev = level; b = constr_as_binder_kind ->
- { SetItemLevel ([x],Some b,Some lev) }
- | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,None) }
+ lev = level -> { SetItemLevel (x::l,None,lev) }
+ | x = IDENT; "at"; lev = level; b = OPT constr_as_binder_kind ->
+ { SetItemLevel ([x],b,lev) }
+ | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,DefaultLevel) }
| x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) }
] ]
;
@@ -1240,19 +1236,20 @@ GRAMMAR EXTEND Gram
[ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
| IDENT "bigint" -> { ETBigint }
| IDENT "binder" -> { ETBinder true }
- | IDENT "constr" -> { ETConstr (InConstrEntry,None,None) }
- | IDENT "constr"; n = OPT at_level; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
+ | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) }
+ | IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
| IDENT "pattern" -> { ETPattern (false,None) }
| IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (false,Some n) }
| IDENT "strict"; IDENT "pattern" -> { ETPattern (true,None) }
| IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (true,Some n) }
| IDENT "closed"; IDENT "binder" -> { ETBinder false }
- | IDENT "custom"; x = IDENT; n = OPT at_level; b = OPT constr_as_binder_kind ->
+ | IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT constr_as_binder_kind ->
{ ETConstr (InCustomEntry x,b,n) }
] ]
;
- at_level:
- [ [ "at"; n = level -> { n } ] ]
+ at_level_opt:
+ [ [ "at"; n = level -> { n }
+ | -> { DefaultLevel } ] ]
;
constr_as_binder_kind:
[ [ "as"; IDENT "ident" -> { Notation_term.AsIdent }
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index eb39564fed..dfc4631572 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -201,9 +201,7 @@ let explain_bad_assumption env sigma j =
str "because this term is not a type."
let explain_reference_variables sigma id c =
- (* c is intended to be a global reference *)
- let pc = pr_global (fst (Termops.global_of_constr sigma c)) in
- pc ++ strbrk " depends on the variable " ++ Id.print id ++
+ pr_global c ++ strbrk " depends on the variable " ++ Id.print id ++
strbrk " which is not declared in the context."
let rec pr_disjunction pr = function
@@ -1216,8 +1214,12 @@ let error_bad_entry () =
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 constraints declared for inductive type."
+let error_inductive_missing_constraints (us,ind_univ) =
+ let pr_u = Univ.Universe.pr_with UnivNames.pr_with_global_universes in
+ str "Missing universe constraint declared for inductive type:" ++ spc()
+ ++ v 0 (prlist_with_sep spc (fun u ->
+ hov 0 (pr_u u ++ str " <= " ++ pr_u ind_univ))
+ (Univ.Universe.Set.elements us))
(* Recursion schemes errors *)
@@ -1256,7 +1258,7 @@ let explain_inductive_error = function
| BadEntry -> error_bad_entry ()
| LargeNonPropInductiveNotInType ->
error_large_non_prop_inductive_not_in_type ()
- | BadUnivs -> error_inductive_bad_univs ()
+ | MissingConstraints csts -> error_inductive_missing_constraints csts
(* Recursion schemes errors *)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 2f0b1062a7..227d2f1554 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -44,7 +44,6 @@ let elim_flag = ref true
let () =
declare_bool_option
{ optdepr = false;
- optname = "automatic declaration of induction schemes";
optkey = ["Elimination";"Schemes"];
optread = (fun () -> !elim_flag) ;
optwrite = (fun b -> elim_flag := b) }
@@ -53,7 +52,6 @@ let bifinite_elim_flag = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "automatic declaration of induction schemes for non-recursive types";
optkey = ["Nonrecursive";"Elimination";"Schemes"];
optread = (fun () -> !bifinite_elim_flag) ;
optwrite = (fun b -> bifinite_elim_flag := b) }
@@ -62,7 +60,6 @@ let case_flag = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "automatic declaration of case analysis schemes";
optkey = ["Case";"Analysis";"Schemes"];
optread = (fun () -> !case_flag) ;
optwrite = (fun b -> case_flag := b) }
@@ -71,7 +68,6 @@ let eq_flag = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "automatic declaration of boolean equality";
optkey = ["Boolean";"Equality";"Schemes"];
optread = (fun () -> !eq_flag) ;
optwrite = (fun b -> eq_flag := b) }
@@ -82,7 +78,6 @@ let eq_dec_flag = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "automatic declaration of decidable equality";
optkey = ["Decidable";"Equality";"Schemes"];
optread = (fun () -> !eq_dec_flag) ;
optwrite = (fun b -> eq_dec_flag := b) }
@@ -91,7 +86,6 @@ let rewriting_flag = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname ="automatic declaration of rewriting schemes for equality types";
optkey = ["Rewriting";"Schemes"];
optread = (fun () -> !rewriting_flag) ;
optwrite = (fun b -> rewriting_flag := b) }
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 865eded545..f7606f4ede 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -268,7 +268,6 @@ let warn_let_as_axiom =
let get_keep_admitted_vars =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"keep section variables in admitted proofs"
~key:["Keep"; "Admitted"; "Variables"]
~value:true
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 05e23164b1..7794b0a37a 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -126,7 +126,7 @@ let parse_format ({CAst.loc;v=str} : lstring) =
let rec parse_non_format i =
let n = nonspaces false 0 i in
push_token (make_loc i (i+n-1)) (UnpTerminal (String.sub str i n)) (parse_token 1 (i+n))
- and parse_quoted n i =
+ and parse_quoted n k i =
if i < len then match str.[i] with
(* Parse " // " *)
| '/' when i+1 < len && str.[i+1] == '/' ->
@@ -140,7 +140,7 @@ let parse_format ({CAst.loc;v=str} : lstring) =
(parse_token 1 (close_quotation i (i+p+1)))
| c ->
(* The spaces are real spaces *)
- push_white i n (match c with
+ push_white (i-n-1-k) n (match c with
| '[' ->
if i+1 < len then match str.[i+1] with
(* Parse " [h .. ", *)
@@ -177,7 +177,7 @@ let parse_format ({CAst.loc;v=str} : lstring) =
push_white (i-n) (n-k) (push_token (make_loc i (i+1)) (UnpTerminal "'") (parse_token 1 (i+1)))
(* Parse the beginning of a quoted expression *)
| '\'' ->
- parse_quoted (n-k) (i+1)
+ parse_quoted (n-k) k (i+1)
(* Otherwise *)
| _ ->
push_white (i-n) (n-k) (parse_non_format i)
@@ -297,7 +297,11 @@ let precedence_of_position_and_level from_level = function
n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp
| NumLevel n, InternalProd -> n, Prec n
| NextLevel, _ -> from_level, L
+ | DefaultLevel, _ ->
+ (* Fake value, waiting for PR#5 at herbelin's fork *) 200,
+ Any
+(** Computing precedences of subentries for parsing *)
let precedence_of_entry_type (from_custom,from_level) = function
| ETConstr (custom,_,x) when notation_entry_eq custom from_custom ->
precedence_of_position_and_level from_level x
@@ -309,6 +313,22 @@ let precedence_of_entry_type (from_custom,from_level) = function
| ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n
| _ -> 0, E (* should not matter *)
+(** Computing precedences for future insertion of parentheses at
+ the time of printing using hard-wired constr levels *)
+let unparsing_precedence_of_entry_type from_level = function
+ | ETConstr (InConstrEntry,_,x) ->
+ (* Possible insertion of parentheses at printing time to deal
+ with precedence in a constr entry is managed using [prec_less]
+ in [ppconstr.ml] *)
+ snd (precedence_of_position_and_level from_level x)
+ | ETConstr (custom,_,_) ->
+ (* Precedence of printing for a custom entry is managed using
+ explicit insertion of entry coercions at the time of building
+ a [constr_expr] *)
+ Any
+ | ETPattern (_,n) -> (* in constr *) Prec (match n with Some n -> n | None -> 0)
+ | _ -> Any (* should not matter *)
+
(* Some breaking examples *)
(* "x = y" : "x /1 = y" (breaks before any symbol) *)
(* "x =S y" : "x /1 =S /1 y" (protect from confusion; each side for symmetry)*)
@@ -374,7 +394,7 @@ let check_open_binder isopen sl m =
let unparsing_metavar i from typs =
let x = List.nth typs (i-1) in
- let prec = snd (precedence_of_entry_type from x) in
+ let prec = unparsing_precedence_of_entry_type from x in
match x with
| ETConstr _ | ETGlobal | ETBigint ->
UnpMetaVar (i,prec)
@@ -389,12 +409,12 @@ let unparsing_metavar i from typs =
let index_id id l = List.index Id.equal id l
-let make_hunks etyps symbols from =
+let make_hunks etyps symbols from_level =
let vars,typs = List.split etyps in
let rec make b = function
| NonTerminal m :: prods ->
let i = index_id m vars in
- let u = unparsing_metavar i from typs in
+ let u = unparsing_metavar i from_level typs in
if is_next_non_terminal b prods then
(None, u) :: add_break_if_none 1 b (make b prods)
else
@@ -428,7 +448,7 @@ let make_hunks etyps symbols from =
| SProdList (m,sl) :: prods ->
let i = index_id m vars in
let typ = List.nth typs (i-1) in
- let _,prec = precedence_of_entry_type from typ in
+ let prec = unparsing_precedence_of_entry_type from_level typ in
let sl' =
(* If no separator: add a break *)
if List.is_empty sl then add_break 1 []
@@ -477,6 +497,9 @@ let warn_format_break =
(fun () ->
strbrk "Discarding format implicitly indicated by multiple spaces in notation because an explicit format modifier is given.")
+let has_ldots l =
+ List.exists (function (_,UnpTerminal s) -> String.equal s (Id.to_string Notation_ops.ldots_var) | _ -> false) l
+
let rec split_format_at_ldots hd = function
| (loc,UnpTerminal s) :: fmt when String.equal s (Id.to_string Notation_ops.ldots_var) -> loc, List.rev hd, fmt
| u :: fmt ->
@@ -504,11 +527,32 @@ let find_prod_list_loc sfmt fmt =
(* A separator; we highlight the separating sequence *)
Loc.merge_opt (fst (List.hd sfmt)) (fst (List.last sfmt))
+let is_blank s =
+ let n = String.length s in
+ let rec aux i s = i >= n || s.[i] = ' ' && aux (i+1) s in
+ aux 0 s
+
+let is_formatting = function
+ | (_,UnpCut _) -> true
+ | (_,UnpTerminal s) -> is_blank s
+ | _ -> false
+
+let rec is_var_in_recursive_format = function
+ | (_,UnpTerminal s) when not (is_blank s) -> true
+ | (loc,UnpBox (b,l)) ->
+ (match List.filter (fun a -> not (is_formatting a)) l with
+ | [a] -> is_var_in_recursive_format a
+ | _ -> error_not_same ?loc ())
+ | _ -> false
+
+let rec check_eq_var_upto_name = function
+ | (_,UnpTerminal s1), (_,UnpTerminal s2) when not (is_blank s1 && is_blank s2) || s1 = s2 -> ()
+ | (_,UnpBox (b1,l1)), (_,UnpBox (b2,l2)) when b1 = b2 -> List.iter check_eq_var_upto_name (List.combine l1 l2)
+ | (_,UnpCut b1), (_,UnpCut b2) when b1 = b2 -> ()
+ | _, (loc,_) -> error_not_same ?loc ()
+
let skip_var_in_recursive_format = function
- | (_,UnpTerminal s) :: sl (* skip first var *) when not (List.for_all (fun c -> c = " ") (String.explode s)) ->
- (* To do, though not so important: check that the names match
- the names in the notation *)
- sl
+ | a :: sl when is_var_in_recursive_format a -> a, sl
| (loc,_) :: _ -> error_not_same ?loc ()
| [] -> assert false
@@ -516,17 +560,22 @@ let read_recursive_format sl fmt =
(* Turn [[UnpTerminal s :: some-list @ UnpTerminal ".." :: same-some-list @ UnpTerminal s' :: rest] *)
(* into [(some-list,rest)] *)
let get_head fmt =
- let sl = skip_var_in_recursive_format fmt in
- try split_format_at_ldots [] sl with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in
+ let var,sl = skip_var_in_recursive_format fmt in
+ try var, split_format_at_ldots [] sl
+ with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in
let rec get_tail = function
| (loc,a) :: sepfmt, (_,b) :: fmt when (=) a b -> get_tail (sepfmt, fmt) (* FIXME *)
| [], tail -> skip_var_in_recursive_format tail
| (loc,_) :: _, ([] | (_,UnpTerminal _) :: _)-> error_not_same ?loc ()
| _, (loc,_)::_ -> error_not_same ?loc () in
- let loc, slfmt, fmt = get_head fmt in
- slfmt, get_tail (slfmt, fmt)
-
-let hunks_of_format (from,(vars,typs)) symfmt =
+ let var1, (loc, slfmt, fmt) = get_head fmt in
+ let var2, res = get_tail (slfmt, fmt) in
+ check_eq_var_upto_name (var1,var2);
+ (* To do, though not so important: check that the names match
+ the names in the notation *)
+ slfmt, res
+
+let hunks_of_format (from_level,(vars,typs)) symfmt =
let rec aux = function
| symbs, (_,(UnpTerminal s' as u)) :: fmt
when String.equal s' (String.make (String.length s') ' ') ->
@@ -536,17 +585,13 @@ let hunks_of_format (from,(vars,typs)) symfmt =
let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
| NonTerminal s :: symbs, (_,UnpTerminal s') :: fmt when Id.equal s (Id.of_string s') ->
let i = index_id s vars in
- let symbs, l = aux (symbs,fmt) in symbs, unparsing_metavar i from typs :: l
- | symbs, (_,UnpBox (a,b)) :: fmt ->
- let symbs', b' = aux (symbs,b) in
- let symbs', l = aux (symbs',fmt) in
- symbs', UnpBox (a,List.map (fun x -> (None,x)) b') :: l
+ let symbs, l = aux (symbs,fmt) in symbs, unparsing_metavar i from_level typs :: l
| symbs, (_,(UnpCut _ as u)) :: fmt ->
let symbs, l = aux (symbs,fmt) in symbs, u :: l
- | SProdList (m,sl) :: symbs, fmt ->
+ | SProdList (m,sl) :: symbs, fmt when has_ldots fmt ->
let i = index_id m vars in
let typ = List.nth typs (i-1) in
- let _,prec = precedence_of_entry_type from typ in
+ let prec = unparsing_precedence_of_entry_type from_level typ in
let loc_slfmt,rfmt = read_recursive_format sl fmt in
let sl, slfmt = aux (sl,loc_slfmt) in
if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) ();
@@ -558,6 +603,10 @@ let hunks_of_format (from,(vars,typs)) symfmt =
UnpBinderListMetaVar (i,isopen,slfmt)
| _ -> assert false in
symbs, hunk :: l
+ | symbs, (_,UnpBox (a,b)) :: fmt ->
+ let symbs', b' = aux (symbs,b) in
+ let symbs', l = aux (symbs',fmt) in
+ symbs', UnpBox (a,List.map (fun x -> (None,x)) b') :: l
| symbs, [] -> symbs, []
| Break _ :: symbs, fmt -> warn_format_break (); aux (symbs,fmt)
| _, fmt -> error_format ?loc:(fst (List.hd fmt)) ()
@@ -926,18 +975,23 @@ let is_only_printing mods =
(* Compute precedences from modifiers (or find default ones) *)
-let set_entry_type from etyps (x,typ) =
+let set_entry_type from n etyps (x,typ) =
+ let make_lev n s = match typ with
+ | BorderProd _ -> NumLevel n
+ | InternalProd -> DefaultLevel in
let typ = try
match List.assoc x etyps, typ with
- | ETConstr (s,bko,Some n), (_,BorderProd (left,_)) ->
+ | ETConstr (s,bko,DefaultLevel), _ ->
+ if notation_entry_eq from s then ETConstr (s,bko,(make_lev n s,typ))
+ else ETConstr (s,bko,(DefaultLevel,typ))
+ | ETConstr (s,bko,n), BorderProd (left,_) ->
ETConstr (s,bko,(n,BorderProd (left,None)))
- | ETConstr (s,bko,Some n), (_,InternalProd) ->
- ETConstr (s,bko,(n,InternalProd))
+ | ETConstr (s,bko,n), InternalProd ->
+ ETConstr (s,bko,(n,InternalProd))
| ETPattern (b,n), _ -> ETPattern (b,n)
| (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
- | ETConstr (s,bko,None), _ -> ETConstr (s,bko,typ)
with Not_found ->
- ETConstr (from,None,typ)
+ ETConstr (from,None,(make_lev n from,typ))
in (x,typ)
let join_auxiliary_recursive_types recvars etyps =
@@ -1094,7 +1148,7 @@ let find_precedence custom lev etyps symbols onlyprint =
else
user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in
(try match List.assoc x etyps, custom with
- | ETConstr (s,_,Some _), s' when s = s' -> test ()
+ | ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test ()
| (ETIdent | ETBigint | ETGlobal), _ ->
begin match lev with
| None ->
@@ -1187,14 +1241,13 @@ module SynData = struct
end
let find_subentry_types from n assoc etyps symbols =
- let innerlevel = NumLevel 200 in
let typs =
find_symbols
- (NumLevel n,BorderProd(Left,assoc))
- (innerlevel,InternalProd)
- (NumLevel n,BorderProd(Right,assoc))
+ (BorderProd(Left,assoc))
+ (InternalProd)
+ (BorderProd(Right,assoc))
symbols in
- let sy_typs = List.map (set_entry_type from etyps) typs in
+ let sy_typs = List.map (set_entry_type from n etyps) typs in
let prec = List.map (assoc_of_type from n) sy_typs in
sy_typs, prec
@@ -1416,7 +1469,7 @@ let make_syntax_rules (sd : SynData.syn_data) = let open SynData in
let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in
let custom,level,_,_ = sd.level in
let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in
- let pp_rule = make_pp_rule (custom,level) sd.pp_syntax_data sd.format in {
+ let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in {
synext_level = sd.level;
synext_notation = fst sd.info;
synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 2bac35b08f..ab9d008659 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -11,7 +11,6 @@
open CErrors
open Util
open Pp
-open Libobject
open System
(* Code to hook Coq into the ML toplevel -- depends on having the
@@ -304,23 +303,38 @@ let _ =
(* Liboject entries of declared ML Modules *)
+(* Digest of module used to compile the file *)
+type ml_module_digest =
+ | NoDigest
+ | AnyDigest of Digest.t (* digest of any used cma / cmxa *)
+
type ml_module_object = {
mlocal : Vernacexpr.locality_flag;
- mnames : string list
+ mnames : (string * ml_module_digest) list
}
+let add_module_digest m =
+ try
+ let file = file_of_name m in
+ let path, file = System.where_in_path ~warn:false !coq_mlpath_copy file in
+ m, AnyDigest (Digest.file file)
+ with
+ | Not_found ->
+ m, NoDigest
+
let cache_ml_objects (_,{mnames=mnames}) =
- let iter obj = trigger_ml_object true true true obj in
+ let iter (obj, _) = trigger_ml_object true true true obj in
List.iter iter mnames
let load_ml_objects _ (_,{mnames=mnames}) =
- let iter obj = trigger_ml_object true false true obj in
+ let iter (obj, _) = trigger_ml_object true false true obj in
List.iter iter mnames
let classify_ml_objects ({mlocal=mlocal} as o) =
- if mlocal then Dispose else Substitute o
+ if mlocal then Libobject.Dispose else Libobject.Substitute o
-let inMLModule : ml_module_object -> obj =
+let inMLModule : ml_module_object -> Libobject.obj =
+ let open Libobject in
declare_object
{(default_object "ML-MODULE") with
cache_function = cache_ml_objects;
@@ -330,6 +344,7 @@ let inMLModule : ml_module_object -> obj =
let declare_ml_modules local l =
let l = List.map mod_of_name l in
+ let l = List.map add_module_digest l in
Lib.add_anonymous_leaf ~cache_first:false (inMLModule {mlocal=local; mnames=l})
let print_ml_path () =
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index a1bd99c237..314c423f65 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -107,8 +107,11 @@ open Pputils
| InCustomEntry s -> keyword "custom" ++ spc () ++ str s
let pr_at_level = function
- | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
- | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
+ | NumLevel n -> spc () ++ keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
+ | NextLevel -> spc () ++ keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
+ | DefaultLevel -> mt ()
+
+ let level_of_pattern_level = function None -> DefaultLevel | Some n -> NumLevel n
let pr_constr_as_binder_kind = let open Notation_term in function
| AsIdent -> spc () ++ keyword "as ident"
@@ -120,19 +123,14 @@ open Pputils
let pr_set_entry_type pr = function
| ETIdent -> str"ident"
| ETGlobal -> str"global"
- | ETPattern (b,None) -> pr_strict b ++ str"pattern"
- | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
+ | ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n)
| ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko
| ETBigint -> str "bigint"
| ETBinder true -> str "binder"
| ETBinder false -> str "closed binder"
- let pr_at_level_opt = function
- | None -> mt ()
- | Some n -> spc () ++ pr_at_level n
-
let pr_set_simple_entry_type =
- pr_set_entry_type pr_at_level_opt
+ pr_set_entry_type pr_at_level
let pr_comment pr_c = function
| CommentConstr c -> pr_c c
@@ -402,7 +400,7 @@ let string_of_theorem_kind = let open Decls in function
let pr_syntax_modifier = let open Gramlib.Gramext in function
| SetItemLevel (l,bko,n) ->
- prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++
+ prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n ++
pr_opt pr_constr_as_binder_kind bko
| SetLevel n -> pr_at_level (NumLevel n)
| SetCustomEntry (s,n) -> keyword "in" ++ spc() ++ keyword "custom" ++ spc() ++ str s ++ (match n with None -> mt () | Some n -> pr_at_level (NumLevel n))
@@ -476,7 +474,7 @@ let string_of_theorem_kind = let open Decls in function
let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
- let pr_record_decl b c fs =
+ let pr_record_decl c fs =
pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++
hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
@@ -802,7 +800,7 @@ let string_of_definition_object_kind = let open Decls in function
(if coe then str":>" else str":") ++
Flags.without_option Flags.beautify pr_spc_lconstr c)
in
- let pr_constructor_list b l = match l with
+ let pr_constructor_list l = match l with
| Constructors [] -> mt()
| Constructors l ->
let fst_sep = match l with [_] -> " " | _ -> " | " in
@@ -810,21 +808,21 @@ let string_of_definition_object_kind = let open Decls in function
fnl() ++ str fst_sep ++
prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l
| RecordDecl (c,fs) ->
- pr_record_decl b c fs
+ pr_record_decl c fs
in
- let pr_oneind key (((coe,iddecl),indpar,s,k,lc),ntn) =
+ let pr_oneind key (((coe,iddecl),(indupar,indpar),s,lc),ntn) =
hov 0 (
str key ++ spc() ++
(if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
- pr_and_type_binders_arg indpar ++
+ pr_and_type_binders_arg indupar ++
+ pr_opt (fun p -> str "|" ++ spc() ++ pr_and_type_binders_arg p) indpar ++
pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++
- str" :=") ++ pr_constructor_list k lc ++
+ str" :=") ++ pr_constructor_list lc ++
prlist (pr_decl_notation @@ pr_constr env sigma) ntn
in
let key =
- let (_,_,_,k,_),_ = List.hd l in
let kind =
- match k with Record -> "Record" | Structure -> "Structure"
+ match f with Record -> "Record" | Structure -> "Structure"
| Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
| Class _ -> "Class" | Variant -> "Variant"
in
@@ -1076,14 +1074,14 @@ let string_of_definition_object_kind = let open Decls in function
let pr_br imp force x =
let left,right =
match imp with
- | Impargs.Implicit -> str "[", str "]"
- | Impargs.MaximallyImplicit -> str "{", str "}"
- | Impargs.NotImplicit -> if force then str"(",str")" else mt(),mt()
+ | Glob_term.NonMaxImplicit -> str "[", str "]"
+ | Glob_term.MaxImplicit -> str "{", str "}"
+ | Glob_term.Explicit -> if force then str"(",str")" else mt(),mt()
in
left ++ x ++ right
in
let get_arguments_like s imp tl =
- if s = None && imp = Impargs.NotImplicit then [], tl
+ if s = None && imp = Glob_term.Explicit then [], tl
else
let rec fold extra = function
| RealArg arg :: tl when
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 2cd1cf7c65..32c438c724 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -211,12 +211,10 @@ let pr_template_variables = function
let print_polymorphism ref =
let poly = Global.is_polymorphic ref in
let template_poly = Global.is_template_polymorphic ref in
- let template_checked = Global.is_template_checked ref in
let template_variables = Global.get_template_polymorphic_variables ref in
[ pr_global ref ++ str " is " ++
(if poly then str "universe polymorphic"
else if template_poly then
- (if not template_checked then str "assumed " else mt()) ++
str "template universe polymorphic "
++ h 0 (pr_template_variables template_variables)
else str "not universe polymorphic") ]
@@ -260,18 +258,18 @@ let implicit_name_of_pos = function
| Constrexpr.ExplByPos (n,k) -> Anonymous
let implicit_kind_of_status = function
- | None -> Anonymous, NotImplicit
- | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then MaximallyImplicit else Implicit
+ | None -> Anonymous, Glob_term.Explicit
+ | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit
let dummy = {
- Vernacexpr.implicit_status = NotImplicit;
+ Vernacexpr.implicit_status = Glob_term.Explicit;
name = Anonymous;
recarg_like = false;
notation_scope = None;
}
let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} =
- name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit
+ name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit
let rec main_implicits i renames recargs scopes impls =
if renames = [] && recargs = [] && scopes = [] && impls = [] then []
@@ -283,8 +281,8 @@ let rec main_implicits i renames recargs scopes impls =
let (name, implicit_status) =
match renames, impls with
| _, (Some _ as i) :: _ -> implicit_kind_of_status i
- | name::_, _ -> (name,NotImplicit)
- | [], (None::_ | []) -> (Anonymous, NotImplicit)
+ | name::_, _ -> (name,Glob_term.Explicit)
+ | [], (None::_ | []) -> (Anonymous, Glob_term.Explicit)
in
let notation_scope = match scopes with
| scope :: _ -> Option.map CAst.make scope
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index cfb3248c7b..b329463cb0 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -140,7 +140,6 @@ let suggest_proof_using = ref false
let () =
Goptions.(declare_bool_option
{ optdepr = false;
- optname = "suggest Proof using";
optkey = ["Suggest";"Proof";"Using"];
optread = (fun () -> !suggest_proof_using);
optwrite = ((:=) suggest_proof_using) })
@@ -176,7 +175,6 @@ let proof_using_opt_name = ["Default";"Proof";"Using"]
let () =
Goptions.(declare_stringopt_option
{ optdepr = false;
- optname = "default value for Proof using";
optkey = proof_using_opt_name;
optread = (fun () -> Option.map using_to_string !value);
optwrite = (fun b -> value := Option.map using_from_string b);
diff --git a/vernac/record.ml b/vernac/record.ml
index df9b4a0914..3e44cd85cc 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -39,7 +39,6 @@ let primitive_flag = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "use of primitive projections";
optkey = ["Primitive";"Projections"];
optread = (fun () -> !primitive_flag) ;
optwrite = (fun b -> primitive_flag := b) }
@@ -48,7 +47,6 @@ let typeclasses_strict = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "strict typeclass resolution";
optkey = ["Typeclasses";"Strict";"Resolution"];
optread = (fun () -> !typeclasses_strict);
optwrite = (fun b -> typeclasses_strict := b); }
@@ -57,7 +55,6 @@ let typeclasses_unique = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "unique typeclass instances";
optkey = ["Typeclasses";"Unique";"Instances"];
optread = (fun () -> !typeclasses_unique);
optwrite = (fun b -> typeclasses_unique := b); }
@@ -446,8 +443,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
univs)
param_levels fields
in
- let template_check = Environ.check_template (Global.env ()) in
- ComInductive.template_polymorphism_candidate ~template_check ~ctor_levels univs params
+ ComInductive.template_polymorphism_candidate ~ctor_levels univs params
(Some (Sorts.sort_of_univ min_univ))
in
match template with
@@ -626,7 +622,7 @@ let add_inductive_class env sigma ind =
let env = push_context ~strict:false (Univ.AUContext.repr univs) env in
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 ty = Inductive.type_of_inductive ((mind, oneind), inst) in
let r = Inductive.relevance_of_inductive env ind in
{ cl_univs = univs;
cl_impl = GlobRef.IndRef ind;
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d011fb2e77..63fc587f71 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -609,27 +609,8 @@ let vernac_assumption ~atts discharge kind l nl =
| DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
-let set_template_check b =
- let typing_flags = Environ.typing_flags (Global.env ()) in
- Global.set_typing_flags { typing_flags with Declarations.check_template = b }
-
-let is_template_check () =
- let typing_flags = Environ.typing_flags (Global.env ()) in
- typing_flags.Declarations.check_template
-
-let () =
- let tccheck =
- { optdepr = true;
- optname = "Template universe check";
- optkey = ["Template"; "Check"];
- optread = (fun () -> is_template_check ());
- optwrite = (fun b -> set_template_check b)}
- in
- declare_bool_option tccheck
-
let is_polymorphic_inductive_cumulativity =
declare_bool_option_and_ref ~depr:false ~value:false
- ~name:"Polymorphic inductive cumulativity"
~key:["Polymorphic"; "Inductive"; "Cumulativity"]
let should_treat_as_cumulative cum poly =
@@ -645,7 +626,6 @@ let should_treat_as_cumulative cum poly =
let get_uniform_inductive_parameters =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"Uniform inductive parameters"
~key:["Uniform"; "Inductive"; "Parameters"]
~value:false
@@ -681,25 +661,30 @@ let vernac_record ~template udecl cum k poly finite records =
let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
match indl with
| [] -> assert false
- | (((coe,(id,udecl)),b,c,k,d),e) :: rest ->
- let rest = List.map (fun (((coe,(id,udecl)),b,c,k,d),e) ->
+ | (((coe,(id,udecl)),b,c,d),e) :: rest ->
+ let rest = List.map (fun (((coe,(id,udecl)),b,c,d),e) ->
if Option.has_some udecl
then user_err ~hdr:"inductive udecl" Pp.(strbrk "Universe binders must be on the first inductive of the block.")
- else (((coe,id),b,c,k,d),e))
+ else (((coe,id),b,c,d),e))
rest
in
- udecl, (((coe,id),b,c,k,d),e) :: rest
+ udecl, (((coe,id),b,c,d),e) :: rest
+
+let finite_of_kind = let open Declarations in function
+ | Inductive_kw -> Finite
+ | CoInductive -> CoFinite
+ | Variant | Record | Structure | Class _ -> BiFinite
(** When [poly] is true the type is declared polymorphic. When [lo] is true,
then the type is declared private (as per the [Private] keyword). [finite]
indicates whether the type is inductive, co-inductive or
neither. *)
-let vernac_inductive ~atts cum lo finite indl =
+let vernac_inductive ~atts cum lo kind indl =
let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
let open Pp in
let udecl, indl = extract_inductive_udecl indl in
if Dumpglob.dump () then
- List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
+ List.iter (fun (((coe,lid), _, _, cstrs), _) ->
match cstrs with
| Constructors cstrs ->
Dumpglob.dump_definition lid false "ind";
@@ -708,21 +693,26 @@ let vernac_inductive ~atts cum lo finite indl =
| _ -> () (* dumping is done by vernac_record (called below) *) )
indl;
+ let finite = finite_of_kind kind in
let is_record = function
- | ((_ , _ , _ , _, RecordDecl _), _) -> true
+ | ((_ , _ , _ , RecordDecl _), _) -> true
| _ -> false
in
let is_constructor = function
- | ((_ , _ , _ , _, Constructors _), _) -> true
+ | ((_ , _ , _ , Constructors _), _) -> true
| _ -> false
in
- let is_defclass = match indl with
- | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l)
+ let is_defclass = match kind, indl with
+ | Class _, [ ( id , bl , c , Constructors [l]), [] ] -> Some (id, bl, c, l)
| _ -> None
in
if Option.has_some is_defclass then
(* Definitional class case *)
let (id, bl, c, l) = Option.get is_defclass in
+ let bl = match bl with
+ | bl, None -> bl
+ | _ -> CErrors.user_err Pp.(str "Definitional classes do not support the \"|\" syntax.")
+ in
let (coe, (lid, ce)) = l in
let coe' = if coe then Some true else None in
let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce),
@@ -730,38 +720,39 @@ let vernac_inductive ~atts cum lo finite indl =
vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]]
else if List.for_all is_record indl then
(* Mutual record case *)
- let check_kind ((_, _, _, kind, _), _) = match kind with
- | Variant ->
- user_err (str "The Variant keyword does not support syntax { ... }.")
- | Record | Structure | Class _ | Inductive_kw | CoInductive -> ()
+ let () = match kind with
+ | Variant ->
+ user_err (str "The Variant keyword does not support syntax { ... }.")
+ | Record | Structure | Class _ | Inductive_kw | CoInductive -> ()
in
- let () = List.iter check_kind indl in
- let check_where ((_, _, _, _, _), wh) = match wh with
+ let check_where ((_, _, _, _), wh) = match wh with
| [] -> ()
| _ :: _ ->
user_err (str "where clause not supported for records")
in
let () = List.iter check_where indl in
- let unpack ((id, bl, c, _, decl), _) = match decl with
+ let unpack ((id, bl, c, decl), _) = match decl with
| RecordDecl (oc, fs) ->
+ let bl = match bl with
+ | bl, None -> bl
+ | _ -> CErrors.user_err Pp.(str "Records do not support the \"|\" syntax.")
+ in
(id, bl, c, oc, fs)
| Constructors _ -> assert false (* ruled out above *)
in
- let ((_, _, _, kind, _), _) = List.hd indl in
let kind = match kind with Class _ -> Class false | _ -> kind in
let recordl = List.map unpack indl in
vernac_record ~template udecl cum kind poly finite recordl
else if List.for_all is_constructor indl then
(* Mutual inductive case *)
- let check_kind ((_, _, _, kind, _), _) = match kind with
+ let () = match kind with
| (Record | Structure) ->
user_err (str "The Record keyword is for types defined using the syntax { ... }.")
| Class _ ->
user_err (str "Inductive classes not supported")
| Variant | Inductive_kw | CoInductive -> ()
in
- let () = List.iter check_kind indl in
- let check_name ((na, _, _, _, _), _) = match na with
+ let check_name ((na, _, _, _), _) = match na with
| (true, _) ->
user_err (str "Variant types do not handle the \"> Name\" \
syntax, which is reserved for records. Use the \":>\" \
@@ -769,7 +760,7 @@ let vernac_inductive ~atts cum lo finite indl =
| _ -> ()
in
let () = List.iter check_name indl in
- let unpack (((_, id) , bl, c, _, decl), ntn) = match decl with
+ let unpack (((_, id) , bl, c, decl), ntn) = match decl with
| Constructors l -> (id, bl, c, l), ntn
| RecordDecl _ -> assert false (* ruled out above *)
in
@@ -779,16 +770,6 @@ let vernac_inductive ~atts cum lo finite indl =
ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind:lo ~uniform finite
else
user_err (str "Mixed record-inductive definitions are not allowed")
-(*
-
- match indl with
- | [ ( id , bl , c , Class _, Constructors [l]), [] ] ->
- let f =
- let (coe, ({loc;v=id}, ce)) = l in
- let coe' = if coe then Some true else None in
- (((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), [])
- in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
- *)
let vernac_fixpoint_common ~atts discharge l =
if Dumpglob.dump () then
@@ -1238,7 +1219,6 @@ 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 }
@@ -1246,7 +1226,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "silent";
optkey = ["Silent"];
optread = (fun () -> !Flags.quiet);
optwrite = ((:=) Flags.quiet) }
@@ -1254,7 +1233,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "implicit arguments";
optkey = ["Implicit";"Arguments"];
optread = Impargs.is_implicit_args;
optwrite = Impargs.make_implicit_args }
@@ -1262,7 +1240,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "strict implicit arguments";
optkey = ["Strict";"Implicit"];
optread = Impargs.is_strict_implicit_args;
optwrite = Impargs.make_strict_implicit_args }
@@ -1270,7 +1247,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "strong strict implicit arguments";
optkey = ["Strongly";"Strict";"Implicit"];
optread = Impargs.is_strongly_strict_implicit_args;
optwrite = Impargs.make_strongly_strict_implicit_args }
@@ -1278,7 +1254,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "contextual implicit arguments";
optkey = ["Contextual";"Implicit"];
optread = Impargs.is_contextual_implicit_args;
optwrite = Impargs.make_contextual_implicit_args }
@@ -1286,7 +1261,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "implicit status of reversible patterns";
optkey = ["Reversible";"Pattern";"Implicit"];
optread = Impargs.is_reversible_pattern_implicit_args;
optwrite = Impargs.make_reversible_pattern_implicit_args }
@@ -1294,7 +1268,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "maximal insertion of implicit";
optkey = ["Maximal";"Implicit";"Insertion"];
optread = Impargs.is_maximal_implicit_args;
optwrite = Impargs.make_maximal_implicit_args }
@@ -1302,7 +1275,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "coercion printing";
optkey = ["Printing";"Coercions"];
optread = (fun () -> !Constrextern.print_coercions);
optwrite = (fun b -> Constrextern.print_coercions := b) }
@@ -1310,7 +1282,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "printing of existential variable instances";
optkey = ["Printing";"Existential";"Instances"];
optread = (fun () -> !Detyping.print_evar_arguments);
optwrite = (:=) Detyping.print_evar_arguments }
@@ -1318,7 +1289,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "implicit arguments printing";
optkey = ["Printing";"Implicit"];
optread = (fun () -> !Constrextern.print_implicits);
optwrite = (fun b -> Constrextern.print_implicits := b) }
@@ -1326,7 +1296,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "implicit arguments defensive printing";
optkey = ["Printing";"Implicit";"Defensive"];
optread = (fun () -> !Constrextern.print_implicits_defensive);
optwrite = (fun b -> Constrextern.print_implicits_defensive := b) }
@@ -1334,7 +1303,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "projection printing using dot notation";
optkey = ["Printing";"Projections"];
optread = (fun () -> !Constrextern.print_projections);
optwrite = (fun b -> Constrextern.print_projections := b) }
@@ -1342,7 +1310,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "notations printing";
optkey = ["Printing";"Notations"];
optread = (fun () -> not !Constrextern.print_no_symbol);
optwrite = (fun b -> Constrextern.print_no_symbol := not b) }
@@ -1350,7 +1317,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "raw printing";
optkey = ["Printing";"All"];
optread = (fun () -> !Flags.raw_print);
optwrite = (fun b -> Flags.raw_print := b) }
@@ -1358,7 +1324,6 @@ let () =
let () =
declare_int_option
{ optdepr = false;
- optname = "the level of inlining during functor application";
optkey = ["Inline";"Level"];
optread = (fun () -> Some (Flags.get_inline_level ()));
optwrite = (fun o ->
@@ -1368,7 +1333,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "kernel term sharing";
optkey = ["Kernel"; "Term"; "Sharing"];
optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction);
optwrite = Global.set_share_reduction }
@@ -1376,7 +1340,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "display compact goal contexts";
optkey = ["Printing";"Compact";"Contexts"];
optread = (fun () -> Printer.get_compact_context());
optwrite = (fun b -> Printer.set_compact_context b) }
@@ -1384,7 +1347,6 @@ let () =
let () =
declare_int_option
{ optdepr = false;
- optname = "the printing depth";
optkey = ["Printing";"Depth"];
optread = Topfmt.get_depth_boxes;
optwrite = Topfmt.set_depth_boxes }
@@ -1392,7 +1354,6 @@ let () =
let () =
declare_int_option
{ optdepr = false;
- optname = "the printing width";
optkey = ["Printing";"Width"];
optread = Topfmt.get_margin;
optwrite = Topfmt.set_margin }
@@ -1400,7 +1361,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "printing of universes";
optkey = ["Printing";"Universes"];
optread = (fun () -> !Constrextern.print_universes);
optwrite = (fun b -> Constrextern.print_universes:=b) }
@@ -1408,7 +1368,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "dumping bytecode after compilation";
optkey = ["Dump";"Bytecode"];
optread = (fun () -> !Cbytegen.dump_bytecode);
optwrite = (:=) Cbytegen.dump_bytecode }
@@ -1416,7 +1375,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "dumping VM lambda code after compilation";
optkey = ["Dump";"Lambda"];
optread = (fun () -> !Clambda.dump_lambda);
optwrite = (:=) Clambda.dump_lambda }
@@ -1424,7 +1382,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "explicitly parsing implicit arguments";
optkey = ["Parsing";"Explicit"];
optread = (fun () -> !Constrintern.parsing_explicit);
optwrite = (fun b -> Constrintern.parsing_explicit := b) }
@@ -1432,7 +1389,6 @@ let () =
let () =
declare_string_option ~preprocess:CWarnings.normalize_flags_string
{ optdepr = false;
- optname = "warnings display";
optkey = ["Warnings"];
optread = CWarnings.get_flags;
optwrite = CWarnings.set_flags }
@@ -1440,7 +1396,6 @@ let () =
let () =
declare_string_option
{ optdepr = false;
- optname = "native_compute profiler output";
optkey = ["NativeCompute"; "Profile"; "Filename"];
optread = Nativenorm.get_profile_filename;
optwrite = Nativenorm.set_profile_filename }
@@ -1448,7 +1403,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "enable native compute profiling";
optkey = ["NativeCompute"; "Profiling"];
optread = Nativenorm.get_profiling_enabled;
optwrite = Nativenorm.set_profiling_enabled }
@@ -1456,7 +1410,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "enable native compute timing";
optkey = ["NativeCompute"; "Timing"];
optread = Nativenorm.get_timing_enabled;
optwrite = Nativenorm.set_timing_enabled }
@@ -1464,7 +1417,6 @@ let () =
let _ =
declare_bool_option
{ optdepr = false;
- optname = "guard checking";
optkey = ["Guard"; "Checking"];
optread = (fun () -> (Global.typing_flags ()).Declarations.check_guarded);
optwrite = (fun b -> Global.set_check_guarded b) }
@@ -1472,7 +1424,6 @@ let _ =
let _ =
declare_bool_option
{ optdepr = false;
- optname = "positivity/productivity checking";
optkey = ["Positivity"; "Checking"];
optread = (fun () -> (Global.typing_flags ()).Declarations.check_positive);
optwrite = (fun b -> Global.set_check_positive b) }
@@ -1480,7 +1431,6 @@ let _ =
let _ =
declare_bool_option
{ optdepr = false;
- optname = "universes checking";
optkey = ["Universe"; "Checking"];
optread = (fun () -> (Global.typing_flags ()).Declarations.check_universes);
optwrite = (fun b -> Global.set_check_universes b) }
@@ -1589,7 +1539,7 @@ let query_command_selector ?loc = function
let vernac_check_may_eval ~pstate ~atts redexp glopt rc =
let glopt = query_command_selector glopt in
let sigma, env = get_current_context_of_args ~pstate glopt in
- let sigma, c = interp_open_constr env sigma rc in
+ let sigma, c = interp_open_constr ~expected_type:Pretyping.UnknownIfTermOrType env sigma rc in
let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
Evarconv.check_problems_are_solved env sigma;
let sigma = Evd.minimize_universes sigma in
@@ -1795,7 +1745,6 @@ let search_output_name_only = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "output-name-only search";
optkey = ["Search";"Output";"Name";"Only"];
optread = (fun () -> !search_output_name_only);
optwrite = (:=) search_output_name_only }
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 1daa244986..45018a246c 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -104,7 +104,6 @@ type coercion_flag = bool (* true = AddCoercion false = NoCoercion *)
type instance_flag = bool option
(* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
type export_flag = bool (* true = Export; false = Import *)
-type inductive_flag = Declarations.recursivity_kind
type onlyparsing_flag = { onlyparsing : bool }
(* Some v = Parse only; None = Print also.
If v<>Current, it contains the name of the coq version
@@ -164,12 +163,15 @@ type constructor_expr = (lident * constr_expr) with_coercion
type constructor_list_or_record_decl_expr =
| Constructors of constructor_expr list
| RecordDecl of lident option * (local_decl_expr * record_field_attr) list
+type inductive_params_expr = local_binder_expr list * local_binder_expr list option
+(** If the option is nonempty the "|" marker was used *)
+
type inductive_expr =
- ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind *
+ ident_decl with_coercion * inductive_params_expr * constr_expr option *
constructor_list_or_record_decl_expr
type one_inductive_expr =
- lident * local_binder_expr list * constr_expr option * constructor_expr list
+ lident * inductive_params_expr * constr_expr option * constructor_expr list
type typeclass_constraint = name_decl * Glob_term.binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
@@ -178,7 +180,7 @@ type proof_expr =
ident_decl * (local_binder_expr list * constr_expr)
type syntax_modifier =
- | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option
+ | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level
| SetLevel of int
| SetCustomEntry of string * int option
| SetAssoc of Gramlib.Gramext.g_assoc
@@ -254,7 +256,7 @@ type vernac_one_argument_status = {
name : Name.t;
recarg_like : bool;
notation_scope : string CAst.t option;
- implicit_status : Impargs.implicit_kind;
+ implicit_status : Glob_term.binding_kind;
}
type vernac_argument_status =
@@ -306,7 +308,7 @@ type nonrec vernac_expr =
| VernacExactProof of constr_expr
| VernacAssumption of (discharge * Decls.assumption_object_kind) *
Declaremods.inline * (ident_decl list * constr_expr) with_coercion list
- | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_flag * (inductive_expr * decl_notation list) list
+ | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_kind * (inductive_expr * decl_notation list) list
| VernacFixpoint of discharge * fixpoint_expr list
| VernacCoFixpoint of discharge * cofixpoint_expr list
| VernacScheme of (lident option * scheme) list
@@ -386,7 +388,7 @@ type nonrec vernac_expr =
| VernacArguments of
qualid or_by_notation *
vernac_argument_status list (* Main arguments status list *) *
- (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
+ (Name.t * Glob_term.binding_kind) list list (* Extra implicit status lists *) *
arguments_modifier list
| VernacReserve of simple_binder list
| VernacGeneralizable of (lident list) option
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index c14fc78462..1ec09b6beb 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -65,7 +65,6 @@ let proof_mode_opt_name = ["Default";"Proof";"Mode"]
let () =
Goptions.declare_string_option Goptions.{
optdepr = false;
- optname = "default proof mode" ;
optkey = proof_mode_opt_name;
optread = get_default_proof_mode_opt;
optwrite = set_default_proof_mode_opt;
@@ -249,7 +248,6 @@ let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } =
let () = let open Goptions in
declare_int_option
{ optdepr = false;
- optname = "the default timeout";
optkey = ["Default";"Timeout"];
optread = (fun () -> !default_timeout);
optwrite = ((:=) default_timeout) }
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 18:17:50 +0000