diff options
| author | ppedrot | 2012-10-04 11:53:07 +0000 |
|---|---|---|
| committer | ppedrot | 2012-10-04 11:53:07 +0000 |
| commit | 5b6582f8d47975f6f4f394cf44a1c65c799d43ff (patch) | |
| tree | e1be15920daf8b2e5ae788f57e772e79ddaacd30 /grammar/q_util.ml4 | |
| parent | 621625757d04bdb19075d92e764749d0a1393ce3 (diff) | |
Moved Compat to parsing. This permits to break the dependency of the
kernel on CAMLP4/5 structures, and consequently should also erase
such structures from vo files.
This modification requires some code duplication, mainly while
reimplementing our own location data type. This is chiefly visible
in the ml4 files, where CAMLP4/5 locations must be manually converted
to our locations with an explicit (!@) cast operator.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar/q_util.ml4')
| -rw-r--r-- | grammar/q_util.ml4 | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index 895584703a..eee84c38db 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -14,27 +14,27 @@ let mlexpr_of_list f l = List.fold_right (fun e1 e2 -> let e1 = f e1 in - let loc = Loc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< [$e1$ :: $e2$] >>) - l (let loc = Loc.ghost in <:expr< [] >>) + l (let loc = CompatLoc.ghost in <:expr< [] >>) let mlexpr_of_pair m1 m2 (a1,a2) = let e1 = m1 a1 and e2 = m2 a2 in - let loc = Loc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< ($e1$, $e2$) >> let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)= let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in - let loc = Loc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in + let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in <:expr< ($e1$, $e2$, $e3$) >> let mlexpr_of_quadruple m1 m2 m3 m4 (a1,a2,a3,a4)= let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 and e4 = m4 a4 in - let loc = Loc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e4) in + let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e4) in <:expr< ($e1$, $e2$, $e3$, $e4$) >> (* We don't give location for tactic quotation! *) -let loc = Loc.ghost +let loc = CompatLoc.ghost let mlexpr_of_bool = function |