diff options
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/decl_interp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index a25fcd923..2be95056e 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -342,7 +342,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 false)) + list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark (Evd.Define 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 |