diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-19 08:42:37 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-19 08:42:37 +0000 |
| commit | efc43d10527308cfc3ec358f9a14420add3735d0 (patch) | |
| tree | 6f372e3bd279beb98e9d02dc967529ffb8529c37 /contrib/interface | |
| parent | 7d8a167b36d1f27cc38f3b042eb6f2c01a8b6177 (diff) | |
Renommage qualid_of_global en shortest_qualid_of_global
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2201 85f007b7-540e-0410-9357-904b9bb8a0f7
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 bba7396b0..eae99993f 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 8d3fd79c0..e96106368 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]);; |