diff options
Diffstat (limited to 'plugins/decl_mode/decl_interp.ml')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 3aa5725295..a29480a554 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -264,7 +264,7 @@ let prod_one_id (loc,id) glob = GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob) let let_in_one_alias (id,pat) glob = - GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob) + GLetIn (Loc.ghost,Name id, glob_of_pat pat, None, glob) let rec bind_primary_aliases map pat = match pat with @@ -359,10 +359,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = let rids=ref ([],pat_vars) in let npatt= deanonymize rids patt in List.rev (fst !rids),npatt in - let term2 = - GLetIn(Loc.ghost,Anonymous, - GCast(Loc.ghost,glob_of_pat npatt, - CastConv app_ind),term1) in + let term2=GLetIn(Loc.ghost,Anonymous,glob_of_pat npatt,Some 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 |