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/notation_ops.ml | |
| 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/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |