diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 2d55a6b63..c69eb629d 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -90,8 +90,8 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = else l in let rec aux bdvars l c = match c with - | CRef (Ident (loc,id)) -> found loc id bdvars l - | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [], [])) when not (Id.Set.mem id bdvars) -> + | CRef (Ident (loc,id),_) -> found loc id bdvars l + | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id),_) :: _, [], [])) when not (Id.Set.mem id bdvars) -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c | c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c @@ -127,6 +127,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp else (id, loc) :: vs else vs | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) + | GProj (loc,p,c) -> vars bound vs c | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> let vs' = vars bound vs ty in let bound' = add_name_to_ids bound na in @@ -241,19 +242,19 @@ let combine_params avoid fn applied needed = let combine_params_freevar = fun avoid (_, (na, _, _)) -> let id' = next_name_away_from na avoid in - (CRef (Ident (Loc.ghost, id')), Id.Set.add id' avoid) + (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid) let destClassApp cl = match cl with - | CApp (loc, (None, CRef ref), l) -> loc, ref, List.map fst l - | CAppExpl (loc, (None, ref), l) -> loc, ref, l - | CRef ref -> loc_of_reference ref, ref, [] + | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, List.map fst l + | CAppExpl (loc, (None, ref,_), l) -> loc, ref, l + | CRef (ref,_) -> loc_of_reference ref, ref, [] | _ -> raise Not_found let destClassAppExpl cl = match cl with - | CApp (loc, (None, CRef ref), l) -> loc, ref, l - | CRef ref -> loc_of_reference ref, ref, [] + | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, l + | CRef (ref,_) -> loc_of_reference ref, ref, [] | _ -> raise Not_found let implicit_application env ?(allow_partial=true) f ty = @@ -285,7 +286,7 @@ let implicit_application env ?(allow_partial=true) f ty = end; let pars = List.rev (List.combine ci rd) in let args, avoid = combine_params avoid f par pars in - CAppExpl (loc, (None, id), args), avoid + CAppExpl (loc, (None, id, None), args), avoid in c, avoid let implicits_of_glob_constr ?(with_products=true) l = |