From 0f4f723a5608075ff4aa48290314df30843efbcb Mon Sep 17 00:00:00 2001
From: corbinea
Date: Wed, 20 Sep 2006 17:18:18 +0000
Subject: Declarative Proof Language: main commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/funind/tacinvutils.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'contrib/funind')

diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 2877c19db9..ce775e0bee 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