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.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'pretyping/evd.mli')

diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 3f9eaa5fa7..df362a9bfa 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -63,6 +63,10 @@ val existential_value : evar_map -> existential -> constr
 val existential_type : evar_map -> existential -> types
 val existential_opt_value : evar_map -> existential -> constr option
 
+(*************************)
+(* constr with holes *)
+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