diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 10 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 6 | ||||
| -rw-r--r-- | proofs/logic.ml | 6 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 62 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 9 | ||||
| -rw-r--r-- | proofs/proof.ml | 97 | ||||
| -rw-r--r-- | proofs/proof.mli | 63 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 106 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 5 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 1 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 278 | ||||
| -rw-r--r-- | proofs/redexpr.mli | 48 | ||||
| -rw-r--r-- | proofs/refine.ml | 32 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 14 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 4 |
15 files changed, 255 insertions, 486 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index b7ccd647b5..1f1bdf4da7 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -601,17 +601,17 @@ let make_evar_clause env sigma ?len t = | None -> -1 | Some n -> assert (0 <= n); n in - (** FIXME: do the renaming online *) + (* FIXME: do the renaming online *) let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in let rec clrec (sigma, holes) inst n t = if n = 0 then (sigma, holes, t) else match EConstr.kind sigma t with | Cast (t, _, _) -> clrec (sigma, holes) inst n t | Prod (na, t1, t2) -> - (** Share the evar instances as we are living in the same context *) + (* Share the evar instances as we are living in the same context *) let inst, ctx, args, subst = match inst with | None -> - (** Dummy type *) + (* Dummy type *) let ctx, _, args, subst = push_rel_context_to_named_context env sigma mkProp in Some (ctx, args, subst), ctx, args, subst | Some (ctx, args, subst) -> inst, ctx, args, subst @@ -688,7 +688,7 @@ let solve_evar_clause env sigma hyp_only clause = function let open EConstr in let fold holes h = if h.hole_deps then - (** Some subsequent term uses the hole *) + (* Some subsequent term uses the hole *) let (ev, _) = destEvar sigma h.hole_evar in let is_dep hole = occur_evar sigma ev hole.hole_type in let in_hyp = List.exists is_dep holes in @@ -697,7 +697,7 @@ let solve_evar_clause env sigma hyp_only clause = function let h = { h with hole_deps = dep } in h :: holes else - (** The hole does not occur anywhere *) + (* The hole does not occur anywhere *) h :: holes in let holes = List.fold_left fold [] (List.rev clause.cl_holes) in diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 4720328893..c36b0fa337 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -61,9 +61,9 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv = clenv_pose_metas_as_evars clenv dep_mvs let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = - (** ppedrot: a Goal.enter here breaks things, because the tactic below may - solve goals by side effects, while the compatibility layer keeps those - useless goals. That deserves a FIXME. *) + (* ppedrot: a Goal.enter here breaks things, because the tactic below may + solve goals by side effects, while the compatibility layer keeps those + useless goals. That deserves a FIXME. *) Proofview.V82.tactic begin fun gl -> let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in let evd' = diff --git a/proofs/logic.ml b/proofs/logic.ml index 15ba0a704f..3581e90b79 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -63,7 +63,7 @@ let catchable_exception = function | CErrors.UserError _ | TypeError _ | Proof.OpenProof _ (* abstract will call close_proof inside a tactic *) - | Notation.NumeralNotationError _ + | Notation.PrimTokenNotationError _ | RefinerError _ | Indrec.RecursionSchemeError _ | Nametab.GlobalizationError _ (* reduction errors *) @@ -373,8 +373,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm = check_typability env sigma ty; let sigma = check_conv_leq_goal env sigma trm ty conclty in let res = mk_refgoals sigma goal goalacc ty t in - (** we keep the casts (in particular VMcast and NATIVEcast) except - when they are annotating metas *) + (* we keep the casts (in particular VMcast and NATIVEcast) except + when they are annotating metas *) if isMeta t then begin assert (k != VMcast && k != NATIVEcast); res diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 886a62cb89..7f1ae6d12b 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -33,7 +33,7 @@ let () = CErrors.register_handler begin function end let get_nth_V82_goal p i = - let goals,_,_,_,sigma = Proof.proof p in + let Proof.{ sigma; goals } = Proof.data p in try { it = List.nth goals (i-1) ; sigma } with Failure _ -> raise NoSuchGoal @@ -107,11 +107,14 @@ let solve ?with_end_tac gi info_lvl tac pr = Proofview.tclTHEN tac Refine.solve_constraints else tac in - let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in + let env = Global.env () in + let (p,(status,info)) = Proof.run_tactic env tac pr in + let env = Global.env () in + let sigma = Evd.from_env env in let () = match info_lvl with | None -> () - | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info)) + | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info)) in (p,status) with @@ -120,7 +123,8 @@ let solve ?with_end_tac gi info_lvl tac pr = let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) let instantiate_nth_evar_com n com = - Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p) + Proof_global.simple_with_current_proof (fun _ p -> + Proof.V82.instantiate_evar Global.(env ())n com p) (**********************************************************************) @@ -166,51 +170,51 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in cb, status, univs -let refine_by_tactic env sigma ty tac = - (** Save the initial side-effects to restore them afterwards. We set the - current set of side-effects to be empty so that we can retrieve the - ones created during the tactic invocation easily. *) +let refine_by_tactic ~name ~poly env sigma ty tac = + (* Save the initial side-effects to restore them afterwards. We set the + current set of side-effects to be empty so that we can retrieve the + ones created during the tactic invocation easily. *) let eff = Evd.eval_side_effects sigma in let sigma = Evd.drop_side_effects sigma in - (** Save the existing goals *) + (* Save the existing goals *) let prev_future_goals = save_future_goals sigma in - (** Start a proof *) - let prf = Proof.start sigma [env, ty] in + (* Start a proof *) + let prf = Proof.start ~name ~poly sigma [env, ty] in let (prf, _) = try Proof.run_tactic env tac prf with Logic_monad.TacticFailure e as src -> - (** Catch the inner error of the monad tactic *) + (* Catch the inner error of the monad tactic *) let (_, info) = CErrors.push src in iraise (e, info) in - (** Plug back the retrieved sigma *) - let (goals,stack,shelf,given_up,sigma) = Proof.proof prf in + (* Plug back the retrieved sigma *) + let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in assert (stack = []); - let ans = match Proof.initial_goals prf with + let ans = match Proofview.initial_goals entry with | [c, _] -> c | _ -> assert false in let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in - (** [neff] contains the freshly generated side-effects *) + (* [neff] contains the freshly generated side-effects *) let neff = Evd.eval_side_effects sigma in - (** Reset the old side-effects *) + (* Reset the old side-effects *) let sigma = Evd.drop_side_effects sigma in let sigma = Evd.emit_side_effects eff sigma in - (** Restore former goals *) + (* Restore former goals *) let sigma = restore_future_goals sigma prev_future_goals in - (** Push remaining goals as future_goals which is the only way we - have to inform the caller that there are goals to collect while - not being encapsulated in the monad *) - (** Goals produced by tactic "shelve" *) + (* Push remaining goals as future_goals which is the only way we + have to inform the caller that there are goals to collect while + not being encapsulated in the monad *) + (* Goals produced by tactic "shelve" *) let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in - (** Goals produced by tactic "give_up" *) + (* Goals produced by tactic "give_up" *) let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in - (** Other goals *) + (* Other goals *) let sigma = List.fold_right Evd.declare_future_goal goals sigma in - (** Get rid of the fresh side-effects by internalizing them in the term - itself. Note that this is unsound, because the tactic may have solved - other goals that were already present during its invocation, so that - those goals rely on effects that are not present anymore. Hopefully, - this hack will work in most cases. *) + (* Get rid of the fresh side-effects by internalizing them in the term + itself. Note that this is unsound, because the tactic may have solved + other goals that were already present during its invocation, so that + those goals rely on effects that are not present anymore. Hopefully, + this hack will work in most cases. *) let ans = Safe_typing.inline_private_constants_in_constr env ans neff in ans, sigma diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 155221947a..5699320af5 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -81,8 +81,13 @@ val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic -> EConstr.types -> unit Proofview.tactic -> constr * bool * UState.t -val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic -> - constr * Evd.evar_map +val refine_by_tactic + : name:Id.t + -> poly:bool + -> env -> Evd.evar_map + -> EConstr.types + -> unit Proofview.tactic + -> constr * Evd.evar_map (** A variant of the above function that handles open terms as well. Caveat: all effects are purged in the returned term at the end, but other evars solved by side-effects are NOT purged, so that unexpected failures may diff --git a/proofs/proof.ml b/proofs/proof.ml index 6c13c4946a..1aeb24606b 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -105,22 +105,29 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k) (* Subpart of the type of proofs. It contains the parts of the proof which are under control of the undo mechanism *) -type t = { - (* Current focused proofview *) - proofview: Proofview.proofview; - (* Entry for the proofview *) - entry : Proofview.entry; - (* History of the focusings, provides information on how - to unfocus the proof and the extra information stored while focusing. - The list is empty when the proof is fully unfocused. *) - focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list; - (* List of goals that have been shelved. *) - shelf : Goal.goal list; - (* List of goals that have been given up *) - given_up : Goal.goal list; - (* The initial universe context (for the statement) *) - initial_euctx : UState.t -} +type t = + { proofview: Proofview.proofview + (** Current focused proofview *) + ; entry : Proofview.entry + (** Entry for the proofview *) + ; focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list + (** History of the focusings, provides information on how to unfocus + the proof and the extra information stored while focusing. The + list is empty when the proof is fully unfocused. *) + ; shelf : Goal.goal list + (** List of goals that have been shelved. *) + ; given_up : Goal.goal list + (** List of goals that have been given up *) + ; initial_euctx : UState.t + (** The initial universe context (for the statement) *) + ; name : Names.Id.t + (** the name of the theorem whose proof is being constructed *) + ; poly : bool + (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *) + } + +let initial_goals pf = Proofview.initial_goals pf.entry +let initial_euctx pf = pf.initial_euctx (*** General proof functions ***) @@ -141,7 +148,7 @@ let proof p = (goals,stack,shelf,given_up,sigma) type 'a pre_goals = { - fg_goals : 'a list; + fg_goals : 'a list; (** List of the focussed goals *) bg_goals : ('a list * 'a list) list; (** Zipper representing the unfocussed background goals *) @@ -311,7 +318,7 @@ let end_of_stack = CondEndStack end_of_stack_kind let unfocused = is_last_focus end_of_stack_kind -let start sigma goals = +let start ~name ~poly sigma goals = let entry, proofview = Proofview.init sigma goals in let pr = { proofview; @@ -320,9 +327,13 @@ let start sigma goals = shelf = [] ; given_up = []; initial_euctx = - Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in + Evd.evar_universe_context (snd (Proofview.proofview proofview)) + ; name + ; poly + } in _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr -let dependent_start goals = + +let dependent_start ~name ~poly goals = let entry, proofview = Proofview.dependent_init goals in let pr = { proofview; @@ -331,7 +342,10 @@ let dependent_start goals = shelf = [] ; given_up = []; initial_euctx = - Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in + Evd.evar_universe_context (snd (Proofview.proofview proofview)) + ; name + ; poly + } in let number_of_goals = List.length (Proofview.initial_goals pr.entry) in _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr @@ -375,9 +389,6 @@ let return ?pid (p : t) = let p = unfocus end_of_stack_kind p () in Proofview.return p.proofview -let initial_goals p = Proofview.initial_goals p.entry -let initial_euctx p = p.initial_euctx - let compact p = let entry, proofview = Proofview.compact p.entry p.proofview in { p with proofview; entry } @@ -468,7 +479,7 @@ module V82 = struct { p with proofview = Proofview.V82.grab p.proofview } (* Main component of vernac command Existential *) - let instantiate_evar n com pr = + let instantiate_evar env n com pr = let tac = Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma -> let (evk, evi) = @@ -487,7 +498,7 @@ module V82 = struct let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in Proofview.Unsafe.tclEVARS sigma end in - let ((), proofview, _, _) = Proofview.apply (Global.env ()) tac pr.proofview in + let ((), proofview, _, _) = Proofview.apply env tac pr.proofview in let shelf = List.filter begin fun g -> Evd.is_undefined (Proofview.return proofview) g @@ -507,3 +518,37 @@ let all_goals p = let set = add given_up set in let { Evd.it = bgoals ; sigma = bsigma } = V82.background_subgoals p in add bgoals set + +type data = + { sigma : Evd.evar_map + (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *) + ; goals : Evar.t list + (** Focused goals *) + ; entry : Proofview.entry + (** Entry for the proofview *) + ; stack : (Evar.t list * Evar.t list) list + (** A representation of the focus stack *) + ; shelf : Evar.t list + (** A representation of the shelf *) + ; given_up : Evar.t list + (** A representation of the given up goals *) + ; initial_euctx : UState.t + (** The initial universe context (for the statement) *) + ; name : Names.Id.t + (** The name of the theorem whose proof is being constructed *) + ; poly : bool + (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *) + } + +let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name; poly } = + let goals, sigma = Proofview.proofview proofview in + (* spiwack: beware, the bottom of the stack is used by [Proof] + internally, and should not be exposed. *) + let rec map_minus_one f = function + | [] -> assert false + | [_] -> [] + | a::l -> f a :: (map_minus_one f l) + in + let stack = + map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in + { sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly } diff --git a/proofs/proof.mli b/proofs/proof.mli index aaabea3454..fd5e905a3b 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -50,27 +50,70 @@ val proof : t -> * Goal.goal list * Goal.goal list * Evd.evar_map +[@@ocaml.deprecated "use [Proof.data]"] + +val initial_goals : t -> (EConstr.constr * EConstr.types) list +[@@ocaml.deprecated "use [Proof.data]"] + +val initial_euctx : t -> UState.t +[@@ocaml.deprecated "use [Proof.data]"] + +type data = + { sigma : Evd.evar_map + (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *) + ; goals : Evar.t list + (** Focused goals *) + ; entry : Proofview.entry + (** Entry for the proofview *) + ; stack : (Evar.t list * Evar.t list) list + (** A representation of the focus stack *) + ; shelf : Evar.t list + (** A representation of the shelf *) + ; given_up : Evar.t list + (** A representation of the given up goals *) + ; initial_euctx : UState.t + (** The initial universe context (for the statement) *) + ; name : Names.Id.t + (** The name of the theorem whose proof is being constructed *) + ; poly : bool; + (** polymorphism *) + } + +val data : t -> data (* Generic records structured like the return type of proof *) type 'a pre_goals = { fg_goals : 'a list; + [@ocaml.deprecated "use [Proof.data]"] (** List of the focussed goals *) bg_goals : ('a list * 'a list) list; + [@ocaml.deprecated "use [Proof.data]"] (** Zipper representing the unfocussed background goals *) shelved_goals : 'a list; + [@ocaml.deprecated "use [Proof.data]"] (** List of the goals on the shelf. *) given_up_goals : 'a list; + [@ocaml.deprecated "use [Proof.data]"] (** List of the goals that have been given up *) } +[@@ocaml.deprecated "use [Proof.data]"] -val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) - +(* needed in OCaml 4.05.0, not needed in newer ones *) +[@@@ocaml.warning "-3"] +val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) [@ocaml.warning "-3"] +[@@ocaml.deprecated "use [Proof.data]"] +[@@@ocaml.warning "+3"] (*** General proof functions ***) -val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> t -val dependent_start : Proofview.telescope -> t -val initial_goals : t -> (EConstr.constr * EConstr.types) list -val initial_euctx : t -> UState.t +val start + : name:Names.Id.t + -> poly:bool + -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t + +val dependent_start + : name:Names.Id.t + -> poly:bool + -> Proofview.telescope -> t (* Returns [true] if the considered proof is completed, that is if no goal remain to be considered (this does not require that all evars have been solved). *) @@ -177,8 +220,9 @@ val no_focused_goal : t -> bool (* the returned boolean signal whether an unsafe tactic has been used. In which case it is [false]. *) -val run_tactic : Environ.env -> - unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) +val run_tactic + : Environ.env + -> unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) val maximal_unfocus : 'a focus_kind -> t -> t @@ -208,7 +252,8 @@ module V82 : sig val grab_evars : t -> t (* Implements the Existential command *) - val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t + val instantiate_evar : + Environ.env -> int -> Constrexpr.constr_expr -> t -> t end (* returns the set of all goals in the proof *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 67e19df0e7..f8adc58921 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -53,11 +53,12 @@ let default_proof_mode = ref (find_proof_mode "No") let get_default_proof_mode_name () = (CEphemeron.default !default_proof_mode standard).name +let proof_mode_opt_name = ["Default";"Proof";"Mode"] let () = Goptions.(declare_string_option { optdepr = false; optname = "default proof mode" ; - optkey = ["Default";"Proof";"Mode"] ; + optkey = proof_mode_opt_name ; optread = begin fun () -> (CEphemeron.default !default_proof_mode standard).name end; @@ -90,14 +91,13 @@ type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator type pstate = { - pid : Id.t; (* the name of the theorem whose proof is being constructed *) terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; section_vars : Constr.named_context option; proof : Proof.t; - strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; universe_decl: UState.universe_decl; + strength : Decl_kinds.goal_kind; } type t = pstate list @@ -142,7 +142,7 @@ end (*** Proof Global manipulation ***) let get_all_proof_names () = - List.map (function { pid = id } -> id) !pstates + List.map Proof.(function pf -> (data pf.proof).name) !pstates let cur_pstate () = match !pstates with @@ -151,7 +151,7 @@ let cur_pstate () = let give_me_the_proof () = (cur_pstate ()).proof let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None -let get_current_proof_name () = (cur_pstate ()).pid +let get_current_proof_name () = (Proof.data (cur_pstate ()).proof).Proof.name let with_current_proof f = match !pstates with @@ -205,8 +205,12 @@ let check_no_pending_proof () = str"Use \"Abort All\" first or complete proof(s).") end +let pf_name_eq id ps = + let Proof.{ name } = Proof.data ps.proof in + Id.equal name id + let discard_gen id = - pstates := List.filter (fun { pid = id' } -> not (Id.equal id id')) !pstates + pstates := List.filter (fun pf -> not (pf_name_eq id pf)) !pstates let discard {CAst.loc;v=id} = let n = List.length !pstates in @@ -223,9 +227,9 @@ let discard_all () = pstates := [] (* [set_proof_mode] sets the proof mode to be used after it's called. It is typically called by the Proof Mode command. *) let set_proof_mode m id = - pstates := - List.map (function { pid = id' } as p -> - if Id.equal id' id then { p with mode = m } else p) !pstates; + pstates := List.map + (fun ps -> if pf_name_eq id ps then { ps with mode = m } else ps) + !pstates; update_proof_mode () let set_proof_mode mn = @@ -244,28 +248,26 @@ let disactivate_current_proof_mode () = end of the proof to close the proof. The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -let start_proof sigma id ?(pl=UState.default_univ_decl) str goals terminator = +let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator = let initial_state = { - pid = id; terminator = CEphemeron.create terminator; - proof = Proof.start sigma goals; + proof = Proof.start ~name ~poly:(pi2 kind) sigma goals; endline_tactic = None; section_vars = None; - strength = str; mode = find_proof_mode "No"; - universe_decl = pl } in + universe_decl = pl; + strength = kind } in push initial_state pstates -let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator = +let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator = let initial_state = { - pid = id; terminator = CEphemeron.create terminator; - proof = Proof.dependent_start goals; + proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals; endline_tactic = None; section_vars = None; - strength = str; mode = find_proof_mode "No"; - universe_decl = pl } in + universe_decl = pl; + strength = kind } in push initial_state pstates let get_used_variables () = (cur_pstate ()).section_vars @@ -301,10 +303,10 @@ let set_used_variables l = ctx, [] let get_open_goals () = - let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in - List.length gl + + let Proof.{ goals; stack; shelf } = Proof.data (cur_pstate ()).proof in + List.length goals + List.fold_left (+) 0 - (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + + (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + List.length shelf type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t @@ -323,12 +325,9 @@ let private_poly_univs = let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now (fpl : closed_proof_output Future.computation) = - let { pid; section_vars; strength; proof; terminator; universe_decl } = - cur_pstate () in + let { section_vars; proof; terminator; universe_decl; strength } = cur_pstate () in + let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in let opaque = match opaque with Opaque -> true | Transparent -> false in - let poly = pi2 strength (* Polymorphic *) in - let initial_goals = Proof.initial_goals proof in - let initial_euctx = Proof.initial_euctx proof in let constrain_variables ctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx in @@ -341,6 +340,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now Proof.in_proof proof (fun m -> Evd.existential_opt_value0 m k) in let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst universes) in + let make_body = if poly || now then let make_body t (c, eff) = @@ -388,14 +388,21 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now fun t p -> (* Already checked the univ_decl for the type universes when starting the proof. *) let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in - Future.from_val (univctx, nf t), + let t = nf t in + Future.from_val (univctx, t), Future.chain p (fun (pt,eff) -> (* Deferred proof, we already checked the universe declaration with the initial universes, ensure that the final universes respect the declaration as well. If the declaration is non-extensible, this will prevent the body from adding universes and constraints. *) - let bodyunivs = constrain_variables (Future.force univs) in - let univs = UState.check_mono_univ_decl bodyunivs universe_decl in + let univs = Future.force univs in + let univs = constrain_variables univs in + let used_univs = Univ.LSet.union + (Vars.universes_of_constr t) + (Vars.universes_of_constr pt) + in + let univs = UState.restrict univs used_univs in + let univs = UState.check_mono_univ_decl univs universe_decl in (pt,univs),eff) in let entry_fn p (_, t) = @@ -411,30 +418,31 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now const_entry_opaque = opaque; const_entry_universes = univs; } in - let entries = Future.map2 entry_fn fpl initial_goals in - { id = pid; entries = entries; persistence = strength; + let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in + { id = name; entries = entries; persistence = strength; universes }, fun pr_ending -> CEphemeron.get terminator pr_ending let return_proof ?(allow_partial=false) () = - let { pid; proof; strength = (_,poly,_) } = cur_pstate () in + let { proof } = cur_pstate () in if allow_partial then begin let proofs = Proof.partial_proof proof in - let _,_,_,_, evd = Proof.proof proof in + let Proof.{sigma=evd} = Proof.data proof in let eff = Evd.eval_side_effects evd in - (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate - side-effects... This may explain why one need to uniquize side-effects - thereafter... *) + (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate + side-effects... This may explain why one need to uniquize side-effects + thereafter... *) let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in proofs, Evd.evar_universe_context evd end else - let initial_goals = Proof.initial_goals proof in + let Proof.{name=pid;entry} = Proof.data proof in + let initial_goals = Proofview.initial_goals entry in let evd = Proof.return ~pid proof in let eff = Evd.eval_side_effects evd in let evd = Evd.minimize_universes evd in - (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate - side-effects... This may explain why one need to uniquize side-effects - thereafter... *) + (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate + side-effects... This may explain why one need to uniquize side-effects + thereafter... *) let proofs = List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in proofs, Evd.evar_universe_context evd @@ -455,25 +463,23 @@ let set_terminator hook = module V82 = struct let get_current_initial_conclusions () = - let { pid; strength; proof } = cur_pstate () in - let initial = Proof.initial_goals proof in + let { proof; strength } = cur_pstate () in + let Proof.{ name; entry } = Proof.data proof in + let initial = Proofview.initial_goals entry in let goals = List.map (fun (o, c) -> c) initial in - pid, (goals, strength) + name, (goals, strength) end let freeze ~marshallable = - match marshallable with - | `Yes -> - CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") - | `Shallow -> !pstates - | `No -> !pstates + if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") + else !pstates let unfreeze s = pstates := s; update_proof_mode () let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof let copy_terminators ~src ~tgt = assert(List.length src = List.length tgt); List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt -let update_global_env () = +let update_global_env pf_info = with_current_proof (fun _ p -> Proof.in_proof p (fun sigma -> let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index d9c32cf9d5..e762f3b7dc 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -135,7 +135,7 @@ module V82 : sig Decl_kinds.goal_kind) end -val freeze : marshallable:[`Yes | `No | `Shallow] -> t +val freeze : marshallable:bool -> t val unfreeze : t -> unit val proof_of_state : t -> Proof.t val copy_terminators : src:t -> tgt:t -> t @@ -168,6 +168,8 @@ val register_proof_mode : proof_mode -> unit (* Can't make this deprecated due to limitations of camlp5 *) (* [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] *) +val proof_mode_opt_name : string list + val get_default_proof_mode_name : unit -> proof_mode_name [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] @@ -181,4 +183,3 @@ val activate_proof_mode : proof_mode_name -> unit val disactivate_current_proof_mode : unit -> unit [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] - diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index dbd5be23ab..0ce726db25 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -7,7 +7,6 @@ Logic Goal_select Proof_bullet Proof_global -Redexpr Refiner Tacmach Pfedit diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml deleted file mode 100644 index 6658c37f41..0000000000 --- a/proofs/redexpr.ml +++ /dev/null @@ -1,278 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open CErrors -open Util -open Names -open Constr -open EConstr -open Declarations -open Genredexpr -open Pattern -open Reductionops -open Tacred -open CClosure -open RedFlags -open Libobject - -(* call by value normalisation function using the virtual machine *) -let cbv_vm env sigma c = - if Coq_config.bytecode_compiler then - let ctyp = Retyping.get_type_of env sigma c in - Vnorm.cbv_vm env sigma c ctyp - else - compute env sigma c - -let warn_native_compute_disabled = - CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler" - (fun () -> - strbrk "native_compute disabled at configure time; falling back to vm_compute.") - -let cbv_native env sigma c = - if Coq_config.native_compiler then - let ctyp = Retyping.get_type_of env sigma c in - Nativenorm.native_norm env sigma c ctyp - else - (warn_native_compute_disabled (); - cbv_vm env sigma c) - -let whd_cbn flags env sigma t = - let (state,_) = - (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty)) - in - Reductionops.Stack.zip ~refold:true sigma state - -let strong_cbn flags = - strong_with_flags whd_cbn flags - -let simplIsCbn = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optname = - "Plug the simpl tactic to the new cbn mechanism"; - optkey = ["SimplIsCbn"]; - optread = (fun () -> !simplIsCbn); - optwrite = (fun a -> simplIsCbn:=a); -}) - -let set_strategy_one ref l = - let k = - match ref with - | EvalConstRef sp -> ConstKey sp - | EvalVarRef id -> VarKey id in - Global.set_strategy k l; - match k,l with - ConstKey sp, Conv_oracle.Opaque -> - Csymtable.set_opaque_const sp - | ConstKey sp, _ -> - let cb = Global.lookup_constant sp in - (match cb.const_body with - | OpaqueDef _ -> - user_err ~hdr:"set_transparent_const" - (str "Cannot make" ++ spc () ++ - Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++ - spc () ++ str "transparent because it was declared opaque."); - | _ -> Csymtable.set_transparent_const sp) - | _ -> () - -let cache_strategy (_,str) = - List.iter - (fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql) - str - -let subst_strategy (subs,(local,obj)) = - local, - List.Smart.map - (fun (k,ql as entry) -> - let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in - if ql==ql' then entry else (k,ql')) - obj - - -let map_strategy f l = - let l' = List.fold_right - (fun (lev,ql) str -> - let ql' = List.fold_right - (fun q ql -> - match f q with - Some q' -> q' :: ql - | None -> ql) ql [] in - if List.is_empty ql' then str else (lev,ql')::str) l [] in - if List.is_empty l' then None else Some (false,l') - -let classify_strategy (local,_ as obj) = - if local then Dispose else Substitute obj - -let disch_ref ref = - match ref with - EvalConstRef c -> Some ref - | EvalVarRef id -> if Lib.is_in_section (GlobRef.VarRef id) then None else Some ref - -let discharge_strategy (_,(local,obj)) = - if local then None else - map_strategy disch_ref obj - -type strategy_obj = - bool * (Conv_oracle.level * evaluable_global_reference list) list - -let inStrategy : strategy_obj -> obj = - declare_object {(default_object "STRATEGY") with - cache_function = (fun (_,obj) -> cache_strategy obj); - load_function = (fun _ (_,obj) -> cache_strategy obj); - subst_function = subst_strategy; - discharge_function = discharge_strategy; - classify_function = classify_strategy } - - -let set_strategy local str = - Lib.add_anonymous_leaf (inStrategy (local,str)) - -(* Generic reduction: reduction functions used in reduction tactics *) - -type red_expr = - (constr, evaluable_global_reference, constr_pattern) red_expr_gen - -let make_flag_constant = function - | EvalVarRef id -> fVAR id - | EvalConstRef sp -> fCONST sp - -let make_flag env f = - let red = no_red in - let red = if f.rBeta then red_add red fBETA else red in - let red = if f.rMatch then red_add red fMATCH else red in - let red = if f.rFix then red_add red fFIX else red in - let red = if f.rCofix then red_add red fCOFIX else red in - let red = if f.rZeta then red_add red fZETA else red in - let red = - if f.rDelta then (* All but rConst *) - let red = red_add red fDELTA in - let red = red_add_transparent red - (Conv_oracle.get_transp_state (Environ.oracle env)) in - List.fold_right - (fun v red -> red_sub red (make_flag_constant v)) - f.rConst red - else (* Only rConst *) - let red = red_add_transparent (red_add red fDELTA) TransparentState.empty in - List.fold_right - (fun v red -> red_add red (make_flag_constant v)) - f.rConst red - in red - -(* table of custom reductino fonctions, not synchronized, - filled via ML calls to [declare_reduction] *) -let reduction_tab = ref String.Map.empty - -(* table of custom reduction expressions, synchronized, - filled by command Declare Reduction *) -let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction" - -let declare_reduction s f = - if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then user_err ~hdr:"Redexpr.declare_reduction" - (str "There is already a reduction expression of name " ++ str s) - else reduction_tab := String.Map.add s f !reduction_tab - -let check_custom = function - | ExtraRedExpr s -> - if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab) - then user_err ~hdr:"Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s) - |_ -> () - -let decl_red_expr s e = - if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then user_err ~hdr:"Redexpr.decl_red_expr" - (str "There is already a reduction expression of name " ++ str s) - else begin - check_custom e; - red_expr_tab := String.Map.add s e !red_expr_tab - end - -let out_arg = function - | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.") - | Locus.ArgArg x -> x - -let out_with_occurrences (occs,c) = - (Locusops.occurrences_map (List.map out_arg) occs, c) - -let e_red f env evm c = evm, f env evm c - -let head_style = false (* Turn to true to have a semantics where simpl - only reduce at the head when an evaluable reference is given, e.g. - 2+n would just reduce to S(1+n) instead of S(S(n)) *) - -let contextualize f g = function - | Some (occs,c) -> - let l = Locusops.occurrences_map (List.map out_arg) occs in - let b,c,h = match c with - | Inl r -> true,PRef (global_of_evaluable_reference r),f - | Inr c -> false,c,f in - e_red (contextually b (l,c) (fun _ -> h)) - | None -> e_red g - -let warn_simpl_unfolding_modifiers = - CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:"tactics" - (fun () -> - Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.") - -let reduction_of_red_expr env = - let make_flag = make_flag env in - let rec reduction_of_red_expr = function - | Red internal -> - if internal then (e_red try_red_product,DEFAULTcast) - else (e_red red_product,DEFAULTcast) - | Hnf -> (e_red hnf_constr,DEFAULTcast) - | Simpl (f,o) -> - let whd_am = if !simplIsCbn then whd_cbn (make_flag f) else whd_simpl in - let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in - let () = - if not (!simplIsCbn || List.is_empty f.rConst) then - warn_simpl_unfolding_modifiers () in - (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) - | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast) - | Cbn f -> - (e_red (strong_cbn (make_flag f)), DEFAULTcast) - | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast) - | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast) - | Fold cl -> (e_red (fold_commands cl),DEFAULTcast) - | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast) - | ExtraRedExpr s -> - (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast) - with Not_found -> - (try reduction_of_red_expr (String.Map.find s !red_expr_tab) - with Not_found -> - user_err ~hdr:"Redexpr.reduction_of_red_expr" - (str "unknown user-defined reduction \"" ++ str s ++ str "\""))) - | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) - | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) - in - reduction_of_red_expr - -let subst_mps subst c = - EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c)) - -let subst_red_expr subs = - Redops.map_red_expr_gen - (subst_mps subs) - (Mod_subst.subst_evaluable_reference subs) - (Patternops.subst_pattern subs) - -let inReduction : bool * string * red_expr -> obj = - declare_object - {(default_object "REDUCTION") with - cache_function = (fun (_,(_,s,e)) -> decl_red_expr s e); - load_function = (fun _ (_,(_,s,e)) -> decl_red_expr s e); - subst_function = - (fun (subs,(b,s,e)) -> b,s,subst_red_expr subs e); - classify_function = - (fun ((b,_,_) as obj) -> if b then Dispose else Substitute obj) } - -let declare_red_expr locality s expr = - Lib.add_anonymous_leaf (inReduction (locality,s,expr)) diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli deleted file mode 100644 index 1e59f436c3..0000000000 --- a/proofs/redexpr.mli +++ /dev/null @@ -1,48 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Interpretation layer of redexprs such as hnf, cbv, etc. *) - -open Names -open Constr -open EConstr -open Pattern -open Genredexpr -open Reductionops -open Locus - -type red_expr = - (constr, evaluable_global_reference, constr_pattern) red_expr_gen - -val out_with_occurrences : 'a with_occurrences -> occurrences * 'a - -val reduction_of_red_expr : - Environ.env -> red_expr -> e_reduction_function * cast_kind - -(** [true] if we should use the vm to verify the reduction *) - -(** Adding a custom reduction (function to be use at the ML level) - NB: the effect is permanent. *) -val declare_reduction : string -> reduction_function -> unit - -(** Adding a custom reduction (function to be called a vernac command). - The boolean flag is the locality. *) -val declare_red_expr : bool -> string -> red_expr -> unit - -(** Opaque and Transparent commands. *) - -(** Sets the expansion strategy of a constant. When the boolean is - true, the effect is non-synchronous (i.e. it does not survive - section and module closure). *) -val set_strategy : - bool -> (Conv_oracle.level * evaluable_global_reference list) list -> unit - -(** call by value normalisation function using the virtual machine *) -val cbv_vm : reduction_function diff --git a/proofs/refine.ml b/proofs/refine.ml index 540a8bb420..1d796fece5 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -27,7 +27,7 @@ let extract_prefix env info = let typecheck_evar ev env sigma = let info = Evd.find sigma ev in - (** Typecheck the hypotheses. *) + (* Typecheck the hypotheses. *) let type_hyp (sigma, env) decl = let t = NamedDecl.get_type decl in let sigma, _ = Typing.sort_of env sigma t in @@ -40,7 +40,7 @@ let typecheck_evar ev env sigma = let (common, changed) = extract_prefix env info in let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in - (** Typecheck the conclusion *) + (* Typecheck the conclusion *) let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in sigma @@ -60,39 +60,39 @@ let generic_refine ~typecheck f gl = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let state = Proofview.Goal.state gl in - (** Save the [future_goals] state to restore them after the - refinement. *) + (* Save the [future_goals] state to restore them after the + refinement. *) let prev_future_goals = Evd.save_future_goals sigma in - (** Create the refinement term *) + (* Create the refinement term *) Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () -> f >>= fun (v, c) -> Proofview.tclEVARMAP >>= fun sigma -> Proofview.V82.wrap_exceptions begin fun () -> let evs = Evd.save_future_goals sigma in - (** Redo the effects in sigma in the monad's env *) + (* Redo the effects in sigma in the monad's env *) let privates_csts = Evd.eval_side_effects sigma in let sideff = Safe_typing.side_effects_of_private_constants privates_csts in let env = add_side_effects env sideff in - (** Check that the introduced evars are well-typed *) + (* Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in - (** Check that the refined term is typesafe *) + (* Check that the refined term is typesafe *) let sigma = if typecheck then Typing.check env sigma c concl else sigma in - (** Check that the goal itself does not appear in the refined term *) + (* Check that the goal itself does not appear in the refined term *) let self = Proofview.Goal.goal gl in let _ = if not (Evarutil.occur_evar_upto sigma self c) then () else Pretype_errors.error_occur_check env sigma self c in - (** Restore the [future goals] state. *) + (* Restore the [future goals] state. *) let sigma = Evd.restore_future_goals sigma prev_future_goals in - (** Select the goals *) + (* Select the goals *) let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in - (** Proceed to the refinement *) + (* Proceed to the refinement *) let sigma = match Proofview.Unsafe.advance sigma self with | None -> - (** Nothing to do, the goal has been solved by side-effect *) + (* Nothing to do, the goal has been solved by side-effect *) sigma | Some self -> match evkmain with @@ -104,11 +104,11 @@ let generic_refine ~typecheck f gl = | None -> sigma | Some id -> Evd.rename evk id sigma in - (** Mark goals *) + (* Mark goals *) let sigma = Proofview.Unsafe.mark_as_goals sigma comb in let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in - let trace () = Pp.(hov 2 (str"simple refine"++spc()++ - Termops.Internal.print_constr_env env sigma c)) in + let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++ + Termops.Internal.print_constr_env env sigma c)) in Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> Proofview.Unsafe.tclEVARS sigma <*> diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 64d7630d55..df90354717 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -15,7 +15,6 @@ open Environ open Reductionops open Evd open Typing -open Redexpr open Tacred open Logic open Context.Named.Declaration @@ -71,11 +70,6 @@ let pf_global gls id = let sigma = project gls in Evd.fresh_global env sigma (Constrintern.construct_reference (pf_hyps gls) id) -let pf_reduction_of_red_expr gls re c = - let (redfun, _) = reduction_of_red_expr (pf_env gls) re in - let sigma = project gls in - redfun (pf_env gls) sigma c - let pf_apply f gls = f (pf_env gls) (project gls) let pf_eapply f gls x = on_sig gls (fun evm -> f (pf_env gls) evm x) @@ -133,7 +127,7 @@ module New = struct f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; } let pf_global id gl = - (** We only check for the existence of an [id] in [hyps] *) + (* We only check for the existence of an [id] in [hyps] *) let hyps = Proofview.Goal.hyps gl in Constrintern.construct_reference hyps id @@ -149,12 +143,12 @@ module New = struct let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2 let pf_ids_of_hyps gl = - (** We only get the identifiers in [hyps] *) + (* We only get the identifiers in [hyps] *) let hyps = Proofview.Goal.hyps gl in ids_of_named_context hyps let pf_ids_set_of_hyps gl = - (** We only get the identifiers in [hyps] *) + (* We only get the identifiers in [hyps] *) let env = Proofview.Goal.env gl in Environ.ids_of_named_context_val (Environ.named_context_val env) @@ -186,7 +180,7 @@ module New = struct List.hd hyps let pf_nf_concl (gl : Proofview.Goal.t) = - (** We normalize the conclusion just after *) + (* We normalize the conclusion just after *) let concl = Proofview.Goal.concl gl in let sigma = project gl in nf_evar sigma concl diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index ef6a1544e4..213ed7bfda 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -12,7 +12,6 @@ open Names open Constr open Environ open EConstr -open Redexpr open Locus (** Operations for handling terms under a local typing context. *) @@ -44,9 +43,6 @@ val pf_get_hyp_typ : Goal.goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> Goal.goal sigma -> Id.t -val pf_reduction_of_red_expr : Goal.goal sigma -> red_expr -> constr -> evar_map * constr - - val pf_apply : (env -> evar_map -> 'a) -> Goal.goal sigma -> 'a val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) -> Goal.goal sigma -> 'a -> Goal.goal sigma * 'b |