diff options
| author | Matthieu Sozeau | 2013-11-25 17:03:04 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:56 +0200 |
| commit | 6f54f7411f6e42298e833215fde9f38dd899e5dc (patch) | |
| tree | 233c01b784eb2404c28747c56637b7e591c95f08 /interp/notation_ops.ml | |
| parent | 1dd78acac418c0f69abb8d9f5d8db13351f01ccc (diff) | |
Fix inversion of notations for projections.
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 4984bfc387..5cad2b54d6 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -669,6 +669,8 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma | GRef (_,r1,_), NRef r2 when (eq_gr r1 r2) -> sigma | GPatVar (_,(_,n1)), NPatVar n2 when Id.equal n1 n2 -> sigma + | GProj (loc,f1,c1), NProj (f2,c2) when Constant.equal f1 f2 -> + match_in u alp metas sigma c1 c2 | GApp (loc,f1,l1), NApp (f2,l2) -> let n1 = List.length l1 and n2 = List.length l2 in let f1,l1,f2,l2 = |