diff options
| author |  vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-29 09:41:09 +0000 |
|---|---|---|
| committer | vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-29 09:41:09 +0000 |
| commit | 4dce356eacb7b9804c2e2398447dbbc3b0dc1383 (patch) | |
| tree | 14f44a67e0d0ec5e835792ec238ac2a1ed7a59f5 /toplevel/record.ml | |
| parent | 7e2f953c3c19904616c43990fada92e762aadec9 (diff) | |
change the flag "internal" in declare/ind_tables from bool to
a 3 state type to allow:
* KernelVerbose / KernelSilent : handle the display of messages launch by Coq
* UserVerbose : handle the display of messages launch by user actions
Coq will still behaves the same way (TODOs in the code mark the places
where we can now change the behaviour). I'll remove them in a few days
when we'll have agreed on the correct behaviour.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13217 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index e4177b0fc..89bf76911 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -259,7 +259,8 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls mind_entry_record = true; mind_entry_finite = recursivity_flag_of_kind finite; mind_entry_inds = [mie_ind] } in - let kn = Command.declare_mutual_inductive_with_eliminations true mie [(paramimpls,[])] in +(* TODO : maybe switch to KernelVerbose *) + let kn = Command.declare_mutual_inductive_with_eliminations KernelSilent mie [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in |