diff options
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 26 |
1 files changed, 23 insertions, 3 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 04945040..1a1640a4 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*) +(*i $Id: classes.ml 12187 2009-06-13 19:36:59Z msozeau $ i*) (*i*) open Names @@ -264,6 +264,14 @@ let named_of_rel_context l = l ([], []) in ctx +let push_named_context = List.fold_right push_named + +let rec list_filter_map f = function + | [] -> [] + | hd :: tl -> match f hd with + | None -> list_filter_map f tl + | Some x -> x :: list_filter_map f tl + let context ?(hook=fun _ -> ()) l = let env = Global.env() in let evars = ref (Evd.create_evar_defs Evd.empty) in @@ -274,6 +282,14 @@ let context ?(hook=fun _ -> ()) l = let ctx = try named_of_rel_context fullctx with _ -> error "Anonymous variables not allowed in contexts." in + let env = push_named_context ctx env in + let keeps = + List.fold_left (fun acc (id,_,t) -> + match class_of_constr t with + | None -> acc + | Some _ -> List.map pi1 (keep_hyps env (Idset.singleton id)) :: acc) + [] ctx + in List.iter (function (id,_,t) -> if Lib.is_modtype () then let cst = Declare.declare_internal_constant id @@ -285,10 +301,14 @@ let context ?(hook=fun _ -> ()) l = hook (ConstRef cst) | None -> () else ( - let impl = List.exists (fun (x,_) -> match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls + let impl = List.exists (fun (x,_) -> + match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls + and keep = + let l = list_filter_map (fun ids -> if List.mem id ids then Some ids else None) keeps in + List.concat l in Command.declare_one_assumption false (Local (* global *), Definitional) t - [] impl (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id); + [] impl (* implicit *) keep (* always kept *) false (* inline *) (dummy_loc, id); match class_of_constr t with | None -> () | Some tc -> hook (VarRef id))) |