diff options
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 0576ec57ba..afb1c94759 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -325,7 +325,7 @@ let rec pat_of_raw metas vars = function metas := n::!metas; PMeta (Some n) | GRef (_,gr,_) -> PRef (canonical_gr gr) - (* Hack pour ne pas réécrire une interprétation complète des patterns*) + (* Hack to avoid rewriting a complete interpretation of patterns *) | GApp (_, GPatVar (_,(true,n)), cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) | GApp (_,c,cl) -> |