diff options
| author | msozeau | 2008-08-21 15:49:30 +0000 |
|---|---|---|
| committer | msozeau | 2008-08-21 15:49:30 +0000 |
| commit | 70aa6184a399ebf2b70bf284ad57fc4e4dd5c226 (patch) | |
| tree | ffc803cda254ce791f81e48b763b4d5e84dfe990 /toplevel/command.ml | |
| parent | 994048e670339c3709f7735446b40341d21aa6a9 (diff) | |
Various fixes w.r.t typeclasses and subtac: resolve tcs properly inside
inductive and Program defs. Fix eterm bug when generating obligations
and remove optimization of let-in removal which prevents factorization
of proofs/"asserts" in Program.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11330 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 413146ca7d..f18cecb207 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -539,6 +539,7 @@ let interp_mutual paramsl indl notations finite = (* Instantiate evars and check all are resolved *) let evd,_ = consider_remaining_unif_problems env_params !evdref in + let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in let sigma = evars_of evd in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in |