diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-12 17:49:21 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-12 17:49:21 +0000 |
| commit | cb1ae314411d78952062e5092804b85d981ad6e1 (patch) | |
| tree | 52b9a4058c89b5849d875a4c1129951f35e9c1b1 /contrib/interface/centaur.ml4 | |
| parent | 7cb6a61133b6e3c2cd5601282a1f472ff0104c1f (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/centaur.ml4')
| -rw-r--r-- | contrib/interface/centaur.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index c9197ab34..87f8c8af1 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -259,7 +259,7 @@ let filter_by_module_from_varg_list l = let add_search (global_reference:global_reference) assumptions cstr = try let id_string = - string_of_qualid (Nametab.shortest_qualid_of_global None + string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty global_reference) in let ast = try @@ -323,10 +323,10 @@ let globcv x = match x with | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) -> convert_qualid - (Nametab.shortest_qualid_of_global None (IndRef(sp,tyi))) + (Nametab.shortest_qualid_of_global Idset.empty (IndRef(sp,tyi))) | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) -> convert_qualid - (Nametab.shortest_qualid_of_global None + (Nametab.shortest_qualid_of_global Idset.empty (ConstructRef ((sp, tyi), i))) | _ -> failwith "globcv : unexpected value";; |