diff options
| author | herbelin | 2011-04-15 22:28:52 +0000 |
|---|---|---|
| committer | herbelin | 2011-04-15 22:28:52 +0000 |
| commit | e2257ae597fd213463dcc7d56e1eb6e6663c0ad3 (patch) | |
| tree | c7d3aff958477c20d732bab4185053af0bb63461 /pretyping | |
| parent | 6717a057b9903b632baadfa1c570645792a9c07b (diff) | |
Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14018 85f007b7-540e-0410-9357-904b9bb8a0f7
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 *) |