From 34bc13e0ef3642244fe77fe8a8a7869fbc8d2fca Mon Sep 17 00:00:00 2001
From: barras
Date: Sun, 12 Sep 2004 11:38:09 +0000
Subject: inclusion de meta_map dans evar_defs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evd.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'pretyping/evd.ml')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index be35cb9475..d7468eded5 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -117,6 +117,9 @@ let existential_opt_value sigma ev =
   try Some (existential_value sigma ev)
   with NotInstantiatedEvar -> None
 
+(*******************************************************************)
+type open_constr = evar_map * constr
+
 (*******************************************************************)
 (* The type constructor ['a sigma] adds an evar map to an object of
   type ['a] *)
-- 
cgit v1.2.3