From ee90aac584d123fa709d6629d99057b62bb343d0 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 10 Feb 2008 14:10:38 +0000
Subject: 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
---
 contrib/subtac/subtac_classes.ml     | 18 +++++++++++-------
 contrib/subtac/subtac_obligations.ml |  4 ++--
 2 files changed, 13 insertions(+), 9 deletions(-)

(limited to 'contrib')

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 = 
-- 
cgit v1.2.3