aboutsummaryrefslogtreecommitdiff
path: root/pretyping/patternops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/patternops.ml')
-rw-r--r--pretyping/patternops.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 5828e7f433..54ce29bf71 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -324,8 +324,6 @@ let rec pat_of_raw metas vars = function
(* Hack pour ne pas réécrire une interprétation complète des patterns*)
| GApp (_, GPatVar (_,(true,n)), cl) ->
metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
- | GProj (_, p, c) ->
- PProj (p, pat_of_raw metas vars c)
| GApp (_,c,cl) ->
PApp (pat_of_raw metas vars c,
Array.of_list (List.map (pat_of_raw metas vars) cl))