diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-11 01:25:22 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-11 01:25:22 +0000 |
| commit | 20445e418ffee0c0dc1398c80af4a2b75abe9ac3 (patch) | |
| tree | c019077ca3898406ef9f251b26dba4ec06d24d2d /parsing/termast.ml | |
| parent | d73ae1a52442841ec8c067de7048db977b299a85 (diff) | |
Intégration initiale du Cases
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@234 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/termast.ml')
| -rw-r--r-- | parsing/termast.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/parsing/termast.ml b/parsing/termast.ml index bbc9e368c..cfe85f7fd 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -68,10 +68,14 @@ let ast_of_ref = function let rec ast_of_pattern = function (* loc is thrown away for printing *) | PatVar (loc,Name id) -> nvar (string_of_id id) | PatVar (loc,Anonymous) -> nvar "_" - | PatCstr(loc,cstr,args) -> + | PatCstr(loc,cstr,args,Name id) -> + ope("PATTAS", + [nvar (string_of_id id); + ope("PATTCONSTRUCT", + (ast_of_constructor cstr)::List.map ast_of_pattern args)]) + | PatCstr(loc,cstr,args,Anonymous) -> ope("PATTCONSTRUCT", (ast_of_constructor cstr)::List.map ast_of_pattern args) - | PatAs(loc,id,p) -> ope("PATTAS",[nvar (string_of_id id); ast_of_pattern p]) (* Nouvelle version de renommage des variables (DEC 98) *) (* This is the algorithm to display distinct bound variables @@ -800,7 +804,7 @@ and detype_eqn avoid env constr_id construct_params branch = buildrec new_ids (pat::patlist) new_avoid new_env (l,new_b) | [] , rhs -> - (ids, [PatCstr(dummy_loc, constr_id, List.rev patlist)], + (ids, [PatCstr(dummy_loc, constr_id, List.rev patlist,Anonymous)], detype avoid env rhs) in buildrec [] [] avoid env (construct_params,branch) |