let new_aliases =
match ex with
| TA.Command (_, TA.Alias _)
- | TA.Command (_, TA.Include _) -> DisambiguateTypes.Environment.empty
+ | TA.Command (_, TA.Include _)
+ | TA.Command (_, TA.Interpretation _) ->
+ DisambiguateTypes.Environment.empty
| _ -> MatitaSync.alias_diff ~from:status new_status
in
(* we remove the defined object since we consider them "automatic aliases" *)
let initial_space,status,new_status_and_text_list_rev =
let module DTE = DisambiguateTypes.Environment in
let module UM = UriManager in
- DTE.fold (
+ DTE.fold_flatten (
fun k ((v,_) as value) (initial_space,status,acc) ->
let b =
try
let initial_space =
if initial_space = "" then "\n" else initial_space in
initial_space ^
- DisambiguatePp.pp_environment(DTE.add k value DTE.empty) in
+ DisambiguatePp.pp_environment(DTE.cons k value DTE.empty) in
let new_status =
- {status with aliases = DTE.add k value status.aliases}
+ {status with aliases = DTE.cons k value status.aliases}
in
"\n",new_status,((new_status, new_text)::acc)
) new_aliases (initial_space,status,[]) in
let aliases = MatitaMisc.get_proof_aliases status in
let interps = MD.disambiguate_term dbd context metasenv aliases term in
match interps with
- | [_,_,x,_] -> x
+ | [_,_,x,_], _ -> x
| _ -> assert false
let eval_macro guistuff status unparsed_text parsed_text script mac =
in
let _, metasenv , term, ugraph =
match interps with
- | [x] -> x
+ | [x], _ -> x
| _ -> assert false
in
let ty,_ = CTC.type_of_aux' metasenv context term ugraph in