diff options
| author | msozeau | 2007-03-19 16:54:25 +0000 |
|---|---|---|
| committer | msozeau | 2007-03-19 16:54:25 +0000 |
| commit | 38ff8d2b59a481ba489400ea194fdd78c6c2d5e1 (patch) | |
| tree | b0c539c86860a372b7356e6245e8db4fa50df16a /tactics | |
| parent | 293675b06262698ba3b1ba30db8595bedd5c55ae (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/decl_interp.ml | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
2 files changed, 3 insertions, 3 deletions
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 -> |