From df77da121b86c64a91ea729f39afc92f10676893 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 11 Apr 2008 12:33:08 +0000
Subject: Check that no evars remain in instance types earlier at Instance
 declarations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10779 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/subtac/subtac_classes.ml | 1 +
 toplevel/classes.ml              | 3 +++
 2 files changed, 4 insertions(+)

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 0bff421383..4b4a6458b9 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -194,6 +194,7 @@ let new_instance ctx (instid, bk, cl) props pri =
       Evarutil.nf_isevar !isevars t
   in
   isevars := undefined_evars !isevars;
+  Evarutil.check_evars env Evd.empty !isevars termtype;
 (*   let imps =  *)
 (*     Util.list_map_i  *)
 (*       (fun i binder -> *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 203fe118d3..a539a87baa 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -485,6 +485,7 @@ let new_instance ctx (instid, bk, cl) props ?(tac:Proof_type.tactic option) ?(ho
   in
     if Lib.is_modtype () then
       begin
+	Evarutil.check_evars env Evd.empty !isevars termtype;
 	let cst = Declare.declare_internal_constant id
 	  (Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
 	in
@@ -533,7 +534,9 @@ let new_instance ctx (instid, bk, cl) props ?(tac:Proof_type.tactic option) ?(ho
 	    Typeclasses.add_instance inst;
 	    (match hook with Some h -> h cst | None -> ())
 	in
+	let termtype = Evarutil.nf_isevar !isevars termtype in
 	let evm = Evd.evars_of (undefined_evars !isevars) in
+	  Evarutil.check_evars env Evd.empty !isevars termtype;
 	  if evm = Evd.empty then
 	    let cdecl = 
 	      let kind = IsDefinition Instance in
-- 
cgit v1.2.3