diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comInductive.ml | 25 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 17 | ||||
| -rw-r--r-- | vernac/vernacextend.ml | 24 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 9 |
5 files changed, 33 insertions, 44 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index edb03a5c89..718e62b9b7 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -329,10 +329,7 @@ let template_polymorphism_candidate ~ctor_levels uctx params concl = if not concltemplate then false else let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in - let params, conclunivs = - IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu - in - not (Univ.LSet.is_empty conclunivs) + Option.has_some @@ IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu | Entries.Polymorphic_entry _ -> false let check_param = function @@ -370,6 +367,14 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames (* Build the inductive entries *) let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) -> + { mind_entry_typename = indname; + mind_entry_arity = arity; + mind_entry_consnames = cnames; + mind_entry_lc = ctypes + }) + indnames arities arityconcl constructors + in + let template = List.map4 (fun indname (templatearity, _) concl (_, ctypes) -> let template_candidate () = templatearity || let ctor_levels = @@ -385,22 +390,17 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames in template_polymorphism_candidate ~ctor_levels uctx ctx_params concl in - let template = match template with + match template with | Some template -> if poly && template then user_err Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible."); template | None -> should_auto_template indname (template_candidate ()) - in - { mind_entry_typename = indname; - mind_entry_arity = arity; - mind_entry_template = template; - mind_entry_consnames = cnames; - mind_entry_lc = ctypes - }) + ) indnames arities arityconcl constructors in + let is_template = List.for_all (fun t -> t) template in (* Build the mutual inductive entry *) let mind_ent = { mind_entry_params = ctx_params; @@ -409,6 +409,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames mind_entry_inds = entries; mind_entry_private = if private_ind then Some false else None; mind_entry_universes = uctx; + mind_entry_template = is_template; mind_entry_cumulative = poly && cumulative; } in diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 33fd14a731..10946d78f0 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1708,7 +1708,7 @@ let add_infix ~local deprecation env ({CAst.loc;v=inf},modifiers) pr sc = (* check the precedence *) let vars = names_of_constr_expr pr in let x = Namegen.next_ident_away (Id.of_string "x") vars in - let y = Namegen.next_ident_away (Id.of_string "y") vars in + let y = Namegen.next_ident_away (Id.of_string "y") (Id.Set.add x vars) in let metas = [inject_var x; inject_var y] in let c = mkAppC (pr,metas) in let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in diff --git a/vernac/record.ml b/vernac/record.ml index 3e44cd85cc..065641989d 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -423,7 +423,13 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in - let template = + { mind_entry_typename = id; + mind_entry_arity = arity; + mind_entry_consnames = [idbuild]; + mind_entry_lc = [type_constructor] } + in + let blocks = List.mapi mk_block record_data in + let check_template (id, _, min_univ, _, _, fields, _, _) = let template_candidate () = (* we use some dummy values for the arities in the rel_context as univs_of_constr doesn't care about localassums and @@ -454,14 +460,8 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa | None, template -> (* auto detect template *) ComInductive.should_auto_template id (template && template_candidate ()) - in - { mind_entry_typename = id; - mind_entry_arity = arity; - mind_entry_template = template; - mind_entry_consnames = [idbuild]; - mind_entry_lc = [type_constructor] } in - let blocks = List.mapi mk_block record_data in + let template = List.for_all check_template record_data in let primitive = !primitive_flag && List.for_all (fun (_,_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data @@ -473,6 +473,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa mind_entry_inds = blocks; mind_entry_private = None; mind_entry_universes = univs; + mind_entry_template = template; mind_entry_cumulative = poly && cumulative; } in diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index e0afb7f483..5d38ea32be 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -92,28 +92,18 @@ let warn_deprecated_command = (* Interpretation of a vernac command *) let type_vernac opn converted_args ~atts = - let phase = ref "Looking up command" in - try - let depr, callback = vinterp_map opn in - let () = if depr then + let depr, callback = vinterp_map opn in + let () = if depr then let rules = Egramml.get_extend_vernac_rule opn in let pr_gram = function - | Egramml.GramTerminal s -> str s - | Egramml.GramNonTerminal _ -> str "_" + | Egramml.GramTerminal s -> str s + | Egramml.GramNonTerminal _ -> str "_" in let pr = pr_sequence pr_gram rules in warn_deprecated_command pr; - in - phase := "Checking arguments"; - let hunk = callback converted_args in - phase := "Executing command"; - hunk ~atts - with - | reraise -> - let reraise = Exninfo.capture reraise in - if !Flags.debug then - Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); - Exninfo.iraise reraise + in + let hunk = callback converted_args in + hunk ~atts (** VERNAC EXTEND registering *) diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 59557a60a6..280343f315 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -18,12 +18,9 @@ module Parser = struct let parse ps entry pa = Pcoq.unfreeze ps; - Flags.with_option Flags.we_are_parsing (fun () -> - try Pcoq.Entry.parse entry pa - with e when CErrors.noncritical e -> - let (e, info) = Exninfo.capture e in - Exninfo.iraise (e, info)) - () + Flags.with_option Flags.we_are_parsing + (fun () -> Pcoq.Entry.parse entry pa) + () end |