diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/subtac/subtac_classes.ml | 18 | ||||
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 4 |
2 files changed, 13 insertions, 9 deletions
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index f605988440..fb15e41b6a 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -151,6 +151,17 @@ let new_instance ctx (instid, bk, cl) props = let cl = Option.get (class_of_constr c) in cl, ctx, []) in + let id = + match snd instid with + Name id -> + let sp = Lib.make_path id in + if Nametab.exists_cci sp then + errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists"); + id + | Anonymous -> + let i = Nameops.add_suffix k.cl_name "_instance_0" in + Termops.next_global_ident_away false i (Termops.ids_of_context env) + in let env' = Classes.push_named_context ctx' env in isevars := Evarutil.nf_evar_defs !isevars; let sigma = Evd.evars_of !isevars in @@ -192,13 +203,6 @@ let new_instance ctx (instid, bk, cl) props = Evarutil.nf_isevar !isevars t in isevars := undefined_evars !isevars; - let id = - match snd instid with - Name id -> id - | Anonymous -> - let i = Nameops.add_suffix k.cl_name "_instance_" in - Termops.next_global_ident_away false i (Termops.ids_of_context env) - in let imps = Util.list_map_i (fun i (na, b, t) -> ExplByPos (i, Some na), (true, true)) diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index b7777e6222..a6639abbcf 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -156,7 +156,7 @@ let declare_definition prg = let gr = ConstRef c in if Impargs.is_implicit_args () || prg.prg_implicits <> [] then Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits; - print_message (definition_message c); + print_message (Subtac_utils.definition_message c); prg.prg_hook c; c @@ -217,7 +217,7 @@ let declare_obligation obl body = let constant = Declare.declare_constant obl.obl_name (DefinitionEntry ce,IsProof Property) in - print_message (definition_message constant); + print_message (Subtac_utils.definition_message constant); { obl with obl_body = Some (mkConst constant) } let try_tactics obls = |