diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-19 15:29:48 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-19 15:29:48 +0000 |
commit | 1b089eb0231b4bd6d4cafb30f9e051bb53665978 (patch) | |
tree | 489e0f8ce7b4a80db388c63219b9cf4380b7f185 /pretyping/pretype_errors.ml | |
parent | 259dde7928696593c2d3c6de474f5cf50fa4417d (diff) |
Add (almost) compatibility with camlp4, without breaking support for camlp5
The choice between camlp4/5 is done during configure with flags
-usecamlp5 (default for the moment) vs. -usecamlp4.
Currently, to have a full camlp4 compatibility, you need to change
all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
into "`EOI" in grammar entries. I've a sed script that does that
(actually the converse), but I prefer to re-think it and check a few
things before branching this sed into the build mechanism.
lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
and try to propose a common interface (cf LexerSig / GrammarSig).
A few incompatible quotations have been turned into underlying code
manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
parsable by both camlp4 and 5. See in particular the fate of
<:str_item< declare ... end >>
Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
This forces to use camlp5 > 5.01.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretype_errors.ml')
-rw-r--r-- | pretyping/pretype_errors.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 6adaee81c..5b829e5bf 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Util -open Stdpp open Names open Sign open Term @@ -41,7 +41,7 @@ exception PretypeError of env * pretype_error let precatchable_exception = function | Util.UserError _ | TypeError _ | PretypeError _ - | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | + | Loc.Exc_located(_,(Util.UserError _ | TypeError _ | Nametab.GlobalizationError _ | PretypeError _)) -> true | _ -> false @@ -96,10 +96,10 @@ let contract3 env a b c = match contract env [a;b;c] with | env, [a;b;c] -> env,a,b,c | _ -> assert false let raise_pretype_error (loc,ctx,sigma,te) = - Stdpp.raise_with_loc loc (PretypeError(env_ise sigma ctx,te)) + Loc.raise loc (PretypeError(env_ise sigma ctx,te)) let raise_located_type_error (loc,ctx,sigma,te) = - Stdpp.raise_with_loc loc (TypeError(env_ise sigma ctx,te)) + Loc.raise loc (TypeError(env_ise sigma ctx,te)) let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty = @@ -155,11 +155,11 @@ let error_occur_check env sigma ev c = let error_not_clean env sigma ev c (loc,k) = let c = nf_evar sigma c in - raise_with_loc loc + Loc.raise loc (PretypeError (env_ise sigma env, NotClean (ev,c,k))) let error_unsolvable_implicit loc env sigma evi e explain = - raise_with_loc loc + Loc.raise loc (PretypeError (env_ise sigma env, UnsolvableImplicit (evi, e, explain))) let error_cannot_unify env sigma (m,n) = |