diff options
| author | pboutill | 2013-01-07 18:19:55 +0000 |
|---|---|---|
| committer | pboutill | 2013-01-07 18:19:55 +0000 |
| commit | 680a5f0cac29ca68db8b28415a7759794e0e2f9d (patch) | |
| tree | 933a28902e7cfedc8c71e8b94426f29bc5d87d50 /interp | |
| parent | 890dc4c4260e7782c8550a631163796a40e06d99 (diff) | |
Fixup notation printing in patterns
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16117 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 2 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index c91db464d5..e8e76809c6 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -363,7 +363,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args)) let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in let l2' = if !Topconstr.oldfashion_patterns then l2 else - match drop_implicits_in_patt gr (List.length l1) l2 with + match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with |Some true_args -> true_args |None -> raise No_match in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 9dcd24127f..c0e83447f7 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -772,7 +772,7 @@ let rec match_cases_pattern metas sigma a1 a2 = | r1, NVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) | PatVar (_,Anonymous), NHole _ -> sigma,(0,[]) | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> - sigma,(0,largs) + sigma,(0,add_patterns_for_params (fst r1) largs) | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) when eq_constructor r1 r2 -> let l1 = add_patterns_for_params (fst r1) args1 in |