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/constrintern.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/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7236335c3..e8e42a7b4 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -274,8 +274,8 @@ let rec intern_cases_pattern scopes aliases = function | CPatNumeral (loc, n) -> ([aliases], Symbols.interp_numeral_as_pattern loc n (alias_of aliases) scopes) - | CPatDelimiters (_, sc, e) -> - intern_cases_pattern (sc::scopes) aliases e + | CPatDelimiters (loc, key, e) -> + intern_cases_pattern (find_delimiters_scope loc key::scopes) aliases e | CPatAtom (loc, Some head) -> (match maybe_constructor head with | ConstrPat c -> @@ -396,8 +396,8 @@ let internalise sigma env allow_soapp lvar c = (Symbols.interp_notation ntn scopes) | CNumeral (loc, n) -> Symbols.interp_numeral loc n scopes - | CDelimiters (loc, sc, e) -> - intern (ids,impls,sc::scopes) e + | CDelimiters (loc, key, e) -> + intern (ids,impls,find_delimiters_scope loc key::scopes) e | CAppExpl (loc, ref, args) -> let (f,_,args_scopes) = intern_reference env lvar ref in RApp (loc, f, intern_args env args_scopes args) |