diff options
| author | Hugo Herbelin | 2015-09-23 18:25:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-09-23 18:25:15 +0200 |
| commit | 2ba2ca96be88bad5cd75a02c94cc48ef4f5209b7 (patch) | |
| tree | 7546ab8a3bf1a0e2b5a75028e9efcade1d8d4321 /toplevel/record.ml | |
| parent | 13716dc6561a3379ba130f07ce7ecd1df379475c (diff) | |
Hopefully better names to constructors of internal_flag, as discussed
with Enrico.
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 484fd081df..e214f9ca71 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -298,7 +298,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field const_entry_inline_code = false; const_entry_feedback = None } in let k = (DefinitionEntry entry,IsDefinition kind) in - let kn = declare_constant ~internal:KernelSilent fid k in + let kn = declare_constant ~internal:InternalTacticRequest fid k in let constr_fip = let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in applist (mkConstU (kn,u),proj_args) |