diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 96c323d73..83af30949 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -669,7 +669,8 @@ let h_discrHyp = hide_ident_tactic "DiscrHyp" discrHyp let existS_pattern = put_pat mmk "(existS ?1 ?2 ?3 ?4)" let existT_pattern = put_pat mmk "(existT ?1 ?2 ?3 ?4)" -let constant dir s = Declare.global_qualified_reference (make_qualid dir s) +let constant dir s = + Declare.global_absolute_reference (make_path dir (id_of_string s) CCI) let build_sigma_set () = { proj1 = constant ["Specif"] "projS1"; |