let new_env = build_aliases [(name,uri)] in
LexiconEngine.set_proof_aliases status new_env
-let add_aliases_for_object status uri =
- function
- Cic.InductiveDefinition (types,_,_,_) ->
- add_aliases_for_inductive_def status types uri
- | Cic.Constant _ -> add_alias_for_constant status uri
- | Cic.Variable _
- | Cic.CurrentProof _ -> assert false
-
let add_aliases_for_objs status =
- function
- `Old uris ->
- List.fold_left
- (fun status uri ->
- let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- add_aliases_for_object status uri obj) status uris
- | `New nrefs ->
+ function
+ `Old _ -> assert false (* MATITA 1.0 *)
+ | `New nrefs ->
List.fold_left
(fun status nref ->
let references = NCicLibrary.aliases_of nref in