aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/attributes.ml33
-rw-r--r--vernac/attributes.mli1
-rw-r--r--vernac/classes.ml7
-rw-r--r--vernac/comDefinition.ml7
-rw-r--r--vernac/comProgramFixpoint.ml19
-rw-r--r--vernac/g_vernac.mlg12
-rw-r--r--vernac/himsg.ml3
-rw-r--r--vernac/himsg.mli5
-rw-r--r--vernac/lemmas.ml14
-rw-r--r--vernac/metasyntax.ml8
-rw-r--r--vernac/metasyntax.mli1
-rw-r--r--vernac/obligations.ml36
-rw-r--r--vernac/obligations.mli4
-rw-r--r--vernac/ppvernac.ml2
-rw-r--r--vernac/record.ml26
-rw-r--r--vernac/record.mli9
-rw-r--r--vernac/topfmt.ml2
-rw-r--r--vernac/vernacentries.ml37
-rw-r--r--vernac/vernacexpr.ml2
19 files changed, 130 insertions, 98 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 9b8c4efb37..1ad5862d5d 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -82,9 +82,12 @@ let assert_empty k v =
if v <> VernacFlagEmpty
then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
+let error_twice ~name : 'a =
+ user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.")
+
let assert_once ~name prev =
if Option.has_some prev then
- user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.")
+ error_twice ~name
let attribute_of_list (l:(string * 'a key_parser) list) : 'a option attribute =
let rec p extra v = function
@@ -107,6 +110,24 @@ let bool_attribute ~name ~on ~off : bool option attribute =
attribute_of_list [(on, single_key_parser ~name ~key:on true);
(off, single_key_parser ~name ~key:off false)]
+(* Variant of the [bool] attribute with only two values (bool has three). *)
+let get_bool_value ~key ~default =
+ function
+ | VernacFlagEmpty -> default
+ | VernacFlagList [ "true", VernacFlagEmpty ] -> true
+ | VernacFlagList [ "false", VernacFlagEmpty ] -> false
+ | _ -> user_err Pp.(str "Attribute " ++ str key ++ str " only accepts boolean values.")
+
+let enable_attribute ~key ~default : bool attribute =
+ fun atts ->
+ let default = default () in
+ let this, extra = List.partition (fun (k, _) -> String.equal key k) atts in
+ extra,
+ match this with
+ | [] -> default
+ | [ _, value ] -> get_bool_value ~key ~default:true value
+ | _ -> error_twice ~name:key
+
let qualify_attribute qual (parser:'a attribute) : 'a attribute =
fun atts ->
let rec extract extra qualified = function
@@ -139,11 +160,8 @@ let () = let open Goptions in
optread = (fun () -> !program_mode);
optwrite = (fun b -> program_mode:=b) }
-let program_opt = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram"
-
-let program = program_opt >>= function
- | Some b -> return b
- | None -> return (!program_mode)
+let program =
+ enable_attribute ~key:"program" ~default:(fun () -> !program_mode)
let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
@@ -219,3 +237,6 @@ let only_polymorphism atts = parse polymorphic atts
let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty]
let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty]
+
+let canonical =
+ enable_attribute ~key:"canonical" ~default:(fun () -> true)
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 3cb4d69ca0..44688ddafc 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -52,6 +52,7 @@ val program : bool attribute
val template : bool option attribute
val locality : bool option attribute
val deprecation : deprecation option attribute
+val canonical : bool attribute
val program_mode_option_name : string list
(** For internal use when messing with the global option. *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 9f233a2551..ece9fc8937 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -374,6 +374,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po
let obls, constr, typ =
match term with
| Some t ->
+ let termtype = EConstr.of_constr termtype in
let obls, _, constr, typ =
Obligations.eterm_obligations env id sigma 0 t termtype
in obls, Some constr, typ
@@ -400,7 +401,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po
if not (Option.is_empty term) then
let init_refine =
Tacticals.New.tclTHENLIST [
- Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term)));
+ Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term));
Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
Tactics.New.reduce_after_refine;
]
@@ -497,10 +498,10 @@ let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program
(* Check that the type is free of evars now. *)
Pretyping.check_evars env (Evd.from_env env) sigma termtype;
let termtype = to_constr sigma termtype in
- let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
let pstate =
if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
- (declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype;
+ let term = to_constr sigma (Option.get term) in
+ (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype;
None)
else if program_mode || refine || Option.is_empty props then
declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 12df3215ad..d2c986fe5c 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -88,11 +88,12 @@ let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ct
let (c,ctx), sideff = Future.force ce.const_entry_body in
assert(Safe_typing.empty_private_constants = sideff);
assert(Univ.ContextSet.is_empty ctx);
+ Obligations.check_evars env evd;
+ let c = EConstr.of_constr c in
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))
+ | Some t -> EConstr.of_constr t
+ | None -> Retyping.get_type_of env evd c
in
- Obligations.check_evars env evd;
let obls, _, c, cty =
Obligations.eterm_obligations env ident evd 0 c typ
in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 20a2db7ca2..69e2a209eb 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -230,12 +230,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
in
(* XXX: Capturing sigma here... bad bad *)
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 ~abort_on_undefined_evars:false sigma typ in
Obligations.check_evars env sigma;
let evars, _, evars_def, evars_typ =
- Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp
+ Obligations.eterm_obligations env recname sigma 0 def typ
in
let ctx = Evd.evar_universe_context sigma in
ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
@@ -246,7 +243,7 @@ let out_def = function
| None -> user_err Pp.(str "Program Fixpoint needs defined bodies.")
let collect_evars_of_term evd c ty =
- let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in
+ let evars = Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty) in
Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
evars (Evd.from_ctx (Evd.evar_universe_context evd))
@@ -262,17 +259,13 @@ let do_program_recursive local poly fixkind fixl ntns =
let evd = nf_evar_map_undefined evd in
let collect_evars id def typ imps =
(* Generalize by the recursive prototypes *)
- let def =
- EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign)
- and typ =
- (* Worrying... *)
- EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign)
- in
+ let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
+ let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
let evm = collect_evars_of_term evd def typ in
let evars, _, def, typ =
Obligations.eterm_obligations env id evm
- (List.length rec_sign) def typ
- in (id, def, typ, imps, evars)
+ (List.length rec_sign) def typ in
+ (id, def, typ, imps, evars)
in
let (fixnames,fixrs,fixdefs,fixtypes) = fix in
let fiximps = List.map pi2 info in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 59d2a66259..6438b48e32 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -43,6 +43,7 @@ let query_command = Entry.create "vernac:query_command"
let subprf = Entry.create "vernac:subprf"
+let quoted_attributes = Entry.create "vernac:quoted_attributes"
let class_rawexpr = Entry.create "vernac:class_rawexpr"
let thm_token = Entry.create "vernac:thm_token"
let def_body = Entry.create "vernac:def_body"
@@ -75,7 +76,7 @@ let parse_compat_version = let open Flags in function
}
GRAMMAR EXTEND Gram
- GLOBAL: vernac_control gallina_ext noedit_mode subprf;
+ GLOBAL: vernac_control quoted_attributes gallina_ext noedit_mode subprf;
vernac_control: FIRST
[ [ IDENT "Time"; c = vernac_control -> { CAst.make ~loc @@ VernacTime (false,c) }
| IDENT "Redirect"; s = ne_string; c = vernac_control -> { CAst.make ~loc @@ VernacRedirect (s, c) }
@@ -447,10 +448,12 @@ GRAMMAR EXTEND Gram
*)
(* ... with coercions *)
record_field:
- [ [ bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
+ [ [ attr = LIST0 quoted_attributes ;
+ bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
rf_notation = decl_notation -> {
+ let rf_canonical = attr |> List.flatten |> parse canonical in
let rf_subclass, rf_decl = bd in
- rf_decl, { rf_subclass ; rf_priority ; rf_notation } } ] ]
+ rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ]
;
record_fields:
[ [ f = record_field; ";"; fs = record_fields -> { f :: fs }
@@ -1003,6 +1006,9 @@ GRAMMAR EXTEND Gram
| IDENT "Grammar"; ent = IDENT ->
(* This should be in "syntax" section but is here for factorization*)
{ PrintGrammar ent }
+ | IDENT "Custom"; IDENT "Grammar"; ent = IDENT ->
+ (* Should also be in "syntax" section *)
+ { PrintCustomGrammar ent }
| IDENT "LoadPath"; dir = OPT dirpath -> { PrintLoadPath dir }
| IDENT "Modules" ->
{ user_err Pp.(str "Print Modules is obsolete; use Print Libraries instead") }
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index f58eeae6dc..b2382ce6fc 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1348,9 +1348,6 @@ let explain_pattern_matching_error env sigma = function
| CannotInferPredicate typs ->
explain_cannot_infer_predicate env sigma typs
-let map_pguard_error = map_pguard_error
-let map_ptype_error = map_ptype_error
-
let explain_reduction_tactic_error = function
| Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
let e = map_ptype_error EConstr.of_constr e in
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index d0f42ea16b..d1c1c092e3 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -43,9 +43,4 @@ val explain_module_error : Modops.module_typing_error -> Pp.t
val explain_module_internalization_error :
Modintern.module_internalization_error -> Pp.t
-val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
-[@@ocaml.deprecated "Use [Type_errors.map_pguard_error]."]
-val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
-[@@ocaml.deprecated "Use [Type_errors.map_ptype_error]."]
-
val explain_prim_token_notation_error : string -> env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 1c7cc5e636..317cf487cc 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -75,13 +75,7 @@ let adjust_guardness_conditions const = function
List.interval 0 (List.length ((lam_assum c))))
lemma_guard (Array.to_list fixdefs) in
*)
- let fold env eff =
- try
- let _ = Environ.lookup_constant eff.seff_constant env in
- env
- with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
- in
- let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in
+ let env = Safe_typing.push_private_constants env eff in
let indexes =
search_guard env
possible_indexes fixdecls in
@@ -395,10 +389,10 @@ let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms s
maybe_declare_manual_implicits false ref imps;
call_hook ?hook ctx [] strength ref) thms_data in
let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
- let pstate, _ = Proof_global.with_current_proof (fun _ p ->
+ let pstate = Proof_global.simple_with_current_proof (fun _ p ->
match init_tac with
- | None -> p,(true,[])
- | Some tac -> Proof.run_tactic Global.(env ()) tac p) pstate in
+ | None -> p
+ | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in
pstate
let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms =
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 843296d24e..50914959dc 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -50,10 +50,10 @@ let pr_entry e =
str (Buffer.contents entry_buf)
let pr_registered_grammar name =
- let gram = try Some (Pcoq.find_grammars_by_name name) with Not_found -> None in
+ let gram = Pcoq.find_grammars_by_name name in
match gram with
- | None -> user_err Pp.(str "Unknown or unprintable grammar entry.")
- | Some entries ->
+ | [] -> user_err Pp.(str "Unknown or unprintable grammar entry.")
+ | entries ->
let pr_one (Pcoq.AnyEntry e) =
str "Entry " ++ str (Pcoq.Entry.name e) ++ str " is" ++ fnl () ++
pr_entry e
@@ -85,6 +85,8 @@ let pr_grammar = function
pr_entry Pvernac.Vernac_.gallina_ext
| name -> pr_registered_grammar name
+let pr_custom_grammar name = pr_registered_grammar ("constr:"^name)
+
(**********************************************************************)
(* Parse a format (every terminal starting with a letter or a single
quote (except a single quote alone) must be quoted) *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 38dbdf7e41..6435df23c7 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -57,6 +57,7 @@ val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr ->
(** Print the Camlp5 state of a grammar *)
val pr_grammar : string -> Pp.t
+val pr_custom_grammar : string -> Pp.t
val check_infix_modifiers : syntax_modifier list -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 1b1c618dc7..f768278dd7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -39,7 +39,7 @@ let check_evars env evm =
type oblinfo =
{ ev_name: int * Id.t;
- ev_hyps: Constr.named_context;
+ ev_hyps: EConstr.named_context;
ev_status: bool * Evar_kinds.obligation_definition_status;
ev_chop: int option;
ev_src: Evar_kinds.t Loc.located;
@@ -50,11 +50,11 @@ type oblinfo =
(** Substitute evar references in t using de Bruijn indices,
where n binders were passed through. *)
-let subst_evar_constr evs n idf t =
+let subst_evar_constr evm evs n idf t =
let seen = ref Int.Set.empty in
let transparent = ref Id.Set.empty in
let evar_info id = List.assoc_f Evar.equal id evs in
- let rec substrec (depth, fixrels) c = match Constr.kind c with
+ let rec substrec (depth, fixrels) c = match EConstr.kind evm c with
| Evar (k, args) ->
let { ev_name = (id, idstr) ;
ev_hyps = hyps ; ev_chop = chop } =
@@ -84,18 +84,18 @@ let subst_evar_constr evs n idf t =
in aux hyps args []
in
if List.exists
- (fun x -> match Constr.kind x with
+ (fun x -> match EConstr.kind evm x with
| Rel n -> Int.List.mem n fixrels
| _ -> false) args
then
transparent := Id.Set.add idstr !transparent;
- mkApp (idf idstr, Array.of_list args)
+ EConstr.mkApp (idf idstr, Array.of_list args)
| Fix _ ->
- Constr.map_with_binders succfix substrec (depth, 1 :: fixrels) c
- | _ -> Constr.map_with_binders succfix substrec (depth, fixrels) c
+ EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c
+ | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c
in
let t' = substrec (0, []) t in
- t', !seen, !transparent
+ EConstr.to_constr evm t', !seen, !transparent
(** Substitute variable references in t using de Bruijn indices,
@@ -112,18 +112,18 @@ let subst_vars acc n t =
to a product : forall H1 : t1, ..., forall Hn : tn, concl.
Changes evars and hypothesis references to variable references.
*)
-let etype_of_evar evs hyps concl =
+let etype_of_evar evm evs hyps concl =
let open Context.Named.Declaration in
let rec aux acc n = function
decl :: tl ->
- let t', s, trans = subst_evar_constr evs n mkVar (NamedDecl.get_type decl) in
+ let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar (NamedDecl.get_type decl) in
let t'' = subst_vars acc 0 t' in
let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in
let s' = Int.Set.union s s' in
let trans' = Id.Set.union trans trans' in
(match decl with
| LocalDef (id,c,_) ->
- let c', s'', trans'' = subst_evar_constr evs n mkVar c in
+ let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in
let c' = subst_vars acc 0 c' in
mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
Int.Set.union s'' s',
@@ -131,7 +131,7 @@ let etype_of_evar evs hyps concl =
| LocalAssum (id,_) ->
mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
| [] ->
- let t', s, trans = subst_evar_constr evs n mkVar concl in
+ let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in
subst_vars acc 0 t', s, trans
in aux [] 0 (List.rev hyps)
@@ -151,7 +151,7 @@ let evar_dependencies evm oev =
let one_step deps =
Evar.Set.fold (fun ev s ->
let evi = Evd.find evm ev in
- let deps' = evars_of_filtered_evar_info evi in
+ let deps' = evars_of_filtered_evar_info evm evi in
if Evar.Set.mem oev deps' then
invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev)
else Evar.Set.union deps' s)
@@ -209,9 +209,7 @@ let eterm_obligations env name evm fs ?status t ty =
(fun (id, (n, nstr), ev) l ->
let hyps = Evd.evar_filtered_context ev in
let hyps = trunc_named_context nc_len hyps in
- let hyps = EConstr.Unsafe.to_named_context hyps in
- let concl = EConstr.Unsafe.to_constr ev.evar_concl in
- let evtyp, deps, transp = etype_of_evar l hyps concl in
+ let evtyp, deps, transp = etype_of_evar evm l hyps ev.evar_concl in
let evtyp, hyps, chop =
match chop_product fs evtyp with
| Some t -> t, trunc_named_context fs hyps, fs
@@ -237,9 +235,9 @@ let eterm_obligations env name evm fs ?status t ty =
evn []
in
let t', _, transparent = (* Substitute evar refs in the term by variables *)
- subst_evar_constr evts 0 mkVar t
+ subst_evar_constr evm evts 0 EConstr.mkVar t
in
- let ty, _, _ = subst_evar_constr evts 0 mkVar ty in
+ let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in
let evars =
List.map (fun (ev, info) ->
let { ev_name = (_, name); ev_status = force_status, status;
@@ -252,7 +250,7 @@ let eterm_obligations env name evm fs ?status t ty =
in name, typ, src, (force_status, status), deps, tac) evts
in
let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
- let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
+ let evmap f c = pi1 (subst_evar_constr evm evts 0 f c) in
Array.of_list (List.rev evars), (evnames, evmap), t', ty
let hide_obligation () =
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index d25daeed9c..9214ddd4b9 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -26,14 +26,14 @@ val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar
(* env, id, evars, number of function prototypes to try to clear from
evars contexts, object and type *)
val eterm_obligations : env -> Id.t -> evar_map -> int ->
- ?status:Evar_kinds.obligation_definition_status -> constr -> types ->
+ ?status:Evar_kinds.obligation_definition_status -> EConstr.constr -> EConstr.types ->
(Id.t * types * Evar_kinds.t Loc.located *
(bool * Evar_kinds.obligation_definition_status) * Int.Set.t *
unit Proofview.tactic option) array
(* Existential key, obl. name, type as product,
location of the original evar, associated tactic,
status and dependencies as indexes into the array *)
- * ((Evar.t * Id.t) list * ((Id.t -> constr) -> constr -> constr)) *
+ * ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) *
constr * types
(* Translations from existential identifiers to obligation identifiers
and for terms with existentials to closed terms, given a
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 889dbafabd..f2332bab8b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -476,6 +476,8 @@ open Pputils
keyword "Print Section" ++ spc() ++ Libnames.pr_qualid s
| PrintGrammar ent ->
keyword "Print Grammar" ++ spc() ++ str ent
+ | PrintCustomGrammar ent ->
+ keyword "Print Custom Grammar" ++ spc() ++ str ent
| PrintLoadPath dir ->
keyword "Print LoadPath" ++ pr_opt DirPath.print dir
| PrintModules ->
diff --git a/vernac/record.ml b/vernac/record.ml
index f489707eb3..f737a8c524 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -276,8 +276,13 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields =
let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in
Termops.substl_rel_context (subst @ subst') fields
+type projection_flags = {
+ pf_subclass: bool;
+ pf_canonical: bool;
+}
+
(* We build projections *)
-let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers fieldimpls fields =
+let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags fieldimpls fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
let poly = Declareops.inductive_is_polymorphic mib in
@@ -299,7 +304,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
in
let (_,_,kinds,sp_projs,_) =
List.fold_left3
- (fun (nfi,i,kinds,sp_projs,subst) coe decl impls ->
+ (fun (nfi,i,kinds,sp_projs,subst) flags decl impls ->
let fi = RelDecl.get_name decl in
let ti = RelDecl.get_type decl in
let (sp_projs,i,subst) =
@@ -359,17 +364,17 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
in
let refi = ConstRef kn in
Impargs.maybe_declare_manual_implicits false refi impls;
- if coe then begin
+ if flags.pf_subclass then begin
let cl = Class.class_of_global (IndRef indsp) in
Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl
end;
let i = if is_local_assum decl then i+1 else i in
(Some kn::sp_projs, i, Projection term::subst)
with NotDefinable why ->
- warning_or_error coe indsp why;
+ warning_or_error flags.pf_subclass indsp why;
(None::sp_projs,i,NoProjection fi::subst) in
- (nfi-1,i,(fi, is_local_assum decl)::kinds,sp_projs,subst))
- (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
+ (nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst))
+ (List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls)
in (kinds,sp_projs)
open Typeclasses
@@ -525,7 +530,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
in
[cref, [Name proj_name, sub, Some proj_cst]]
| _ ->
- let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in
+ let record_data = [id, idbuild, arity, fieldimpls, fields, false,
+ List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in
let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls
params template ~kind:Method ~name:[|binder_name|] record_data
in
@@ -699,7 +705,11 @@ let definition_structure udecl kind ~template cum poly finite records =
let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
- let coe = List.map (fun (_, { rf_subclass }) -> not (Option.is_empty rf_subclass)) cfs in
+ let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
+ { pf_subclass = not (Option.is_empty rf_subclass);
+ pf_canonical = rf_canonical })
+ cfs
+ in
id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
in
let data = List.map2 map data records in
diff --git a/vernac/record.mli b/vernac/record.mli
index d6e63901cd..24bb27e107 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -14,15 +14,20 @@ open Constrexpr
val primitive_flag : bool ref
+type projection_flags = {
+ pf_subclass: bool;
+ pf_canonical: bool;
+}
+
val declare_projections :
inductive ->
Entries.universes_entry ->
?kind:Decl_kinds.definition_object_kind ->
Id.t ->
- bool list ->
+ projection_flags list ->
Impargs.manual_implicits list ->
Constr.rel_context ->
- (Name.t * bool) list * Constant.t option list
+ Recordops.proj_kind list * Constant.t option list
val declare_structure_entry : Recordops.struc_tuple -> unit
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 118c126970..bf2efb2542 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -201,7 +201,7 @@ let set_emacs_print_strings () =
let diff = "diff." in
List.iter (fun b ->
let (name, attrs) = b in
- if diff = (String.sub name 0 (String.length diff)) then
+ if CString.is_sub diff name 0 then
tag_map := CString.Map.add name
{ attrs with prefix = Some (Printf.sprintf "<%s>" name);
suffix = Some (Printf.sprintf "</%s>" name) }
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 388f6957cf..e1d134f3a9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -744,7 +744,7 @@ let vernac_inductive ~atts cum lo finite indl =
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),
- { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] } in
+ { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in
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 *)
@@ -1231,16 +1231,13 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
let clear_implicits_flag = List.mem `ClearImplicits flags in
let default_implicits_flag = List.mem `DefaultImplicits flags in
let never_unfold_flag = List.mem `ReductionNeverUnfold flags in
+ let nomatch_flag = List.mem `ReductionDontExposeCase flags in
let err_incompat x y =
user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in
if assert_flag && rename_flag then
err_incompat "assert" "rename";
- if Option.has_some nargs_for_red && never_unfold_flag then
- err_incompat "simpl never" "/";
- if never_unfold_flag && List.mem `ReductionDontExposeCase flags then
- err_incompat "simpl never" "simpl nomatch";
if clear_scopes_flag && extra_scopes_flag then
err_incompat "clear scopes" "extra scopes";
if clear_implicits_flag && default_implicits_flag then
@@ -1385,19 +1382,24 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
(Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 args)
in
- let rec narrow = function
- | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl
- | [] -> [] | _ :: tl -> narrow tl
- in
- let red_flags = narrow flags in
- let red_modifiers_specified =
- not (List.is_empty rargs) || Option.has_some nargs_for_red
- || not (List.is_empty red_flags)
+ let red_behavior =
+ let open Reductionops.ReductionBehaviour in
+ match never_unfold_flag, nomatch_flag, rargs, nargs_for_red with
+ | true, false, [], None -> Some NeverUnfold
+ | true, true, _, _ -> err_incompat "simpl never" "simpl nomatch"
+ | true, _, _::_, _ -> err_incompat "simpl never" "!"
+ | true, _, _, Some _ -> err_incompat "simpl never" "/"
+ | false, false, [], None -> None
+ | false, false, _, _ -> Some (UnfoldWhen { nargs = nargs_for_red;
+ recargs = rargs;
+ })
+ | false, true, _, _ -> Some (UnfoldWhenNoMatch { nargs = nargs_for_red;
+ recargs = rargs;
+ })
in
- if not (List.is_empty rargs) && never_unfold_flag then
- err_incompat "simpl never" "!";
+ let red_modifiers_specified = Option.has_some red_behavior in
(* Actions *)
@@ -1424,8 +1426,8 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
match sr with
| ConstRef _ as c ->
Reductionops.ReductionBehaviour.set
- section_local c
- (rargs, Option.default ~-1 nargs_for_red, red_flags)
+ ~local:section_local c (Option.get red_behavior)
+
| _ -> user_err
(strbrk "Modifiers of the behavior of the simpl tactic "++
strbrk "are relevant for constants only.")
@@ -1883,6 +1885,7 @@ let vernac_print ~(pstate : Proof_global.t option) ~atts =
| PrintSectionContext qid -> print_sec_context_typ env sigma qid
| PrintInspect n -> inspect env sigma n
| PrintGrammar ent -> Metasyntax.pr_grammar ent
+ | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent
| PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir
| PrintModules -> print_modules ()
| PrintModule qid -> print_module qid
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 34a9b9394a..23633e39ab 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -29,6 +29,7 @@ type printable =
| PrintSectionContext of qualid
| PrintInspect of int
| PrintGrammar of string
+ | PrintCustomGrammar of string
| PrintLoadPath of DirPath.t option
| PrintModules
| PrintModule of qualid
@@ -148,6 +149,7 @@ type record_field_attr = {
rf_subclass: instance_flag; (* the projection is an implicit coercion or an instance *)
rf_priority: int option; (* priority of the instance, if relevant *)
rf_notation: decl_notation list;
+ rf_canonical: bool; (* use this projection in the search for canonical instances *)
}
type constructor_expr = (lident * constr_expr) with_coercion
type constructor_list_or_record_decl_expr =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 15:13:27 +0000