1 files changed, 86 insertions, 0 deletions
diff --git a/grammar/gramCompat.mlp b/grammar/gramCompat.mlp
new file mode 100644
index 00000000..6246da7b
--- /dev/null
+++ b/grammar/gramCompat.mlp
@@ -0,0 +1,86 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Compatibility file depending on ocaml/camlp4 version *)
+
+(** Misc module emulation *)
+
+IFDEF CAMLP5 THEN
+
+module CompatLoc = struct
+  include Ploc
+  let ghost = dummy
+  let merge = encl
+end
+
+ELSE
+
+module CompatLoc = Camlp4.PreCast.Loc
+
+END
+
+IFDEF CAMLP5 THEN
+
+module PcamlSig = struct end
+
+ELSE
+
+module PcamlSig = Camlp4.Sig
+module Ast = Camlp4.PreCast.Ast
+module Pcaml = Camlp4.PreCast.Syntax
+module MLast = Ast
+
+END
+
+(** Compatibility with camlp5 strict mode *)
+IFDEF CAMLP5 THEN
+  IFDEF STRICT THEN
+    let vala x = Ploc.VaVal x
+  ELSE
+    let vala x = x
+  END
+ELSE
+  let vala x = x
+END
+
+(** Fix a quotation difference in [str_item] *)
+
+let declare_str_items loc l =
+IFDEF CAMLP5 THEN
+  MLast.StDcl (loc, vala l) (* correspond to <:str_item< declare $list:l'$ end >> *)
+ELSE
+  Ast.stSem_of_list l
+END
+
+(** Quotation difference for match clauses *)
+
+let default_patt loc =
+  (<:patt< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>)
+
+IFDEF CAMLP5 THEN
+
+let make_fun loc cl =
+  let l = cl @ [default_patt loc] in
+  MLast.ExFun (loc, vala l)  (* correspond to <:expr< fun [ $list:l$ ] >> *)
+
+ELSE
+
+let make_fun loc cl =
+  let mk_when = function
+    | Some w -> w
+    | None -> Ast.ExNil loc
+  in
+  let mk_clause (patt,optwhen,expr) =
+    (* correspond to <:match_case< ... when ... -> ... >> *)
+    Ast.McArr (loc, patt, mk_when optwhen, expr) in
+  let init = mk_clause (default_patt loc) in
+  let add_clause x acc = Ast.McOr (loc, mk_clause x, acc) in
+  let l = List.fold_right add_clause cl init in
+  Ast.ExFun (loc,l) (* correspond to <:expr< fun [ $l$ ] >> *)
+
+END