diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-19 18:20:53 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-19 18:20:53 +0000 |
| commit | b820ff40cb8053df01ac422f36d5f3520727b5c6 (patch) | |
| tree | 56005796146af1aaf2120c2e76afdce49a89b0c0 /parsing | |
| parent | 3b59ca927cba26b3bfbf53f22c3783bfa03b9f32 (diff) | |
Substitution dans REvar et PEvar plutot que encodage via noeud application pour eviter la confusion avec la (vraie) application
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5114 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/termast.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/parsing/termast.ml b/parsing/termast.ml index 3174898c4..0e8b84f74 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -194,7 +194,7 @@ let ast_of_app impl f args = let rec ast_of_raw = function | RRef (_,ref) -> ast_of_ref ref | RVar (_,id) -> ast_of_ident id - | REvar (_,n) -> ast_of_existential_ref n + | REvar (_,n,_) -> (* we drop args *) ast_of_existential_ref n | RPatVar (_,(_,n)) -> ope("META",[ast_of_ident n]) | RApp (_,f,args) -> let (f,args) = @@ -202,7 +202,6 @@ let rec ast_of_raw = function let astf = ast_of_raw f in let astargs = List.map ast_of_raw args in (match f with - | REvar (_,ev) -> ast_of_existential_ref ev (* we drop args *) | RRef (_,ref) -> ast_of_app (implicits_of_global ref) astf astargs | _ -> ast_of_app [] astf astargs) @@ -368,7 +367,7 @@ let rec ast_of_pattern tenv env = function | PVar id -> ast_of_ident id - | PEvar n -> ast_of_existential_ref n + | PEvar (n,_) -> ast_of_existential_ref n | PRel n -> (try match lookup_name_of_rel n env with |