diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-15 22:28:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-15 22:28:52 +0000 |
| commit | e2257ae597fd213463dcc7d56e1eb6e6663c0ad3 (patch) | |
| tree | c7d3aff958477c20d732bab4185053af0bb63461 /pretyping/glob_term.ml | |
| 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/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 |