diff options
| author | herbelin | 2003-09-09 15:06:44 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-09 15:06:44 +0000 |
| commit | a580a7a07da8651887c6fb386bd9af55bbe673a2 (patch) | |
| tree | 4233682720571f3fa09fba77bb31e446dc6203e1 /pretyping/pattern.ml | |
| parent | 51cd60453da3f1fe136904404046098d9c4f1cc3 (diff) | |
Ajout construction If primitive dans constr_expr et rawconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4336 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pattern.ml')
| -rw-r--r-- | pretyping/pattern.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index d3479a8466..f453e911e4 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -241,6 +241,9 @@ let rec pat_of_raw metas vars = function PCase ((None,st),option_app (pat_of_raw metas vars) po, pat_of_raw metas vars c, Array.map (pat_of_raw metas vars) br) + | RIf (_,c,(_,None),b1,b2) -> + PCase ((None,IfStyle),None, pat_of_raw metas vars c, + [|pat_of_raw metas vars b1; pat_of_raw metas vars b2|]) | RCases (loc,(po,_),[c,_],brs) -> let sp = match brs with |