diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 18:01:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 18:21:25 +0100 |
| commit | 3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (patch) | |
| tree | 45fdbfc2fd03e30105d1ead1e184bdf6ef822de8 /pretyping/inductiveops.ml | |
| parent | cca57bcd89770e76e1bcc21eb41756dca2c51425 (diff) | |
| parent | 4fd59386e7f60d16bfe9858c372b354d422ac0b6 (diff) | |
Merge branch 'master'.
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 9e823ab4c..d5967c4bf 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -24,14 +24,14 @@ open Context.Rel.Declaration let type_of_inductive env (ind,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - Typeops.check_hyps_inclusion env (mkInd ind) mib.mind_hyps; + Typeops.check_hyps_inclusion env mkInd ind mib.mind_hyps; Inductive.type_of_inductive env (specif,u) (* Return type as quoted by the user *) let type_of_constructor env (cstr,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Typeops.check_hyps_inclusion env (mkConstruct cstr) mib.mind_hyps; + Typeops.check_hyps_inclusion env mkConstruct cstr mib.mind_hyps; Inductive.type_of_constructor (cstr,u) specif (* Return constructor types in user form *) @@ -632,7 +632,7 @@ let type_of_projection_knowing_arg env sigma p c ty = raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type") in let (_,u), pars = dest_ind_family pars in - substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u)) + substl (c :: List.rev pars) (Typeops.type_of_projection_constant env (p,u)) (***********************************************) (* Guard condition *) |