diff options
| author | Gaëtan Gilbert | 2020-02-07 13:54:23 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-12 13:10:38 +0100 |
| commit | 30a2f4c5469e25038f5720f03e948519efeef48d (patch) | |
| tree | e12198192b5c8b7a9a9fdc2c69834f5c1ce2059e /pretyping/inductiveops.ml | |
| parent | 6c1de3455d5cd79958a8e26ac728f7d5d1b8d025 (diff) | |
ReferenceVariables error contains a globref instead of a constr
The previous system was from before globref was in the kernel.
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 36b405e981..816a8c4703 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -28,14 +28,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 (GlobRef.IndRef 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 (GlobRef.ConstructRef cstr) mib.mind_hyps; Inductive.type_of_constructor (cstr,u) specif (* Return constructor types in user form *) |