diff options
| author | herbelin | 2004-03-30 12:20:50 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-30 12:20:50 +0000 |
| commit | 06f1e9bcd8f846628665a3d83b0e2b30e190f41e (patch) | |
| tree | b12ea5b110fc631a2263fc333a60af44f913001e | |
| parent | c7d8caa601c12b35ed0568aff9fa54e22a742474 (diff) | |
Distinction entre declarations internes (p.ex. _subproof) et declarations utilisateurs pour export xml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5615 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 89cb35b74b..36d83bb28d 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -183,7 +183,7 @@ let declare_projections indsp coers fields = const_entry_type = Some projtyp; const_entry_opaque = false } in let k = (DefinitionEntry cie,IsDefinition) in - let sp = declare_constant fid k in + let sp = declare_internal_constant fid k in Options.if_verbose message (string_of_id fid ^" is defined"); sp with Type_errors.TypeError (ctx,te) -> |