diff options
| author | herbelin | 2000-11-26 20:43:25 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-26 20:43:25 +0000 |
| commit | 96a64b9be7551b562e0f6d3204a8a1af837a0626 (patch) | |
| tree | 16a34129a30dfd88568216945fa257834099aa8f /tactics | |
| parent | 735070100540076e715792bf17fa291e4a4cbfd5 (diff) | |
Appel des constantes globaux par des noms absolus
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@966 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 3 |
2 files changed, 4 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 96c323d733..83af309491 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"; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6d3da97ad0..cf9946b8e9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1524,7 +1524,8 @@ let contradiction_on_hyp id gl = else error "Not a contradiction" -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 coq_False = lazy (constant ["Logic"] "False") let coq_not = lazy (constant ["Logic"] "not") |