From 0e189432da864d7e31c9d6bb2355f349308a3d0a Mon Sep 17 00:00:00 2001
From: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 7 Sep 2008 00:05:39 +0000
Subject: Better handling of the opacity of proof obligations, add the
 possibility of overriding the default tactic when adding a definition.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11373 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 26ed02379..be7c75663 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -940,7 +940,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let p' = Option.map (intern_type env'') po in
         RIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole (loc, k) -> 
-	RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark true)
+	RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
     | CPatVar (loc, n) when allow_patvar ->
 	RPatVar (loc, n)
     | CPatVar (loc, _) ->
-- 
cgit v1.2.3