From a62c7d7ebd7c650710c8a48eec8dab6b7f18f26e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 4 Jan 2008 15:06:59 +0000
Subject: Add partial setoids in theories/Classes, add SetoidDec class for
 setoids with a decidable equality. Fix name capture bug, again.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10419 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/subtac/subtac_pretyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib')

diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 0703bcb837..aba11231cd 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -118,7 +118,6 @@ let env_with_binders env isevars l =
 
 let subtac_process env isevars id bl c tycon =
 (*   let bl = Implicit_quantifiers.ctx_of_class_binders (vars_of_env env) cbl @ l in *)
-  let imps = Implicit_quantifiers.implicits_of_binders bl in
   let c = Command.abstract_constr_expr c bl in
   let tycon = 
     match tycon with
@@ -130,6 +129,7 @@ let subtac_process env isevars id bl c tycon =
 	    mk_tycon coqt
   in    
   let c = coqintern_constr !isevars env c in
+  let imps = Implicit_quantifiers.implicits_of_rawterm c in
   let coqc, ctyp = interp env isevars c tycon in
   let evm = non_instanciated_map env isevars (evars_of !isevars) in
     evm, coqc, ctyp, imps
-- 
cgit v1.2.3