diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comPrimitive.ml | 8 | ||||
| -rw-r--r-- | vernac/declare.ml | 10 | ||||
| -rw-r--r-- | vernac/himsg.ml | 25 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 9 |
4 files changed, 40 insertions, 12 deletions
diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml index 110dcdc98a..eaa5271a73 100644 --- a/vernac/comPrimitive.ml +++ b/vernac/comPrimitive.ml @@ -38,7 +38,13 @@ let do_primitive id udecl prim typopt = Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env) env evd typ in - let evd = Evarconv.unify_delay env evd typ expected_typ in + let evd = try Evarconv.unify_delay env evd typ expected_typ + with Evarconv.UnableToUnify (evd,e) as exn -> + let _, info = Exninfo.capture exn in + Exninfo.iraise (Pretype_errors.( + PretypeError (env,evd,CannotUnify (typ,expected_typ,Some e)),info)) + in + Pretyping.check_evars_are_solved ~program_mode:false env evd; let evd = Evd.minimize_universes evd in let uvars = EConstr.universes_of_constr evd typ in let evd = Evd.restrict_universe_context evd uvars in diff --git a/vernac/declare.ml b/vernac/declare.ml index 12a261517f..eedbee852b 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1152,13 +1152,6 @@ let declare_mutual_definition ~pm l = Some (List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes) | IsCoFixpoint -> None in - (* In the future we will pack all this in a proper record *) - (* XXX: info refactoring *) - let _kind = - if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) - else Decls.(IsDefinition CoFixpoint) - in - let scope = first.prg_info.Info.scope in (* Declare the recursive definitions *) let kns = declare_mutually_recursive_core ~info:first.prg_info ~ntns:first.prg_notations @@ -1167,6 +1160,7 @@ let declare_mutual_definition ~pm l = in (* Only for the first constant *) let dref = List.hd kns in + let scope = first.prg_info.Info.scope in let s_hook = {Hook.S.uctx = first.prg_uctx; obls; scope; dref} in Hook.call ?hook:first.prg_info.Info.hook s_hook; (* XXX: We call the obligation hook here, by consistency with the @@ -1503,7 +1497,7 @@ let start_mutual_with_initialization ~info ~cinfo ~mutual_info sigma snl = in match cinfo with | [] -> CErrors.anomaly (Pp.str "No proof to start.") - | { CInfo.name; typ; impargs; _} :: thms -> + | { CInfo.name; typ; _} :: thms -> let pinfo = Proof_info.make ~cinfo ~info ~compute_guard () in (* start_lemma has the responsibility to add (name, impargs, typ) to thms, once Info.t is more refined this won't be necessary *) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index f9ecf10d1b..762c95fffe 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1252,6 +1252,29 @@ let explain_inductive_error = function error_large_non_prop_inductive_not_in_type () | MissingConstraints csts -> error_inductive_missing_constraints csts +(* Primitive errors *) + +let explain_incompatible_prim_declarations (type a) (act:a Primred.action_kind) (x:a) (y:a) = + let open Primred in + let env = Global.env() in + (* The newer constant/inductive (either coming from Primitive or a + Require) may be absent from the nametab as the error got raised + while adding it to the safe_env. In that case we can't use + nametab printing. + + There are still cases where the constant/inductive is added + separately from its retroknowledge (using Register), so we still + try nametab based printing. *) + match act with + | IncompatTypes typ -> + let px = try pr_constant env x with Not_found -> Constant.print x in + str "Cannot declare " ++ px ++ str " as primitive " ++ str (CPrimitives.prim_type_to_string typ) ++ + str ": " ++ pr_constant env y ++ str " is already declared." + | IncompatInd ind -> + let px = try pr_inductive env x with Not_found -> MutInd.print (fst x) in + str "Cannot declare " ++ px ++ str " as primitive " ++ str (CPrimitives.prim_ind_to_string ind) ++ + str ": " ++ pr_inductive env y ++ str " is already declared." + (* Recursion schemes errors *) let explain_recursion_scheme_error env = function @@ -1386,6 +1409,8 @@ let rec vernac_interp_error_handler = function explain_typeclass_error env sigma te | InductiveError e -> explain_inductive_error e + | Primred.IncompatibleDeclarations (act,x,y) -> + explain_incompatible_prim_declarations act x y | Modops.ModuleTypingError e -> explain_module_error e | Modintern.ModuleInternalizationError e -> diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index e9b86f323b..6cc48d0e48 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1579,9 +1579,12 @@ let warn_irrelevant_format = let make_printing_rules reserved (sd : SynData.syn_data) = let open SynData in let custom,level,_ = sd.level in - let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in - if sd.only_parsing then (if sd.format <> None then warn_irrelevant_format (); None) - else Some { + let format = + if sd.only_parsing && sd.format <> None then (warn_irrelevant_format (); None) + else sd.format in + let pp_rule = make_pp_rule level sd.pp_syntax_data format in + (* We produce a generic rule even if this precise notation is only parsing *) + Some { synext_reserved = reserved; synext_unparsing = (pp_rule,level); synext_extra = sd.extra; |