diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/centaur.ml | 6 | ||||
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml index bba7396b0d..eae99993f6 100644 --- a/contrib/interface/centaur.ml +++ b/contrib/interface/centaur.ml @@ -246,7 +246,7 @@ let add_search (global_reference:global_reference) assumptions cstr = try let env = Global.env() in let id_string = - string_of_qualid (Nametab.qualid_of_global env global_reference) in + string_of_qualid (Nametab.shortest_qualid_of_global env global_reference) in let ast = try CT_premise (CT_ident id_string, translate_constr assumptions cstr) @@ -308,11 +308,11 @@ let globcv = function | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) -> let env = Global.env() in convert_qualid - (Nametab.qualid_of_global env (IndRef(sp,tyi))) + (Nametab.shortest_qualid_of_global env (IndRef(sp,tyi))) | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) -> let env = Global.env() in convert_qualid - (Nametab.qualid_of_global env (ConstructRef ((sp, tyi), i))) + (Nametab.shortest_qualid_of_global env (ConstructRef ((sp, tyi), i))) | _ -> failwith "globcv : unexpected value";; let pbp_tac_pcoq = diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 8d3fd79c06..e961063689 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -110,7 +110,7 @@ let convert_one_inductive sp tyi = let env = Global.env () in let envpar = push_rel_context params env in ope("VERNACARGLIST", - [convert_qualid (Nametab.qualid_of_global env (IndRef (sp, tyi))); + [convert_qualid (Nametab.shortest_qualid_of_global env (IndRef (sp, tyi))); ope("CONSTR", [ast_of_constr true envpar arity]); ope("BINDERLIST", convert_env(List.rev params)); convert_constructors envpar cstrnames cstrtypes]);; |