diff options
| author | herbelin | 2002-10-12 14:32:51 +0000 |
|---|---|---|
| committer | herbelin | 2002-10-12 14:32:51 +0000 |
| commit | 455d9130fb9c55315173e2a32b9bc334e95bba16 (patch) | |
| tree | b491888dd1b9f86e681d2766653a3dcaad244ba1 /pretyping/syntax_def.ml | |
| parent | 72fb50ce5d3e802aadff66495a0e90065f2fab42 (diff) | |
Restriction sur la forme des Syntactic Definition et re-localisation en fonction de l'endroit d'utilisation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3117 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/syntax_def.ml')
| -rw-r--r-- | pretyping/syntax_def.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml index dc5824dc71..0bb144867b 100644 --- a/pretyping/syntax_def.ml +++ b/pretyping/syntax_def.ml @@ -65,4 +65,13 @@ let (in_syntax_constant, out_syntax_constant) = let declare_syntactic_definition id c = let _ = add_leaf id (in_syntax_constant c) in () -let search_syntactic_definition kn = KNmap.find kn !syntax_table +let rec set_loc loc = function + | RRef (_,a) -> RRef (loc,a) + | RVar (_,a) -> RVar (loc,a) + | RApp (_,a,b) -> RApp (loc,set_loc loc a,List.map (set_loc loc) b) + | RSort (_,a) -> RSort (loc,a) + | RHole (_,a) -> RHole (loc,a) + | a -> warning "Unrelocatated syntactic definition"; a + +let search_syntactic_definition loc kn = + set_loc loc (KNmap.find kn !syntax_table) |