module Logic

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@105 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 1 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index a1232ab5a9..5d9817fdef 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -353,7 +353,7 @@ let hd_app  = function
 
 (* Destructs a constant *)
 let destConst = function
-  | DOPN (Const  sp, a) -> (sp, a)
+  | DOPN (Const sp, a) -> (sp, a)
   | _ -> invalid_arg "destConst"
 
 let path_of_const = function
@@ -364,6 +364,11 @@ let args_of_const = function
   | DOPN (Const _,args) -> args
   | _ -> anomaly "args_of_const called with bad args"
 
+(* Destructs an existential variable *)
+let destEvar = function
+  | DOPN (Evar n, a) -> (n,a)
+  | _ -> invalid_arg "destEvar"
+
 (* Destructs an abstract term *)
 let destAbst = function
   | DOPN (Abst sp, a) -> (sp, a)