diff options
| author | Maxime Dénès | 2017-06-23 17:04:53 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-23 17:04:53 +0200 |
| commit | f5a746eca3866b4652ead49548d08b2fe460960c (patch) | |
| tree | 8bdbc6aad06fe2ba7460ad39a743519df3aa6e8b /vernac/classes.ml | |
| parent | 8d92701f1a017354504c84d60c9e76da50feaf49 (diff) | |
| parent | ec8523065abfb68aff9bd3664869224419885385 (diff) | |
Merge PR#762: [vernac] Fix unneeded mutual references in Obligations
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 007b70bc0f..2e8ebb8531 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -417,7 +417,7 @@ let context poly l = let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in let hook = Lemmas.mk_hook (fun _ gr -> gr) in - let _ = Command.declare_definition id decl entry [] [] hook in + let _ = DeclareDef.declare_definition id decl entry [] [] hook in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus |