diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-24 23:27:14 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-24 23:27:14 +0200 |
commit | 860dc1cb91549068cf65f963bf819f47eb13ebe4 (patch) | |
tree | 419adf42d07f3bcc2f979eb1f42fa3cd1fd7c585 /engine/proofview.ml | |
parent | 12c78d4e45ccc9b923cd300f981ef205fee1c650 (diff) | |
parent | 8232f27773f3463600fbaac0f70966bd4893ea20 (diff) |
Merge branch 'v8.6'
Diffstat (limited to 'engine/proofview.ml')
-rw-r--r-- | engine/proofview.ml | 38 |
1 files changed, 7 insertions, 31 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index d7fb65126..333ae78b3 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -152,33 +152,9 @@ let focus i j sp = let (new_comb, context) = focus_sublist i j sp.comb in ( { sp with comb = new_comb } , context ) - -(** [advance sigma g] returns [Some g'] if [g'] is undefined and is - the current avatar of [g] (for instance [g] was changed by [clear] - into [g']). It returns [None] if [g] has been (partially) - solved. *) -(* spiwack: [advance] is probably performance critical, and the good - behaviour of its definition may depend sensitively to the actual - definition of [Evd.find]. Currently, [Evd.find] starts looking for - a value in the heap of undefined variable, which is small. Hence in - the most common case, where [advance] is applied to an unsolved - goal ([advance] is used to figure if a side effect has modified the - goal) it terminates quickly. *) -let rec advance sigma g = - let open Evd in - let evi = Evd.find sigma g in - match evi.evar_body with - | Evar_empty -> Some g - | Evar_defined v -> - if Option.default false (Store.get evi.evar_extra Evarutil.cleared) then - let (e,_) = Term.destEvar v in - advance sigma e - else - None - (** [undefined defs l] is the list of goals in [l] which are still unsolved (after advancing cleared goals). *) -let undefined defs l = CList.map_filter (advance defs) l +let undefined defs l = CList.map_filter (Evarutil.advance defs) l (** Unfocuses a proofview with respect to a context. *) let unfocus c sp = @@ -465,7 +441,7 @@ let iter_goal i = Comb.get >>= fun initial -> Proof.List.fold_left begin fun (subgoals as cur) goal -> Solution.get >>= fun step -> - match advance step goal with + match Evarutil.advance step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -489,7 +465,7 @@ let fold_left2_goal i s l = in Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a -> Solution.get >>= fun step -> - match advance step goal with + match Evarutil.advance step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -533,7 +509,7 @@ let tclDISPATCHGEN0 join tacs = let open Proof in Pv.get >>= function | { comb=[goal] ; solution } -> - begin match advance solution goal with + begin match Evarutil.advance solution goal with | None -> tclUNIT (join []) | Some _ -> Proof.map (fun res -> join [res]) tac end @@ -965,7 +941,7 @@ module Unsafe = struct let mark_as_goal evd content = mark_in_evm ~goal:true evd content - let advance = advance + let advance = Evarutil.advance let mark_as_unresolvable p gl = { p with solution = mark_in_evm ~goal:false p.solution gl } @@ -1130,7 +1106,7 @@ module Goal = struct Pv.get >>= fun step -> let sigma = step.solution in let map goal = - match advance sigma goal with + match Evarutil.advance sigma goal with | None -> None (** ppedrot: Is this check really necessary? *) | Some goal -> let gl = @@ -1144,7 +1120,7 @@ module Goal = struct let unsolved { self=self } = tclEVARMAP >>= fun sigma -> - tclUNIT (not (Option.is_empty (advance sigma self))) + tclUNIT (not (Option.is_empty (Evarutil.advance sigma self))) (* compatibility *) let goal { self=self } = self |