From 38ff8d2b59a481ba489400ea194fdd78c6c2d5e1 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 19 Mar 2007 16:54:25 +0000
Subject: Add a parameter to QuestionMark evar kind to say it can be turned
 into an obligations (even an opaque one). Change cast_type to include the
 converted-to type or nothing in case of a Coerce cast, required much minor
 changes. Various little subtac changes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/decl_interp.ml | 4 ++--
 tactics/tacinterp.ml   | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index f341580eb1..87a472003f 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -346,7 +346,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	(fun (loc,(id,_)) -> 
 	   RVar (loc,id)) params in 
     let dum_args= 
-      list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark))
+      list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark false))
 	oib.Declarations.mind_nrealargs in
       raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in
   let pat_vars,aliases,patt = interp_pattern env pat in
@@ -369,7 +369,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
   let term2 =
     RLetIn(dummy_loc,Anonymous,
 	   RCast(dummy_loc,raw_of_pat npatt,
-		 CastConv DEFAULTcast,app_ind),term1) in
+		 CastConv (DEFAULTcast,app_ind)),term1) in
   let term3=List.fold_right let_in_one_alias aliases term2 in  
   let term4=List.fold_right prod_one_id loc_ids term3 in
   let term5=List.fold_right prod_one_hyp params term4 in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 971e0986ae..75f517023f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1246,7 +1246,7 @@ open Evd
 
 let solvable_by_tactic env evi (ev,args) src = 
   match (!implicit_tactic, src) with
-  | Some tac, (ImplicitArg _ | QuestionMark)
+  | Some tac, (ImplicitArg _ | QuestionMark _)
       when 
 	Environ.named_context_of_val evi.evar_hyps = 
 	Environ.named_context env ->
-- 
cgit v1.2.3