GrafiteDisambiguate.disambiguate_tactic
lexicon_status_ref
(GrafiteTypes.get_proof_context grafite_status goal)
- (GrafiteTypes.get_proof_metasenv grafite_status)
+ (GrafiteTypes.get_proof_metasenv grafite_status) (Some goal)
tac
in
GrafiteTypes.set_metasenv metasenv grafite_status,tac
LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in
let _,intermediate_states =
List.fold_left
- (fun (lexicon_status,acc) (k,((v,_) as value)) ->
+ (fun (lexicon_status,acc) (k,value) ->
+ let v = LexiconAst.description_of_alias value in
let b =
try
(* this hack really sucks! *)
?do_heavy_checks ?(enforce_no_new_aliases=true)
?(watch_statuses=fun _ _ -> ()) lexicon_status grafite_status str cb
=
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
let rec loop lexicon_status grafite_status statuses =
let loop =
if first_statement_only then fun _ _ statuses -> statuses
(fun (_,alias) ->
match alias with
None -> ()
- | Some (k,((v,_) as value)) ->
- let newtxt =
- DisambiguatePp.pp_environment
- (DisambiguateTypes.Environment.add k value
- DisambiguateTypes.Environment.empty)
- in
+ | Some (k,value) ->
+ let newtxt = LexiconAstPp.pp_alias value in
raise (TryingToAdd newtxt)) new_statuses;
let grafite_status,lexicon_status =
match new_statuses with
in
watch_statuses lexicon_status grafite_status ;
false, lexicon_status, grafite_status, (new_statuses @ statuses))
- with exn when (not (Helm_registry.get_bool "matita.debug")) ->
+ with exn when not matita_debug ->
raise (EnrichedWithLexiconStatus (exn, lexicon_status))
in
if stop then s else loop l g s