class clickableMathView obj =
let text_width = 80 in
-let dummy_loc = DisambiguateTypes.dummy_floc in
+let dummy_loc = HExtlib.dummy_floc in
object (self)
inherit GMathViewAux.multi_selection_math_view obj
let reduction_action kind () =
let pat = self#tactic_text_pattern_of_selection in
let statement =
- let loc = DisambiguateTypes.dummy_floc in
+ let loc = HExtlib.dummy_floc in
"\n" ^
GrafiteAstPp.pp_executable ~term_pp:(fun s -> s)
~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
method private home () =
self#_showMath;
- match self#script#status.proof_status with
+ match self#script#grafite_status.proof_status with
| Proof (uri, metasenv, bo, ty) ->
let name = UriManager.name_of_uri (HExtlib.unopt uri) in
let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in