diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 1 | ||||
| -rw-r--r-- | contrib/subtac/g_subtac.ml4 | 5 |
2 files changed, 5 insertions, 1 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index f6aad378d8..72b609b24d 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -11,6 +11,7 @@ (* $Id$ *) (*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4use: "pa_extend.cmo" i*) open Options open Util diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index d6040646e8..7fd08c7b05 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -6,13 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4use: "pa_extend.cmo" i*) + + (* Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *) (* $Id$ *) -(*i camlp4deps: "parsing/grammar.cma" i*) open Options open Util |