From e2257ae597fd213463dcc7d56e1eb6e6663c0ad3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 15 Apr 2011 22:28:52 +0000
Subject: 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
---
 pretyping/glob_term.ml  | 5 +++++
 pretyping/glob_term.mli | 3 +++
 2 files changed, 8 insertions(+)

(limited to 'pretyping')

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 *)
-- 
cgit v1.2.3