diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-14 18:38:14 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-14 18:38:14 +0000 |
commit | fd7448ad0f44ef306d910816d7b6d2f6a303f4a7 (patch) | |
tree | 5a5c51c01bbbaa75a4ddffcca384cdf5cc7d0d2e /pretyping/typeclasses.ml | |
parent | 23a51bab686dd0ceaa9a87b09beb49d0ee0575c4 (diff) |
Delayed the computation of parameters in sort polymorphism of
inductive types. This saves some computation, but also allows
incidentally to retype terms with evars without failing if an
inductive type as an argument whose type is an evar.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16526 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typeclasses.ml')
-rw-r--r-- | pretyping/typeclasses.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 9e2175624..c14f107ec 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -384,7 +384,7 @@ let add_inductive_class ind = let ctx = oneind.mind_arity_ctxt in let ty = Inductive.type_of_inductive_knowing_parameters (push_rel_context ctx (Global.env ())) - oneind (Termops.extended_rel_vect 0 ctx) + oneind (Array.map (fun x -> lazy x) (Termops.extended_rel_vect 0 ctx)) in { cl_impl = IndRef ind; cl_context = List.map (const None) ctx, ctx; |