diff options
| author | msozeau | 2009-11-06 22:41:38 +0000 |
|---|---|---|
| committer | msozeau | 2009-11-06 22:41:38 +0000 |
| commit | 6d684ec32bc62ff1e9528081a2369852cc5b5c65 (patch) | |
| tree | 9a972ff099f0ad26296cb0802008cda401dc8ee7 | |
| parent | 4237fa16d23101bc05ebc9a3dad168be4f3f64d8 (diff) | |
- Fix discharge bug in typeclasses: some constrs were not actually
discharged on the other definitions in the section.
- Avoid universe problem in generalize_eqs were we could give an
[@eq_refl Set x x] proof where an [@eq Type x x] was expected.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12478 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/typeclasses.ml | 10 | ||||
| -rw-r--r-- | tactics/tactics.ml | 1 |
2 files changed, 8 insertions, 3 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 38fca2f193..1b8c5a2331 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -132,6 +132,7 @@ let subst_class (subst,cl) = cl_projs = do_subst_projs cl.cl_projs; } let discharge_class (_,cl) = + let repl = Lib.replacement_context () in let rel_of_variable_context ctx = List.fold_right ( fun (n,_,b,t) (ctx', subst) -> let decl = (Name n, Option.map (substn_vars 1 subst) b, substn_vars 1 subst t) in @@ -143,7 +144,8 @@ let discharge_class (_,cl) = (fun (id, b, t) (ctx, k) -> (id, Option.smartmap (substn_vars k subst) b, substn_vars k subst t) :: ctx, succ k) rel ([], n) - in ctx in + in map_rel_context (Cooking.expmod_constr repl) ctx + in let abs_context cl = match cl.cl_impl with | VarRef _ | ConstructRef _ -> assert false @@ -157,9 +159,11 @@ let discharge_class (_,cl) = if cl_impl' == cl.cl_impl then cl else let ctx = abs_context cl in let ctx, subst = rel_of_variable_context ctx in + let context = discharge_context ctx subst cl.cl_context in + let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in { cl_impl = cl_impl'; - cl_context = discharge_context ctx subst cl.cl_context; - cl_props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props; + cl_context = context; + cl_props = props; cl_projs = list_smartmap (fun (x, y) -> x, Option.smartmap Lib.discharge_con y) cl.cl_projs } let rebuild_class cl = cl diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b9d2d9cfef..97006c9e91 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2291,6 +2291,7 @@ let abstract_args gl generalize_vars dep id = List.hd rel, c in let argty = pf_type_of gl arg in + let argty = if isSort argty then new_Type () else argty in let liftargty = lift (List.length ctx) argty in let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in match kind_of_term arg with |