aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml35
-rw-r--r--vernac/comFixpoint.ml2
-rw-r--r--vernac/comInductive.ml29
-rw-r--r--vernac/declare.ml38
-rw-r--r--vernac/egramcoq.ml8
-rw-r--r--vernac/g_vernac.mlg59
-rw-r--r--vernac/himsg.ml41
-rw-r--r--vernac/metasyntax.ml15
-rw-r--r--vernac/ppvernac.ml5
-rw-r--r--vernac/pvernac.ml24
-rw-r--r--vernac/pvernac.mli4
-rw-r--r--vernac/record.ml42
-rw-r--r--vernac/vernacentries.ml2
-rw-r--r--vernac/vernacexpr.ml3
-rw-r--r--vernac/vernacextend.ml2
15 files changed, 157 insertions, 152 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index b38a249b73..a464eab127 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -58,13 +58,7 @@ let is_local_for_hint i =
let add_instance_base inst =
let locality = if is_local_for_hint inst then Goptions.OptLocal else Goptions.OptGlobal in
add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~locality
- inst.is_info;
- List.iter (fun (path, pri, c) ->
- let h = Hints.IsConstr (EConstr.of_constr c, None) [@ocaml.warning "-3"] in
- add_instance_hint h path
- ~locality pri)
- (build_subclasses ~check:(not (isVarRef inst.is_impl))
- (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
+ inst.is_info
let mk_instance cl info glob impl =
let global =
@@ -161,8 +155,17 @@ let subst_class (subst,cl) =
let do_subst_context (grs,ctx) =
List.Smart.map (Option.Smart.map do_subst_gr) grs,
do_subst_ctx ctx in
- let do_subst_projs projs = List.Smart.map (fun (x, y, z) ->
- (x, y, Option.Smart.map do_subst_con z)) projs in
+ let do_subst_meth m =
+ let c = Option.Smart.map do_subst_con m.meth_const in
+ if c == m.meth_const then m
+ else
+ {
+ meth_name = m.meth_name;
+ meth_info = m.meth_info;
+ meth_const = c;
+ }
+ in
+ let do_subst_projs projs = List.Smart.map do_subst_meth projs in
{ cl_univs = cl.cl_univs;
cl_impl = do_subst_gr cl.cl_impl;
cl_context = do_subst_context cl.cl_context;
@@ -247,10 +250,10 @@ let add_class cl =
let add_class env sigma cl =
add_class cl;
- List.iter (fun (n, inst, body) ->
- match inst with
- | Some (Backward, info) ->
- (match body with
+ List.iter (fun m ->
+ match m.meth_info with
+ | Some info ->
+ (match m.meth_const with
| None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance")
| Some b -> declare_instance ~warn:true env sigma (Some info) false (GlobRef.ConstRef b))
| _ -> ())
@@ -430,9 +433,9 @@ let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst =
let rest' = List.filter (fun v -> not (is_id v)) rest
in
let {CAst.loc;v=mid} = get_id loc_mid in
- List.iter (fun (n, _, x) ->
- if Name.equal n (Name mid) then
- Option.iter (fun x -> Dumpglob.add_glob ?loc (GlobRef.ConstRef x)) x) k.cl_projs;
+ List.iter (fun m ->
+ if Name.equal m.meth_name (Name mid) then
+ Option.iter (fun x -> Dumpglob.add_glob ?loc (GlobRef.ConstRef x)) m.meth_const) k.cl_projs;
c :: props, rest'
with Not_found ->
((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 564d24c1ea..78572c6aa6 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -110,7 +110,7 @@ let interp_fix_context ~program_mode ~cofix env sigma fix =
else [], fix.Vernacexpr.binders in
let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in
let sigma, (impl_env', ((env'', ctx'), imps')) =
- interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after
+ interp_context_evars ~program_mode ~impl_env env' sigma after
in
let annot = Option.map (fun _ -> List.length (Termops.assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in
sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 452de69b1d..bb26ce652e 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -16,7 +16,6 @@ open Context
open Environ
open Names
open Libnames
-open Nameops
open Constrexpr
open Constrexpr_ops
open Constrintern
@@ -139,7 +138,7 @@ let model_conclusion env sigma ind_rel params n arity_indices =
let sigma,model_indices =
List.fold_right
(fun (_,t) (sigma, subst) ->
- let t = EConstr.Vars.substl subst (EConstr.Vars.liftn n (List.length subst + 1) (EConstr.Vars.liftn 1 (List.length params + List.length subst + 1) t)) in
+ let t = EConstr.Vars.substl subst (EConstr.Vars.liftn n (List.length subst + 1) t) in
let sigma, c = Evarutil.new_evar env sigma t in
sigma, c::subst)
arity_indices (sigma, []) in
@@ -443,9 +442,8 @@ let interp_params env udecl uparamsl paramsl =
interp_context_evars ~program_mode:false ~impl_env:uimpls env_uparams sigma paramsl
in
(* Names of parameters as arguments of the inductive type (defs removed) *)
- let assums = List.filter is_local_assum ctx_params in
sigma, env_params, (ctx_params, env_uparams, ctx_uparams,
- List.map (RelDecl.get_name %> Name.get_id) assums, userimpls, useruimpls, impls, udecl)
+ userimpls, useruimpls, impls, udecl)
(* When a hole remains for a param, pretend the param is uniform and
do the unification.
@@ -482,11 +480,12 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
then user_err (str "Inductives with uniform parameters may not have attached notations.");
let indnames = List.map (fun ind -> ind.ind_name) indl in
+ let ninds = List.length indl in
(* In case of template polymorphism, we need to compute more constraints *)
let env0 = if poly then env0 else Environ.set_universes_lbound env0 UGraph.Bound.Prop in
- let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) =
+ let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, userimpls, useruimpls, impls, udecl) =
interp_params env0 udecl uparamsl paramsl
in
@@ -496,16 +495,17 @@ 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 lift1_ctx ctx =
+ let lift_ctx n ctx =
let t = EConstr.it_mkProd_or_LetIn EConstr.mkProp ctx in
- let t = EConstr.Vars.lift 1 t in
+ let t = EConstr.Vars.lift n 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
+ let ctx_params_lifted, fullarities =
+ lift_ctx ninds ctx_params,
+ CList.map_i
+ (fun i c -> EConstr.Vars.lift i (EConstr.it_mkProd_or_LetIn c ctx_params))
+ 0 arities
in
let env_ar = push_types env_uparams indnames relevances fullarities in
let env_ar_params = EConstr.push_rel_context ctx_params_lifted env_ar in
@@ -515,14 +515,15 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let impls = compute_internalization_env env_uparams sigma ~impls Inductive indnames fullarities indimpls in
let ntn_impls = compute_internalization_env env_uparams sigma Inductive indnames fullarities indimpls in
- let ninds = List.length indl in
let (sigma, _), constructors =
Metasyntax.with_syntax_protection (fun () ->
(* Temporary declaration of notations and scopes *)
List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations;
(* Interpret the constructor types *)
List.fold_left2_map
- (fun (sigma, ind_rel) -> interp_cstrs env_ar_params (sigma, ind_rel) impls ctx_params)
+ (fun (sigma, ind_rel) ind arity ->
+ interp_cstrs env_ar_params (sigma, ind_rel) impls ctx_params_lifted
+ ind (EConstr.Vars.liftn ninds (Rel.length ctx_params + 1) arity))
(sigma, ninds) indl arities)
()
in
@@ -540,7 +541,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let nuparams = Context.Rel.length ctx_uparams in
let uargs = Context.Rel.to_extended_vect EConstr.mkRel 0 ctx_uparams in
let uparam_subst =
- List.init (List.length indl) EConstr.(fun i -> mkApp (mkRel (i + 1 + nuparams), uargs))
+ List.init ninds EConstr.(fun i -> mkApp (mkRel (i + 1 + nuparams), uargs))
@ List.init nuparams EConstr.(fun i -> mkRel (i + 1)) in
let generalize_constructor c = EConstr.Unsafe.to_constr (EConstr.Vars.substnl uparam_subst nparams c) in
let cimpls = List.map pi3 constructors in
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 099a63cf8f..ae7878b615 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -725,7 +725,6 @@ module Obligation = struct
; obl_tac : unit Proofview.tactic option }
let set_type ~typ obl = {obl with obl_type = typ}
- let set_body ~body obl = {obl with obl_body = Some body}
end
type obligations = {obls : Obligation.t array; remaining : int}
@@ -2464,32 +2463,25 @@ let add_mutual_definitions l ~pm ~info ?obl_hook ~uctx
in
pm
-let admit_prog ~pm prg =
- let {obls; remaining} = Internal.get_obligations prg in
- let obls = Array.copy obls in
- Array.iteri
- (fun i x ->
- match x.obl_body with
- | None ->
- let x = subst_deps_obl obls x in
- let uctx = Internal.get_uctx prg in
- let univs = UState.univ_entry ~poly:false uctx in
- let kn = declare_constant ~name:x.obl_name ~local:Locality.ImportNeedQualified
- (ParameterEntry (None, (x.obl_type, univs), None)) ~kind:Decls.(IsAssumption Conjectural)
- in
- assumption_message x.obl_name;
- obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x
- | Some _ -> ())
- obls;
- Obls_.update_obls ~pm prg obls 0
-
-(* get_any_prog *)
+let rec admit_prog ~pm prg =
+ let {obls} = Internal.get_obligations prg in
+ let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
+ let i = match Array.findi is_open obls with
+ | Some i -> i
+ | None -> CErrors.anomaly (Pp.str "Could not find a solvable obligation.")
+ in
+ let proof = solve_obligation prg i None in
+ let pm = Proof.save_admitted ~pm ~proof in
+ match ProgMap.find_opt (Internal.get_name prg) pm with
+ | Some prg -> admit_prog ~pm (CEphemeron.get prg)
+ | None -> pm
+
let rec admit_all_obligations ~pm =
let prg = State.first_pending pm in
match prg with
| None -> pm
| Some prg ->
- let pm, _prog = admit_prog ~pm prg in
+ let pm = admit_prog ~pm prg in
admit_all_obligations ~pm
let admit_obligations ~pm n =
@@ -2497,7 +2489,7 @@ let admit_obligations ~pm n =
| None -> admit_all_obligations ~pm
| Some _ ->
let prg = get_unique_prog ~pm n in
- let pm, _ = admit_prog ~pm prg in
+ let pm = admit_prog ~pm prg in
pm
let next_obligation ~pm n tac =
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index cbd83e88b6..b134f7b82b 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -268,16 +268,16 @@ let custom_entry_locality = Summary.ref ~name:"LOCAL-CUSTOM-ENTRY" String.Set.em
let create_custom_entry ~local s =
if List.mem s ["constr";"pattern";"ident";"global";"binder";"bigint"] then
user_err Pp.(quote (str s) ++ str " is a reserved entry name.");
- let sc = "constr:"^s in
- let sp = "pattern:"^s in
+ let sc = "custom:"^s in
+ let sp = "custom_pattern:"^s in
let _ = extend_entry_command constr_custom_entry sc in
let _ = extend_entry_command pattern_custom_entry sp in
let () = if local then custom_entry_locality := String.Set.add s !custom_entry_locality in
()
let find_custom_entry s =
- let sc = "constr:"^s in
- let sp = "pattern:"^s in
+ let sc = "custom:"^s in
+ let sp = "custom_pattern:"^s in
try (find_custom_entry constr_custom_entry sc, find_custom_entry pattern_custom_entry sp)
with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".")
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index e0550fd744..49d4847fde 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -33,26 +33,26 @@ open Attributes
(* Rem: do not join the different GEXTEND into one, it breaks native *)
(* compilation on PowerPC and Sun architectures *)
-let query_command = Entry.create "vernac:query_command"
-
-let search_query = Entry.create "vernac:search_query"
-let search_queries = Entry.create "vernac:search_queries"
-
-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_token = Entry.create "vernac:def_token"
-let assumption_token = Entry.create "vernac:assumption_token"
-let def_body = Entry.create "vernac:def_body"
-let decl_notations = Entry.create "vernac:decl_notations"
-let record_field = Entry.create "vernac:record_field"
-let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion"
-let section_subset_expr = Entry.create "vernac:section_subset_expr"
-let scope_delimiter = Entry.create "vernac:scope_delimiter"
-let syntax_modifiers = Entry.create "vernac:syntax_modifiers"
-let only_parsing = Entry.create "vernac:only_parsing"
+let query_command = Entry.create "query_command"
+
+let search_query = Entry.create "search_query"
+let search_queries = Entry.create "search_queries"
+
+let subprf = Entry.create "subprf"
+
+let quoted_attributes = Entry.create "quoted_attributes"
+let class_rawexpr = Entry.create "class_rawexpr"
+let thm_token = Entry.create "thm_token"
+let def_token = Entry.create "def_token"
+let assumption_token = Entry.create "assumption_token"
+let def_body = Entry.create "def_body"
+let decl_notations = Entry.create "decl_notations"
+let record_field = Entry.create "record_field"
+let of_type_with_opt_coercion = Entry.create "of_type_with_opt_coercion"
+let section_subset_expr = Entry.create "section_subset_expr"
+let scope_delimiter = Entry.create "scope_delimiter"
+let syntax_modifiers = Entry.create "syntax_modifiers"
+let only_parsing = Entry.create "only_parsing"
let make_bullet s =
let open Proof_bullet in
@@ -436,12 +436,12 @@ GRAMMAR EXTEND Gram
| l = binders; ":="; b = lconstr -> { fun id ->
match b.CAst.v with
| CCast(b', (CastConv t|CastVM t|CastNative t)) ->
- (None,DefExpr(id,mkLambdaCN ~loc l b',Some (mkProdCN ~loc l t)))
+ (NoInstance,DefExpr(id,mkLambdaCN ~loc l b',Some (mkProdCN ~loc l t)))
| _ ->
- (None,DefExpr(id,mkLambdaCN ~loc l b,None)) } ] ]
+ (NoInstance,DefExpr(id,mkLambdaCN ~loc l b,None)) } ] ]
;
record_binder:
- [ [ id = name -> { (None,AssumExpr(id, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) }
+ [ [ id = name -> { (NoInstance,AssumExpr(id, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) }
| id = name; f = record_binder_body -> { f id } ] ]
;
assum_list:
@@ -452,13 +452,13 @@ GRAMMAR EXTEND Gram
;
simple_assum_coe:
[ [ idl = LIST1 ident_decl; oc = of_type_with_opt_coercion; c = lconstr ->
- { (not (Option.is_empty oc),(idl,c)) } ] ]
+ { (oc <> NoInstance,(idl,c)) } ] ]
;
constructor_type:
[[ l = binders;
t= [ coe = of_type_with_opt_coercion; c = lconstr ->
- { fun l id -> (not (Option.is_empty coe),(id,mkProdCN ~loc l c)) }
+ { fun l id -> (coe <> NoInstance,(id,mkProdCN ~loc l c)) }
| ->
{ fun l id -> (false,(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous, None)))) } ]
-> { t l }
@@ -469,12 +469,9 @@ GRAMMAR EXTEND Gram
[ [ id = identref; c=constructor_type -> { c id } ] ]
;
of_type_with_opt_coercion:
- [ [ ":>>" -> { Some false }
- | ":>"; ">" -> { Some false }
- | ":>" -> { Some true }
- | ":"; ">"; ">" -> { Some false }
- | ":"; ">" -> { Some true }
- | ":" -> { None } ] ]
+ [ [ ":>" -> { BackInstance }
+ | ":"; ">" -> { BackInstance }
+ | ":" -> { NoInstance } ] ]
;
END
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 762c95fffe..c16eaac516 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -71,6 +71,9 @@ let rec contract3' env sigma a b c = function
| ConversionFailed (env',t1,t2) ->
let (env',t1,t2) = contract2 env' sigma t1 t2 in
contract3 env sigma a b c, ConversionFailed (env',t1,t2)
+ | IncompatibleInstances (env',ev,t1,t2) ->
+ let (env',ev,t1,t2) = contract3 env' sigma (EConstr.mkEvar ev) t1 t2 in
+ contract3 env sigma a b c, IncompatibleInstances (env',EConstr.destEvar sigma ev,t1,t2)
| NotSameArgSize | NotSameHead | NoCanonicalStructure
| MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities
| UnifUnivInconsistency _ as x -> contract3 env sigma a b c, x
@@ -313,6 +316,13 @@ let explain_unification_error env sigma p1 p2 = function
let t1, t2 = pr_explicit env sigma t1 t2 in
[str "cannot unify " ++ t1 ++ strbrk " and " ++ t2]
else []
+ | IncompatibleInstances (env,ev,t1,t2) ->
+ let env = make_all_name_different env sigma in
+ let ev = pr_leconstr_env env sigma (EConstr.mkEvar ev) in
+ let t1 = Reductionops.nf_betaiota env sigma t1 in
+ let t2 = Reductionops.nf_betaiota env sigma t2 in
+ let t1, t2 = pr_explicit env sigma t1 t2 in
+ [ev ++ strbrk " has otherwise to unify with " ++ t1 ++ str " which is incompatible with " ++ t2]
| MetaOccurInBody evk ->
[str "instance for " ++ quote (pr_existential_key sigma evk) ++
strbrk " refers to a metavariable - please report your example" ++
@@ -689,34 +699,29 @@ let explain_cannot_unify_binding_type env sigma m n =
str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "."
let explain_cannot_find_well_typed_abstraction env sigma p l e =
- let p = EConstr.to_constr sigma p in
str "Abstracting over the " ++
str (String.plural (List.length l) "term") ++ spc () ++
- hov 0 (pr_enum (fun c -> pr_lconstr_env env sigma (EConstr.to_constr sigma c)) l) ++ spc () ++
- str "leads to a term" ++ spc () ++ pr_ltype_env ~goal_concl_style:true env sigma p ++
+ hov 0 (pr_enum (fun c -> pr_leconstr_env env sigma c) l) ++ spc () ++
+ str "leads to a term" ++ spc () ++ pr_letype_env ~goal_concl_style:true env sigma p ++
spc () ++ str "which is ill-typed." ++
(match e with None -> mt () | Some e -> fnl () ++ str "Reason is: " ++ e)
let explain_wrong_abstraction_type env sigma na abs expected result =
- let abs = EConstr.to_constr sigma abs in
- let expected = EConstr.to_constr sigma expected in
- let result = EConstr.to_constr sigma result in
let ppname = match na with Name id -> Id.print id ++ spc () | _ -> mt () in
str "Cannot instantiate metavariable " ++ ppname ++ strbrk "of type " ++
- pr_lconstr_env env sigma expected ++ strbrk " with abstraction " ++
- pr_lconstr_env env sigma abs ++ strbrk " of incompatible type " ++
- pr_lconstr_env env sigma result ++ str "."
+ pr_leconstr_env env sigma expected ++ strbrk " with abstraction " ++
+ pr_leconstr_env env sigma abs ++ strbrk " of incompatible type " ++
+ pr_leconstr_env env sigma result ++ str "."
let explain_abstraction_over_meta _ m n =
strbrk "Too complex unification problem: cannot find a solution for both " ++
Name.print m ++ spc () ++ str "and " ++ Name.print n ++ str "."
let explain_non_linear_unification env sigma m t =
- let t = EConstr.to_constr sigma t in
strbrk "Cannot unambiguously instantiate " ++
Name.print m ++ str ":" ++
strbrk " which would require to abstract twice on " ++
- pr_lconstr_env env sigma t ++ str "."
+ pr_leconstr_env env sigma t ++ str "."
let explain_unsatisfied_constraints env sigma cst =
strbrk "Unsatisfied constraints: " ++
@@ -803,10 +808,10 @@ let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1
explain_unification_error env sigma c1 c2 (Some e)
in
str "Found incompatible occurrences of the pattern" ++ str ":" ++
- spc () ++ str "Matched term " ++ pr_lconstr_env env sigma (EConstr.to_constr sigma t2) ++
+ spc () ++ str "Matched term " ++ pr_leconstr_env env sigma t2 ++
strbrk " at position " ++ pr_position (cl2,pos2) ++
strbrk " is not compatible with matched term " ++
- pr_lconstr_env env sigma (EConstr.to_constr sigma t1) ++ strbrk " at position " ++
+ pr_leconstr_env env sigma t1 ++ strbrk " at position " ++
pr_position (cl1,pos1) ++ ppreason ++ str "."
let pr_constraints printenv env sigma evars cstrs =
@@ -1287,9 +1292,8 @@ let explain_recursion_scheme_error env = function
(* Pattern-matching errors *)
let explain_bad_pattern env sigma cstr ty =
- let ty = EConstr.to_constr sigma ty in
let env = make_all_name_different env sigma in
- let pt = pr_lconstr_env env sigma ty in
+ let pt = pr_leconstr_env env sigma ty in
let pc = pr_constructor env cstr in
str "Found the constructor " ++ pc ++ brk(1,1) ++
str "while matching a term of type " ++ pt ++ brk(1,1) ++
@@ -1326,12 +1330,11 @@ let explain_non_exhaustive env pats =
spc () ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats)
let explain_cannot_infer_predicate env sigma typs =
- let inj c = EConstr.to_constr sigma c in
- let typs = Array.map_to_list (fun (c1, c2) -> (inj c1, inj c2)) typs in
+ let typs = Array.to_list typs in
let env = make_all_name_different env sigma in
let pr_branch (cstr,typ) =
- let cstr,_ = decompose_app cstr in
- str "For " ++ pr_lconstr_env env sigma cstr ++ str ": " ++ pr_lconstr_env env sigma typ
+ let cstr,_ = EConstr.decompose_app sigma cstr in
+ str "For " ++ pr_leconstr_env env sigma cstr ++ str ": " ++ pr_leconstr_env env sigma typ
in
str "Unable to unify the types found in the branches:" ++
spc () ++ hov 0 (prlist_with_sep fnl pr_branch typs)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index ab1ce44081..58b1698848 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -85,7 +85,7 @@ 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)
+let pr_custom_grammar name = pr_registered_grammar ("custom:"^name)
(**********************************************************************)
(* Parse a format (every terminal starting with a letter or a single
@@ -1614,7 +1614,14 @@ let add_notation_in_scope ~local deprecation df env c mods scope =
let sd = compute_syntax_data ~local deprecation df mods in
(* Prepare the parsing and printing rules *)
let sy_pa_rules = make_parsing_rules sd in
- let sy_pp_rules = make_printing_rules false sd in
+ let sy_pp_rules, gen_sy_pp_rules =
+ match sd.only_parsing, Ppextend.has_generic_notation_printing_rule (fst sd.info) with
+ | true, true -> None, None
+ | onlyparse, has_generic ->
+ let rules = make_printing_rules false sd in
+ let _ = check_reserved_format (fst sd.info) rules in
+ (if onlyparse then None else rules),
+ (if has_generic then None else (* We use the format of this notation as the default *) rules) in
(* Prepare the interpretation *)
let i_vars = make_internalization_vars sd.recvars sd.mainvars sd.intern_typs in
let nenv = {
@@ -1638,10 +1645,6 @@ let add_notation_in_scope ~local deprecation df env c mods scope =
notobj_notation = (notation, location);
notobj_specific_pp_rules = sy_pp_rules;
} in
- let gen_sy_pp_rules =
- if Ppextend.has_generic_notation_printing_rule (fst sd.info) then None
- else sy_pp_rules (* We use the format of this notation as the default *) in
- let _ = check_reserved_format (fst sd.info) sy_pp_rules in
(* Ready to change the global state *)
List.iter (fun f -> f ()) sd.msgs;
Lib.add_anonymous_leaf (inSyntaxExtension (local, (sy_pa_rules,gen_sy_pp_rules)));
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index b73e7c7515..f972e05d3b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -503,9 +503,8 @@ let pr_lconstrarg c =
let pr_intarg n = spc () ++ int n
let pr_oc = function
- | None -> str" :"
- | Some true -> str" :>"
- | Some false -> str" :>>"
+ | NoInstance -> str" :"
+ | BackInstance -> str" :>"
let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = ntn }) =
let prx = match x with
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index f4cb1adfe8..c9f68eed57 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -10,7 +10,9 @@
open Pcoq
-let uvernac = create_universe "vernac"
+[@@@ocaml.warning "-3"]
+let uvernac = create_universe "vernac" [@@deprecated "Deprecated in 8.13"]
+[@@@ocaml.warning "+3"]
type proof_mode = string
@@ -35,20 +37,18 @@ let command_entry_ref = ref None
module Vernac_ =
struct
- let gec_vernac s = Entry.create ("vernac:" ^ s)
-
(* The different kinds of vernacular commands *)
- let gallina = gec_vernac "gallina"
- let gallina_ext = gec_vernac "gallina_ext"
- let command = gec_vernac "command"
- let syntax = gec_vernac "syntax_command"
- let vernac_control = gec_vernac "Vernac.vernac_control"
- let rec_definition = gec_vernac "Vernac.rec_definition"
- let red_expr = new_entry utactic "red_expr"
- let hint_info = gec_vernac "hint_info"
+ let gallina = Entry.create "gallina"
+ let gallina_ext = Entry.create "gallina_ext"
+ let command = Entry.create "command"
+ let syntax = Entry.create "syntax_command"
+ let vernac_control = Entry.create "Vernac.vernac_control"
+ let rec_definition = Entry.create "Vernac.rec_definition"
+ let red_expr = Entry.create "red_expr"
+ let hint_info = Entry.create "hint_info"
(* Main vernac entry *)
let main_entry = Entry.create "vernac"
- let noedit_mode = gec_vernac "noedit_command"
+ let noedit_mode = Entry.create "noedit_command"
let () =
let act_vernac v loc = Some v in
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 1718024edd..8ab4af7d48 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -12,7 +12,9 @@ open Pcoq
open Genredexpr
open Vernacexpr
-val uvernac : gram_universe
+[@@@ocaml.warning "-3"]
+val uvernac : gram_universe [@@deprecated "Deprecated in 8.13"]
+[@@@ocaml.warning "+3"]
type proof_mode
diff --git a/vernac/record.ml b/vernac/record.ml
index bd5b71cd6b..e362cb052a 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -518,7 +518,7 @@ let implicits_of_context ctx =
(List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
let declare_class def cumulative ubinders univs id idbuild paramimpls params univ arity
- template fieldimpls fields ?(kind=Decls.StructureComponent) coers priorities =
+ template fieldimpls fields ?(kind=Decls.StructureComponent) coers =
let fieldimpls =
(* Make the class implicit in the projections, and the params if applicable. *)
let impls = implicits_of_context params in
@@ -556,26 +556,27 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
Impargs.declare_manual_implicits false cref paramimpls;
Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd fieldimpls);
Classes.set_typeclass_transparency (EvalConstRef cst) false false;
- let sub = match List.hd coers with
- | Some b -> Some ((if b then Backward else Forward), List.hd priorities)
- | None -> None
- in
- [cref, [Name proj_name, sub, Some proj_cst]]
+ let sub = List.hd coers in
+ let m = {
+ meth_name = Name proj_name;
+ meth_info = sub;
+ meth_const = Some proj_cst;
+ } in
+ [cref, [m]]
| _ ->
let record_data = [id, idbuild, univ, arity, fieldimpls, fields, false,
List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in
let inds = declare_structure ~cumulative Declarations.BiFinite ubinders univs paramimpls
params template ~kind:Decls.Method ~name:[|binder_name|] record_data
in
- let coers = List.map2 (fun coe pri ->
- Option.map (fun b ->
- if b then Backward, pri else Forward, pri) coe)
- coers priorities
- in
let map ind =
- let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y)
- (List.rev fields) coers (Recordops.lookup_projections ind)
- in GlobRef.IndRef ind, l
+ let map decl b y = {
+ meth_name = RelDecl.get_name decl;
+ meth_info = b;
+ meth_const = y;
+ } in
+ let l = List.map3 map (List.rev fields) coers (Recordops.lookup_projections ind) in
+ GlobRef.IndRef ind, l
in
List.map map inds
in
@@ -731,16 +732,21 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite records =
| [r], [d] -> r, d
| _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
in
- let priorities = List.map (fun (_, { rf_priority }) -> {hint_priority = rf_priority ; hint_pattern = None}) cfs in
- let coers = List.map (fun (_, { rf_subclass }) -> rf_subclass) cfs in
+ let coers = List.map (fun (_, { rf_subclass=coe; rf_priority=pri }) ->
+ match coe with
+ | Vernacexpr.BackInstance -> Some {hint_priority = pri ; hint_pattern = None}
+ | Vernacexpr.NoInstance -> None)
+ cfs
+ in
declare_class def cumulative ubinders univs id.CAst.v idbuild
- implpars params univ arity template implfs fields coers priorities
+ implpars params univ arity template implfs fields coers
| _ ->
let map impls = implpars @ [CAst.make None] @ impls in
let data = List.map (fun (univ, arity, implfs, fields) -> (univ, arity, List.map map implfs, fields)) data in
let map (univ, arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
- { pf_subclass = not (Option.is_empty rf_subclass);
+ { pf_subclass =
+ (match rf_subclass with Vernacexpr.BackInstance -> true | Vernacexpr.NoInstance -> false);
pf_canonical = rf_canonical })
cfs
in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index fba6800729..fe27d9ac8a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -776,7 +776,7 @@ let vernac_inductive ~atts kind indl =
| _ -> 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 coe' = if coe then BackInstance else NoInstance in
let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce),
{ rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in
vernac_record ~template udecl ~cumulative (Class true) ~poly finite [id, bl, c, None, [f]]
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index d8e17d00e3..eeebb43114 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -106,8 +106,7 @@ type search_restriction =
type verbose_flag = bool (* true = Verbose; false = Silent *)
type coercion_flag = bool (* true = AddCoercion false = NoCoercion *)
-type instance_flag = bool option
- (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
+type instance_flag = BackInstance | NoInstance
type export_flag = bool (* true = Export; false = Import *)
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 496b1a43d1..eacb7fe6cb 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -247,7 +247,7 @@ let vernac_argument_extend ~name arg =
let () = Pcoq.register_grammar wit e in
e
| Arg_rules rules ->
- let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
+ let e = Pcoq.create_generic_entry2 name (Genarg.rawwit wit) in
let () = Pcoq.grammar_extend e {Pcoq.pos=None; data=[(None, None, rules)]} in
e
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 02:09:46 +0000