diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/glob_term.ml | 5 | ||||
| -rw-r--r-- | pretyping/glob_term.mli | 3 |
2 files changed, 8 insertions, 0 deletions
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index b973a24f74..85dcf291c8 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 diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli index 9649ad2c01..c445bcd243 100644 --- a/pretyping/glob_term.mli +++ b/pretyping/glob_term.mli @@ -97,6 +97,9 @@ and cases_clauses = cases_clause list val cases_predicate_names : tomatch_tuples -> name list +(* Apply one argument to a glob_constr *) +val mkGApp : loc -> glob_constr -> glob_constr -> glob_constr + val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr (* Ensure traversal from left to right *) |