From 22e4ceb13d18c8b941f6a27cc83f547dd90104b8 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 14 Oct 1999 13:33:49 +0000
Subject: module Logic

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@105 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'kernel/term.ml')

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