diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-02 11:21:56 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-02 11:21:56 +0000 |
| commit | 60524abd12b7719a5c1f57170770af3c37a78d07 (patch) | |
| tree | 0986f671cc5354ff6ec4f73bc11c85777b272fe0 /parsing | |
| parent | e867509591c1e8fad3fd764da652deb28d293d49 (diff) | |
Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@394 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/astterm.ml | 9 | ||||
| -rw-r--r-- | parsing/termast.ml | 2 |
2 files changed, 6 insertions, 5 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 4e556e877..895de7df1 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -330,7 +330,7 @@ let dbize k allow_soapp sigma = Array.of_list (List.map (dbrec env) cl)) | Node(loc,"ISEVAR",[]) -> RHole (Some loc) - | Node(loc,"META",[Num(_,n)]) -> RRef (loc,RMeta n) + | Node(loc,"META",[Num(_,n)]) -> RMeta (loc, n) | Node(loc,"PROP", []) -> RSort(loc,RProp Null) | Node(loc,"SET", []) -> RSort(loc,RProp Pos) @@ -346,7 +346,7 @@ let dbize k allow_soapp sigma = | Node(loc,"SOAPP", Num(locn,n)::args) when allow_soapp -> (* Hack special pour l'interprétation des constr_pattern *) if n<0 then error "Metavariable numbers must be positive" else - RApp (loc,RRef (locn,RMeta (-n)),List.map (dbrec env) args) + RApp (loc,RMeta (locn,-n),List.map (dbrec env) args) | Node(loc,opn,tl) -> anomaly ("dbize found operator "^opn^" with "^ @@ -576,7 +576,6 @@ let rec pat_of_ref metas vars = function | RInd (ip,ctxt) -> RInd (ip, ctxt) | RConstruct(cp,ctxt) ->RConstruct(cp, ctxt) | REVar (n,ctxt) -> REVar (n, ctxt) - | RMeta n -> metas := n::!metas; RMeta n | RAbst _ -> error "pattern_of_rawconstr: not implemented" | RVar _ -> assert false (* Capturé dans pattern_of_raw *) @@ -584,13 +583,15 @@ and pat_of_raw metas vars = function | RRef (_,RVar id) -> (try PRel (list_index (Name id) vars) with Not_found -> PRef (RVar id)) + | RMeta (_,n) -> + metas := n::!metas; PMeta (Some n) | RRef (_,r) -> PRef (pat_of_ref metas vars r) | RApp (_,c,cl) -> PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) (* Petit hack pour ne pas réécrire une interprétation complète des patterns*) - | RApp (_,RRef (_,RMeta n),cl) when n<0 -> + | RApp (_,RMeta (_,n),cl) when n<0 -> PSoApp (-n, List.map (pat_of_raw metas vars) cl) | RBinder (_,bk,na,c1,c2) -> PBinder (bk, na, pat_of_raw metas vars c1, diff --git a/parsing/termast.ml b/parsing/termast.ml index a044c741c..183c015ea 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -133,7 +133,6 @@ let ast_of_ref = function | RConstruct (cstr,ctxt) -> ast_of_constructor_ref (cstr,ids_of_ctxt ctxt) | RVar id -> ast_of_ident id | REVar (ev,ctxt) -> ast_of_existential_ref (ev,ids_of_ctxt ctxt) - | RMeta n -> ope("META",[num n]) (**********************************************************************) (* conversion of patterns *) @@ -216,6 +215,7 @@ let ast_of_app impl f args = let rec ast_of_raw = function | RRef (_,ref) -> ast_of_ref ref + | RMeta (_,n) -> ope("META",[num n]) | RApp (_,f,args) -> let (f,args) = skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args) in |