diff options
| author | Matthieu Sozeau | 2014-09-17 00:03:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-17 00:10:03 +0200 |
| commit | c5ecebf6fefbaa673dda506175a2aa4a69d79807 (patch) | |
| tree | e364fd928f247c249767ffb679b0265857327a6a /pretyping/glob_ops.ml | |
| parent | 4dc8746cac24ba72a1ec4dfa764a1ae88ce79277 (diff) | |
Revert specific syntax for primitive projections, avoiding ugly
contortions in internalization/externalization. It uses a fully typed
version of detyping, requiring the environment, to move from
primitive projection applications to regular applications of
the eta-expanded version. The kernel is unchanged, and only
constrMatching needs compatibility code now.
Diffstat (limited to 'pretyping/glob_ops.ml')
| -rw-r--r-- | pretyping/glob_ops.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index fb52a0481c..9157cdb815 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -159,9 +159,6 @@ let map_glob_constr_left_to_right f = function let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in let comp3 = Util.List.map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in GCases (loc,sty,comp1,comp2,comp3) - | GProj (loc,p,c) -> - let comp1 = f c in - GProj (loc,p,comp1) | GLetTuple (loc,nal,(na,po),b,c) -> let comp1 = Option.map f po in let comp2 = f b in @@ -189,7 +186,6 @@ let fold_glob_constr f acc = let rec fold acc = function | GVar _ -> acc | GApp (_,c,args) -> List.fold_left fold (fold acc c) args - | GProj (_,p,c) -> fold acc c | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) -> fold (fold acc b) c | GCases (_,_,rtntypopt,tml,pl) -> @@ -228,7 +224,6 @@ let occur_glob_constr id = let rec occur = function | GVar (loc,id') -> Id.equal id id' | GApp (loc,f,args) -> (occur f) || (List.exists occur args) - | GProj (loc,p,c) -> occur c | GLambda (loc,na,bk,ty,c) -> (occur ty) || (not (same_id na id) && (occur c)) | GProd (loc,na,bk,ty,c) -> @@ -278,7 +273,6 @@ let free_glob_vars = let rec vars bounded vs = function | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args) - | GProj (loc,p,c) -> vars bounded vs c | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> let vs' = vars bounded vs ty in let bounded' = add_name_to_ids bounded na in @@ -340,7 +334,6 @@ let loc_of_glob_constr = function | GEvar (loc,_,_) -> loc | GPatVar (loc,_) -> loc | GApp (loc,_,_) -> loc - | GProj (loc,p,c) -> loc | GLambda (loc,_,_,_,_) -> loc | GProd (loc,_,_,_,_) -> loc | GLetIn (loc,_,_,_) -> loc |