diff options
| author | msozeau | 2008-06-03 23:08:00 +0000 |
|---|---|---|
| committer | msozeau | 2008-06-03 23:08:00 +0000 |
| commit | 908900165bc6a5b2eb9bc4f177311ee2409dbd6a (patch) | |
| tree | 8fc23b2e62b06e7a9be28e4bce9fcbb77c4a12fe /toplevel | |
| parent | e984c9a611936280e2c0e4a1d4b1739c3d32f4dd (diff) | |
Fixes incorrect handling of existing existentials variables in
typeclass code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11047 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 8 | ||||
| -rw-r--r-- | toplevel/command.ml | 3 |
2 files changed, 5 insertions, 6 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 333a26f035..db5c548553 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -512,8 +512,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau in let env' = push_named_context ctx' env in isevars := Evarutil.nf_evar_defs !isevars; - let sigma = Evd.evars_of !isevars in - isevars := resolve_typeclasses env sigma !isevars; + isevars := resolve_typeclasses env !isevars; let sigma = Evd.evars_of !isevars in let substctx = Typeclasses.nf_substitution sigma subst in let imps = @@ -569,10 +568,10 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau let term = Evarutil.nf_isevar !isevars term in let evm = Evd.evars_of (undefined_evars !isevars) in Evarutil.check_evars env Evd.empty !isevars termtype; - isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env evm !isevars; if evm = Evd.empty then declare_instance_constant k pri global imps ?hook id term termtype - else + else begin + isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !isevars; let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in Flags.silently (fun () -> Command.start_proof id kind termtype @@ -584,6 +583,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau (match tac with Some tac -> Pfedit.by tac | None -> ())) (); Flags.if_verbose (msg $$ Printer.pr_open_subgoals) (); id + end end let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition diff --git a/toplevel/command.ml b/toplevel/command.ml index 11b849c4f7..518ae25cf1 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -844,8 +844,7 @@ let interp_recursive fixkind l boxed = let evd,_ = consider_remaining_unif_problems env_rec !evdref in let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in - let evd = Typeclasses.resolve_typeclasses - ~onlyargs:false ~fail:true env (evars_of evd) evd in + let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in List.iter (check_evars env_rec Evd.empty evd) fixdefs; List.iter (check_evars env Evd.empty evd) fixtypes; check_mutuality env kind (List.combine fixnames fixdefs); |