diff options
Diffstat (limited to 'pretyping/glob_term.ml')
| -rw-r--r-- | pretyping/glob_term.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index b973a24f7..85dcf291c 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -93,6 +93,11 @@ let cases_predicate_names tml = | (tm,(na,None)) -> [na] | (tm,(na,Some (_,_,_,nal))) -> na::nal) tml) +let mkGApp loc p t = + match p with + | GApp (loc,f,l) -> GApp (loc,f,l@[t]) + | _ -> GApp (loc,p,[t]) + let map_glob_decl_left_to_right f (na,k,obd,ty) = let comp1 = Option.map f obd in let comp2 = f ty in |