diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/argextend.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_decl_mode.ml4 | 5 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_minicoq.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_prim.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 3 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/g_xml.ml4 | 2 | ||||
| -rw-r--r-- | parsing/lexer.ml4 | 5 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 2 | ||||
| -rw-r--r-- | parsing/q_constr.ml4 | 2 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 2 | ||||
| -rw-r--r-- | parsing/q_util.ml4 | 2 | ||||
| -rw-r--r-- | parsing/tacextend.ml4 | 2 | ||||
| -rw-r--r-- | parsing/vernacextend.ml4 | 2 |
17 files changed, 41 insertions, 3 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index ebe2b2893..7585ad4d8 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) + (* $Id$ *) open Genarg diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index ecb2e132a..5e68c7308 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4use: "pa_extend.cmo" i*) + (* $Id$ *) open Pcoq diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4 index 8942b6541..91433b8a6 100644 --- a/parsing/g_decl_mode.ml4 +++ b/parsing/g_decl_mode.ml4 @@ -6,8 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) (*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) + +(* $Id$ *) + open Decl_expr open Names diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 5755aee64..3c5c88e89 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4use: "pa_extend.cmo" i*) + (* $Id$ *) open Pp diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4 index 1c838f238..fe7906f63 100644 --- a/parsing/g_minicoq.ml4 +++ b/parsing/g_minicoq.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4use: "pa_extend.cmo" i*) + (* $Id$ *) open Pp diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 73c88540c..d2d5ad36a 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4use: "pa_extend.cmo" i*) + (*i $Id$ i*) open Pcoq diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index e13962ce8..b564828a5 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -6,8 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4use: "pa_extend.cmo" i*) + (* $Id$ *) + open Pcoq open Pp open Tactic diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 7ec88618d..ff23fb225 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4use: "pa_extend.cmo" i*) + (* $Id$ *) open Pp diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c128ff7af..c61dfbf63 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -6,8 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) (*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4use: "pa_extend.cmo" i*) + +(* $Id$ *) + open Pp open Util diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index dea45ac11..cd929e5af 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4use: "pa_extend.cmo" i*) + (* $Id$ *) open Pp diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 9f7e422d7..043a0c08a 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -8,6 +8,11 @@ (*i $Id$ i*) + +(*i camlp4use: "pr_o.cmo" i*) +(* Add pr_o.cmo to circumvent a useless-warning bug when preprocessed with + * ast-based camlp4 *) + open Pp open Token diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 68659bb3e..161a08bfa 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4use: "pa_extend.cmo" i*) + (*i $Id$ i*) open Pp diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 21c851dfb..d8ce0a570 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) + (* $Id: g_constr.ml4,v 1.58 2005/12/30 10:55:32 herbelin Exp $ *) open Rawterm diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index e03d5d7c0..f5bab5d69 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4use: "pa_ifdef.cmo" i*) +(*i camlp4use: "q_MLast.cmo pa_ifdef.cmo" i*) (* $Id$ *) diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index f7ea7ee46..7c684cdc1 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4use: "q_MLast.cmo" i*) + (* $Id$ *) (* This file defines standard combinators to build ml expressions *) diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 7e32879d2..476732a3f 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) + (* $Id$ *) open Genarg diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 5e8337fe9..3c8526c08 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) + (* $Id$ *) open Genarg |