Backport Program Instance into Instance. Proper early error message if

trying to declare an instance with an already existing name. Add
possibility of not giving all the fields in Instance declarations, using
Refine.refine to generate the subgoals. No control over opacity in this
case though...


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10548 85f007b7-540e-0410-9357-904b9bb8a0f7

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 =