From 1b089eb0231b4bd6d4cafb30f9e051bb53665978 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 19 May 2010 15:29:48 +0000 Subject: 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 --- pretyping/typeclasses_errors.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'pretyping/typeclasses_errors.ml') diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 869a7845d..983942aba 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -16,6 +16,7 @@ open Environ open Nametab open Mod_subst open Topconstr +open Compat open Util open Libnames (*i*) @@ -45,7 +46,7 @@ let unsatisfiable_constraints env evd ev = raise (TypeClassError (env, UnsatisfiableConstraints (evd, None))) | Some ev -> let loc, kind = Evd.evar_source ev evd in - raise (Stdpp.Exc_located (loc, TypeClassError + raise (Loc.Exc_located (loc, TypeClassError (env, UnsatisfiableConstraints (evd, Some (ev, kind))))) let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m)) @@ -53,5 +54,5 @@ let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstan let rec unsatisfiable_exception exn = match exn with | TypeClassError (_, UnsatisfiableConstraints _) -> true - | Stdpp.Exc_located(_, e) -> unsatisfiable_exception e + | Loc.Exc_located(_, e) -> unsatisfiable_exception e | _ -> false -- cgit v1.2.3