diff options
| author | herbelin | 2009-08-14 14:54:56 +0000 |
|---|---|---|
| committer | herbelin | 2009-08-14 14:54:56 +0000 |
| commit | 60ddeba351613457bf921e1db58d63dd2c9ee64f (patch) | |
| tree | 2a74a2c44c02c2f8f6524e0bdc4d22f546779a28 /parsing | |
| parent | 6af2902ddd8ea6d4171b882726e9bb4d2fc45748 (diff) | |
Added profile.cmo in grammar.cma so that any functions in one of the
files embedded in grammar.cma can be profiled with the Profile module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12279 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/grammar.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib index 9e714352b1..4356db844e 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -1,5 +1,6 @@ Coq_config +Profile Pp_control Pp Compat |