diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/search.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 18 |
3 files changed, 2 insertions, 20 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 8e6a0f6a72..aba61146c7 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -341,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p if not (Option.is_empty term) then let init_refine = Tacticals.New.tclTHENLIST [ - Refine.refine (fun evm -> (evm,EConstr.of_constr (Option.get term))); + Refine.refine ~typecheck:false (fun evm -> (evm,EConstr.of_constr (Option.get term))); Proofview.Unsafe.tclNEWGOALS gls; Tactics.New.reduce_after_refine; ] diff --git a/vernac/search.ml b/vernac/search.ml index 9160158003..0ff78f439d 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -142,7 +142,7 @@ module ConstrPriority = struct -(3*(num_symbols t) + size t) let compare (_,_,_,p1) (_,_,_,p2) = - compare p1 p2 + Pervasives.compare p1 p2 end module PriorityQueue = Heap.Functional(ConstrPriority) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 5d1def7a4b..c76ced56fd 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -60,13 +60,6 @@ let show_proof () = let pprf = Proof.partial_proof p in Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf) -let show_node () = - (* spiwack: I'm have little clue what this function used to do. I deactivated it, - could, possibly, be cleaned away. (Feb. 2010) *) - () - -let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO.") - let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) let pfts = Proof_global.give_me_the_proof () in @@ -82,9 +75,6 @@ let show_universes () = Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma)); Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx) -(* Spiwack: proof tree is currently not working *) -let show_prooftree () = () - (* Simulate the Intro(s) tactic *) let show_intro all = let open EConstr in @@ -1843,21 +1833,13 @@ let vernac_show = let open Feedback in function | GoalUid id -> pr_goal_by_uid id in msg_notice info - | ShowGoalImplicitly None -> - Constrextern.with_implicits msg_notice (pr_open_subgoals ()) - | ShowGoalImplicitly (Some n) -> - Constrextern.with_implicits msg_notice (pr_nth_open_subgoal n) | ShowProof -> show_proof () - | ShowNode -> show_node () | ShowExistentials -> show_top_evars () | ShowUniverses -> show_universes () - | ShowTree -> show_prooftree () | ShowProofNames -> msg_notice (pr_sequence pr_id (Proof_global.get_all_proof_names())) | ShowIntros all -> show_intro all | ShowMatch id -> show_match id - | ShowThesis -> show_thesis () - let vernac_check_guard () = let pts = Proof_global.give_me_the_proof () in |