diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:50 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:50 +0000 |
| commit | 392300a73bc4e57d2be865d9a8d77c608ef02f59 (patch) | |
| tree | 44b4f39e7f92f29f4626d4aa8265fe68eb129111 /interp/syntax_def.ml | |
| parent | a936f2e879ac1f9b2e7e9d8a5376469e3d53c606 (diff) | |
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/syntax_def.ml')
| -rw-r--r-- | interp/syntax_def.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index eb6f50131..f20d9727d 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -11,7 +11,7 @@ open Util open Pp open Names open Libnames -open Topconstr +open Notation_term open Libobject open Lib open Nameops @@ -38,7 +38,7 @@ let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) = Nametab.push_syndef (Nametab.Until i) sp kn let is_alias_of_already_visible_name sp = function - | _,ARef ref -> + | _,NRef ref -> let (dir,id) = repr_qualid (shortest_qualid_of_global Idset.empty ref) in dir = empty_dirpath && id = basename sp | _ -> @@ -58,7 +58,7 @@ let cache_syntax_constant d = open_syntax_constant 1 d let subst_syntax_constant (subst,(local,pat,onlyparse)) = - (local,subst_interpretation subst pat,onlyparse) + (local,Topconstr.subst_interpretation subst pat,onlyparse) let classify_syntax_constant (local,_,_ as o) = if local then Dispose else Substitute o @@ -71,7 +71,7 @@ let in_syntax_constant : bool * interpretation * bool -> obj = subst_function = subst_syntax_constant; classify_function = classify_syntax_constant } -type syndef_interpretation = (identifier * subscopes) list * aconstr +type syndef_interpretation = (identifier * subscopes) list * notation_constr (* Coercions to the general format of notation that also supports variables bound to list of expressions *) |