diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/discharge.ml | 122 | ||||
| -rw-r--r-- | vernac/discharge.mli | 14 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 13 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
4 files changed, 10 insertions, 141 deletions
diff --git a/vernac/discharge.ml b/vernac/discharge.ml deleted file mode 100644 index 0e4bbd2993..0000000000 --- a/vernac/discharge.ml +++ /dev/null @@ -1,122 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open CErrors -open Util -open Term -open Vars -open Declarations -open Cooking -open Entries -open Context.Rel.Declaration - -(********************************) -(* Discharging mutual inductive *) - -let detype_param = - function - | LocalAssum (Name id, p) -> id, LocalAssumEntry p - | LocalDef (Name id, p,_) -> id, LocalDefEntry p - | _ -> anomaly (Pp.str "Unnamed inductive local variable.") - -(* Replace - - Var(y1)..Var(yq):C1..Cq |- Ij:Bj - Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti - - by - - |- Ij: (y1..yq:C1..Cq)Bj - I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)] -*) - -let abstract_inductive decls nparamdecls inds = - let ntyp = List.length inds in - let ndecls = Context.Named.length decls in - let args = Context.Named.to_instance mkVar (List.rev decls) in - let args = Array.of_list args in - let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in - let inds' = - List.map - (function (tname,arity,template,cnames,lc) -> - let lc' = List.map (substl subs) lc in - let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b decls) lc' in - let arity' = Termops.it_mkNamedProd_wo_LetIn arity decls in - (tname,arity',template,cnames,lc'')) - inds in - let nparamdecls' = nparamdecls + Array.length args in -(* To be sure to be the same as before, should probably be moved to process_inductive *) - let params' = let (_,arity,_,_,_) = List.hd inds' in - let (params,_) = decompose_prod_n_assum nparamdecls' arity in - List.map detype_param params - in - let ind'' = - List.map - (fun (a,arity,template,c,lc) -> - let _, short_arity = decompose_prod_n_assum nparamdecls' arity in - let shortlc = - List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in - { mind_entry_typename = a; - mind_entry_arity = short_arity; - mind_entry_template = template; - mind_entry_consnames = c; - mind_entry_lc = shortlc }) - inds' - in (params',ind'') - -let refresh_polymorphic_type_of_inductive (_,mip) = - match mip.mind_arity with - | RegularArity s -> s.mind_user_arity, false - | TemplateArity ar -> - let ctx = List.rev mip.mind_arity_ctxt in - mkArity (List.rev ctx, Type ar.template_level), true - -let process_inductive (section_decls,_,_ as info) modlist mib = - let section_decls = Lib.named_of_variable_context section_decls in - let nparamdecls = Context.Rel.length mib.mind_params_ctxt in - let subst, ind_univs = - match mib.mind_universes with - | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx - | Polymorphic_ind auctx -> - let subst, auctx = Lib.discharge_abstract_universe_context info auctx in - let auctx = Univ.AUContext.repr auctx in - subst, Polymorphic_ind_entry auctx - | Cumulative_ind cumi -> - let auctx = Univ.ACumulativityInfo.univ_context cumi in - let subst, auctx = Lib.discharge_abstract_universe_context info auctx in - let auctx = Univ.AUContext.repr auctx in - subst, Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context auctx) - in - let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in - let inds = - Array.map_to_list - (fun mip -> - let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in - let arity = discharge ty in - let lc = Array.map discharge mip.mind_user_lc in - (mip.mind_typename, - arity, template, - Array.to_list mip.mind_consnames, - Array.to_list lc)) - mib.mind_packets in - let section_decls' = Context.Named.map discharge section_decls in - let (params',inds') = abstract_inductive section_decls' nparamdecls inds in - let record = match mib.mind_record with - | Some (Some (id, _, _)) -> Some (Some id) - | Some None -> Some None - | None -> None - in - { mind_entry_record = record; - mind_entry_finite = mib.mind_finite; - mind_entry_params = params'; - mind_entry_inds = inds'; - mind_entry_private = mib.mind_private; - mind_entry_universes = ind_univs - } - diff --git a/vernac/discharge.mli b/vernac/discharge.mli deleted file mode 100644 index c8c7e3b8b8..0000000000 --- a/vernac/discharge.mli +++ /dev/null @@ -1,14 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Declarations -open Entries -open Opaqueproof - -val process_inductive : - Lib.abstr_info -> work_list -> mutual_inductive_body -> mutual_inductive_entry diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 5298ef2e44..b2d48bb2f9 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -991,7 +991,7 @@ let is_not_printable onlyparse nonreversible = function (warn_non_reversible_notation (); true) else onlyparse -let find_precedence lev etyps symbols = +let find_precedence lev etyps symbols onlyprint = let first_symbol = let rec aux = function | Break _ :: t -> aux t @@ -1009,8 +1009,13 @@ let find_precedence lev etyps symbols = | None -> [],0 | Some (NonTerminal x) -> (try match List.assoc x etyps with - | ETConstr _ -> - user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") + | ETConstr _ -> + if onlyprint then + if Option.is_empty lev then + user_err Pp.(str "Explicit level needed in only-printing mode when the level of the leftmost non-terminal is given.") + else [],Option.get lev + else + user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") | ETName | ETBigint | ETReference -> begin match lev with | None -> @@ -1134,7 +1139,7 @@ let compute_syntax_data df modifiers = let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in let ntn_for_grammar = if need_squash then make_notation_key symbols_for_grammar else ntn_for_interp in if not onlyprint then check_rule_productivity symbols_for_grammar; - let msgs,n = find_precedence mods.level mods.etyps symbols in + let msgs,n = find_precedence mods.level mods.etyps symbols onlyprint in (* To globalize... *) let etyps = join_auxiliary_recursive_types recvars mods.etyps in let sy_typs, prec = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 83296cf58f..203d913db8 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1785,7 +1785,7 @@ let vernac_locate = let open Feedback in function (Constrextern.without_symbols pr_lglob_constr) ntn sc) | LocateLibrary qid -> print_located_library qid | LocateModule qid -> msg_notice (print_located_module qid) - | LocateTactic qid -> msg_notice (print_located_tactic qid) + | LocateOther (s, qid) -> msg_notice (print_located_other s qid) | LocateFile f -> msg_notice (locate_file f) let vernac_register id r = |