diff options
| author |  Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
| commit | be2a2fda89bba47d5342b7aebc10efd97f1d68b9 (patch) | |
| tree | 45a70ccd12dc139a53b49daba9c9821ffe2fd035 /tactics/decl_interp.ml | |
| parent | 763b05d3e66a0c0c49bad97434d891d22c1054dc (diff) | |
| parent | 72b9a7df489ea47b3e5470741fd39f6100d31676 (diff) | |
Merge commit 'upstream/8.1.pl1+dfsg'
Diffstat (limited to 'tactics/decl_interp.ml')
| -rw-r--r-- | tactics/decl_interp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index f341580e..87a47200 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 |