diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-26 16:17:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-26 16:17:38 +0000 |
| commit | aadcf42183225553b8e5dcf49685ecb59459af58 (patch) | |
| tree | 1ba2f2f69650f4cf1191bc16838a51b79795f228 /interp/constrextern.ml | |
| parent | 22c9662db9caef7fbb3f51d89e17fb4aa3d52646 (diff) | |
Réaffichage des Syntactic Definition (printer constr_expr).
Affinement de la gestion des niveaux de constr.
Cablage en dur du parsing et de l'affichage des délimiteurs de scopes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3295 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index c813cf71d..68bcd1235 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -26,6 +26,7 @@ open Topconstr open Rawterm open Pattern open Nametab +open Symbols (*i*) (* Translation from rawconstr to front constr *) @@ -285,7 +286,7 @@ and extern_numeral scopes t (sc,n) = and extern_symbol scopes t = function | [] -> raise No_match - | (sc,ntn,pat,n as rule)::rules -> + | (keyrule,pat,n as rule)::rules -> try (* Adjusts to the number of arguments expected by the notation *) let (t,args) = match t,n with @@ -296,16 +297,21 @@ and extern_symbol scopes t = function (* Try matching ... *) let subst = match_aconstr t pat in (* Try availability of interpretation ... *) - (match Symbols.availability_of_notation (sc,ntn) scopes with - (* Uninterpretation is not allowed in current context *) - | None -> raise No_match - (* Uninterpretation is allowed in current context *) - | Some scopt -> - let scopes = option_cons scopt scopes in - let l = List.map (fun (id,c) -> (id,extern scopes c)) subst in - let e = insert_delimiters (CNotation (loc,ntn,l)) scopt in - if args = [] then e - else explicitize [] e (List.map (extern scopes) args)) + let e = + match keyrule with + | NotationRule (sc,ntn) -> + (match Symbols.availability_of_notation (sc,ntn) scopes with + (* Uninterpretation is not allowed in current context *) + | None -> raise No_match + (* Uninterpretation is allowed in current context *) + | Some scopt -> + let scopes = option_cons scopt scopes in + let l = list_map_assoc (extern scopes) subst in + insert_delimiters (CNotation (loc,ntn,l)) scopt) + | SynDefRule kn -> + CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in + if args = [] then e + else explicitize [] e (List.map (extern scopes) args) with No_match -> extern_symbol scopes t rules |