diff options
| author | ppedrot | 2013-06-30 01:49:24 +0000 |
|---|---|---|
| committer | ppedrot | 2013-06-30 01:49:24 +0000 |
| commit | 66b6a5540c63b2a690082d479e483d4f52a73d76 (patch) | |
| tree | 09462e65cfcd7f03d0373f12ac0cc308a93d09ac | |
| parent | 2fd40ff72d3b7b54422b9b00b394c9c446cb5cd7 (diff) | |
Fixing Camlp4 compilation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16613 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | grammar/argextend.ml4 | 13 | ||||
| -rw-r--r-- | parsing/compat.ml4 | 13 |
2 files changed, 19 insertions, 7 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 57cde5c8cd..eb4630394b 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -16,21 +16,20 @@ open Compat let loc = CompatLoc.ghost let default_loc = <:expr< Loc.ghost >> -let qualified_name s = +let qualified_name loc s = let path = CString.split '.' s in let (name, path) = CList.sep_last path in - let fold dir accu = <:expr< $uid:dir$.$accu$ >> in - List.fold_right fold path <:expr< $lid:name$ >> + qualified_name loc path name -let mk_extraarg s = +let mk_extraarg loc s = if Extrawit.tactic_genarg_level s = None then try let name = Genarg.get_name0 s in - qualified_name name + qualified_name loc name with Not_found -> <:expr< $lid:"wit_"^s$ >> else - qualified_name ("Extrawit.wit_" ^ s) + qualified_name loc ("Extrawit.wit_" ^ s) let rec make_wit loc = function | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >> @@ -51,7 +50,7 @@ let rec make_wit loc = function | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> | PairArgType (t1,t2) -> <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >> - | ExtraArgType s -> mk_extraarg s + | ExtraArgType s -> mk_extraarg loc s let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >> let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >> diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index e82f352742..f872c4a2d8 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -310,3 +310,16 @@ let expl_anti loc e = <:expr< $anti:e$ >> ELSE let expl_anti _loc e = e (* FIXME: understand someday if we can do better *) END + +(** Qualified names in OCaml *) + +IFDEF CAMLP5 THEN +let qualified_name loc path name = + let fold dir accu = <:expr< $uid:dir$.$accu$ >> in + List.fold_right fold path <:expr< $lid:name$ >> +ELSE +let qualified_name loc path name = + let fold dir accu = Ast.IdAcc (loc, Ast.IdUid (loc, dir), accu) in + let path = List.fold_right fold path (Ast.IdLid (loc, name)) in + Ast.ExId (loc, path) +END |