diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 37 |
1 files changed, 19 insertions, 18 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index e304725d46..751b03a4a8 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -20,6 +20,7 @@ open Pp open Libobject open Nameops open Misctypes +open Context.Rel.Declaration (*i*) let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" @@ -196,7 +197,7 @@ let combine_params avoid fn applied needed = List.partition (function (t, Some (loc, ExplByName id)) -> - let is_id (_, (na, _, _)) = match na with + let is_id (_, decl) = match get_name decl with | Name id' -> Id.equal id id' | Anonymous -> false in @@ -209,22 +210,22 @@ let combine_params avoid fn applied needed = (fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false) named in - let is_unset (_, (_, b, _)) = match b with - | None -> true - | Some _ -> false + let is_unset (_, decl) = match decl with + | LocalAssum _ -> true + | LocalDef _ -> false in let needed = List.filter is_unset needed in let rec aux ids avoid app need = match app, need with [], [] -> List.rev ids, avoid - | app, (_, (Name id, _, _)) :: need when Id.List.mem_assoc id named -> + | app, (_, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need when Id.List.mem_assoc id named -> aux (Id.List.assoc id named :: ids) avoid app need - | (x, None) :: app, (None, (Name id, _, _)) :: need -> + | (x, None) :: app, (None, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need -> aux (x :: ids) avoid app need - | _, (Some cl, (_, _, _) as d) :: need -> + | _, (Some cl, _ as d) :: need -> let t', avoid' = fn avoid d in aux (t' :: ids) avoid' app need @@ -239,27 +240,27 @@ let combine_params avoid fn applied needed = in aux [] avoid applied needed let combine_params_freevar = - fun avoid (_, (na, _, _)) -> - let id' = next_name_away_from na avoid in + fun avoid (_, decl) -> + let id' = next_name_away_from (get_name decl) avoid in (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, inst)), l) -> loc, ref, List.map fst l, inst + | CAppExpl (loc, (None, ref, inst), l) -> loc, ref, l, inst + | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst | _ -> 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, inst)), l) -> loc, ref, l, inst + | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst | _ -> raise Not_found let implicit_application env ?(allow_partial=true) f ty = let is_class = try - let (loc, r, _ as clapp) = destClassAppExpl ty in + let (_, r, _, _ as clapp) = destClassAppExpl ty in let (loc, qid) = qualid_of_reference r in let gr = Nametab.locate qid in if Typeclasses.is_class gr then Some (clapp, gr) else None @@ -267,7 +268,7 @@ let implicit_application env ?(allow_partial=true) f ty = in match is_class with | None -> ty, env - | Some ((loc, id, par), gr) -> + | Some ((loc, id, par, inst), gr) -> let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in let c, avoid = let c = class_info gr in @@ -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, None), args), avoid + CAppExpl (loc, (None, id, inst), args), avoid in c, avoid let implicits_of_glob_constr ?(with_products=true) l = |