diff options
| author | herbelin | 2010-07-22 21:06:06 +0000 |
|---|---|---|
| committer | herbelin | 2010-07-22 21:06:06 +0000 |
| commit | 9b4927d7fdbbafa7ed372e152e7106b3055dfb99 (patch) | |
| tree | c395758164096f2a33ae8d57d2a2895cfa3203b8 /interp/constrextern.ml | |
| parent | 53b06c3069c1234368d14de64ddd9382ff705f3b (diff) | |
Constrintern: unified push_name_env and push_loc_name_env; made
location dumping for binders uniformly treated in constrintern.ml (and
renamed the optional arg of interp_context from fail_anonymous to
global_level since the flag now also decides whether to dump binders as
global or local ones); added locations for the variables occurring in
the "as in" clauses;
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13314 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 28cd12fbde..95a669f751 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -684,10 +684,10 @@ let rec extern inctx scopes vars r = let na' = match na,tm with Anonymous, RVar (_,id) when rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt) - -> Some Anonymous + -> Some (dummy_loc,Anonymous) | Anonymous, _ -> None | Name id, RVar (_,id') when id=id' -> None - | Name _, _ -> Some na in + | Name _, _ -> Some (dummy_loc,na) in (sub_extern false scopes vars tm, (na',Option.map (fun (loc,ind,n,nal) -> let params = list_tabulate @@ -701,15 +701,15 @@ let rec extern inctx scopes vars r = CCases (loc,sty,rtntypopt',tml,eqns) | RLetTuple (loc,nal,(na,typopt),tm,b) -> - CLetTuple (loc,nal, - (Option.map (fun _ -> na) typopt, + CLetTuple (loc,List.map (fun na -> (dummy_loc,na)) nal, + (Option.map (fun _ -> (dummy_loc,na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern inctx scopes (List.fold_left add_vname vars nal) b) | RIf (loc,c,(na,typopt),b1,b2) -> CIf (loc,sub_extern false scopes vars c, - (Option.map (fun _ -> na) typopt, + (Option.map (fun _ -> (dummy_loc,na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2) |