diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-04 15:06:59 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-04 15:06:59 +0000 |
| commit | a62c7d7ebd7c650710c8a48eec8dab6b7f18f26e (patch) | |
| tree | cbddbccbcc1a7ba14feac5c9318e78d63300c420 /contrib | |
| parent | 8f3627741f9d4624851abc7de1f3bda28b7acf9a (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/subtac/subtac_pretyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 0703bcb83..aba11231c 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 |