diff options
| author | herbelin | 2002-12-03 15:05:57 +0000 |
|---|---|---|
| committer | herbelin | 2002-12-03 15:05:57 +0000 |
| commit | 7a1636ec58c426059ff6864edd12868087b7f93c (patch) | |
| tree | 54215ffb7943dbaeb95d3630f24fae5f711f7e72 /interp/constrextern.ml | |
| parent | a9b09fd9c99307b3ffc9660ba53ce0460aeabece (diff) | |
Préparation à la prise en compte des changements de scopes internes aux notations; bugs d'affichage (confusion key/scope dans les délimiteurs); bug de non-indépendance des règles d'affichage et parsing vis à vis du nom des variables de la notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3365 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 1a398c6655..9e86405cc1 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -111,7 +111,7 @@ let rec extern_cases_pattern_in_scope scopes pat = let (sc,n) = Symbols.uninterp_cases_numeral pat in match Symbols.availability_of_numeral sc scopes with | None -> raise No_match - | Some scopt -> insert_pat_delimiters (CPatNumeral (loc,n)) scopt + | Some key -> insert_pat_delimiters (CPatNumeral (loc,n)) key with No_match -> match pat with | PatVar (_,Name id) -> CPatAtom (loc,Some (Ident (loc,id))) @@ -283,7 +283,7 @@ and extern_eqn scopes (loc,ids,pl,c) = and extern_numeral scopes t (sc,n) = match Symbols.availability_of_numeral sc scopes with | None -> raise No_match - | Some scopt -> insert_delimiters (CNumeral (loc,n)) scopt + | Some key -> insert_delimiters (CNumeral (loc,n)) key and extern_symbol scopes t = function | [] -> raise No_match @@ -305,10 +305,11 @@ and extern_symbol scopes t = function (* Uninterpretation is not allowed in current context *) | None -> raise No_match (* Uninterpretation is allowed in current context *) - | Some scopt -> + | Some (scopt,key) -> let scopes = option_cons scopt scopes in - let l = list_map_assoc (extern scopes) subst in - insert_delimiters (CNotation (loc,ntn,l)) scopt) + let l = + List.map (fun (c,scl) -> extern (scl@scopes) c) subst in + insert_delimiters (CNotation (loc,ntn,l)) key) | SynDefRule kn -> CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in if args = [] then e |