diff options
| author | herbelin | 2007-10-05 11:46:28 +0000 |
|---|---|---|
| committer | herbelin | 2007-10-05 11:46:28 +0000 |
| commit | 20720975c49e5c48f6b03a96df0186b56557eb3e (patch) | |
| tree | 79cfbebb13fadb558e87f903eed42363fc98671d /interp | |
| parent | b37ceca4e2c6e39050ade2acef314dfed24c8e49 (diff) | |
Correction de quelques défauts d'affichage (notations sous "as" pour
filtrage; sauts de line intempestifs dans pretty.ml)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10179 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 32d9f107cf..ec88e6fe85 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -386,7 +386,7 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1 | PatVar (_,Anonymous), AHole _ -> sigma | a, AHole _ -> sigma - | PatCstr (loc,(ind,_ as r1),args1,Anonymous), _ -> + | PatCstr (loc,(ind,_ as r1),args1,_), _ -> let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in let l2 = @@ -441,15 +441,15 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function | (keyrule,pat,n as _rule)::rules -> try (* Check the number of arguments expected by the notation *) - let loc = match t,n with + let loc,na = match t,n with | PatCstr (_,f,l,_), Some n when List.length l > n -> raise No_match - | PatCstr (loc,_,_,_),_ -> loc - | PatVar (loc,_),_ -> loc in + | PatCstr (loc,_,_,na),_ -> loc,na + | PatVar (loc,na),_ -> loc,na in (* Try matching ... *) let subst = match_aconstr_cases_pattern t pat in (* Try availability of interpretation ... *) - match keyrule with + let p = match keyrule with | NotationRule (sc,ntn) -> (match availability_of_notation (sc,ntn) allscopes with (* Uninterpretation is not allowed in current context *) @@ -464,7 +464,8 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function insert_pat_delimiters loc (make_pat_notation loc ntn l) key) | SynDefRule kn -> let qid = shortest_qualid_of_syndef vars kn in - CPatAtom (loc,Some (Qualid (loc, qid))) + CPatAtom (loc,Some (Qualid (loc, qid))) in + insert_pat_alias loc p na with No_match -> extern_symbol_pattern allscopes vars t rules |