diff options
Diffstat (limited to 'contrib/omega/coq_omega.ml')
| -rw-r--r-- | contrib/omega/coq_omega.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index bdf4544f95..3b2dff70d9 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -207,9 +207,7 @@ let recognize_number t = To use the constant Zplus, one must type "Lazy.force coq_Zplus" This is the right way to access to Coq constants in tactics ML code *) -let constant dir id = - Declare.global_qualified_reference - (make_path dir (id_of_string id) CCI) +let constant dir s = Declare.global_qualified_reference (make_qualid dir s) (* fast_integer *) let coq_xH = lazy (constant ["fast_integer"] "xH") |