diff options
| author | Guillaume Melquiond | 2016-08-10 11:16:37 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-08-10 11:16:37 +0200 |
| commit | 8d4df809c90352035f7bc92e1f829f2d482625ed (patch) | |
| tree | 76de63eb2cc4767e4205635f201376d5549287c1 /interp/notation_ops.ml | |
| parent | 03bd49e69578665ae33e03300a1277b1c83e1939 (diff) | |
Make it a bit more obvious when variables are of type unit.
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 6478ade61a..f3e0682bd7 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1165,7 +1165,7 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc = let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists) -let rec match_cases_pattern metas (terms,x,termlists,y as sigma) a1 a2 = +let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = match (a1,a2) with | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) | PatVar (_,Anonymous), NHole _ -> sigma,(0,[]) |