From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 contrib/funind/tacinvutils.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'contrib/funind/tacinvutils.ml')

diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 2877c19d..ce775e0b 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -72,10 +72,11 @@ let  rec mkevarmap_from_listex lex =
 		  let _ = prstr ("evar n. " ^ string_of_int ex ^ " ") in
 		  let _ = prstr "OF TYPE: " in
 		  let _ = prconstr typ in*)
-		  let info ={
+		  let info = {
 			 evar_concl = typ;
 			 evar_hyps = empty_named_context_val;
-			 evar_body = Evar_empty} in
+			 evar_body = Evar_empty;
+		         evar_extra = None} in
 		  Evd.add (mkevarmap_from_listex lex') ex info
 
 let mkEq typ c1 c2 = 
-- 
cgit v1.2.3