diff options
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 0dd18f064..1ef51496b 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -277,9 +277,6 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map pi1 ctx))) -let qualid_of_con c = - Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c)) - let declare_instance_cst glob con = let instance = Typeops.type_of_constant (Global.env ()) con in let _, r = decompose_prod_assum instance in |