diff options
| author | herbelin | 2000-11-20 08:46:32 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-20 08:46:32 +0000 |
| commit | 97fd28463ab88a6f1503f9c8c198ca51ef8d6a55 (patch) | |
| tree | ea193230d26eddac67ee1494c31ba90f994ca5ec /tactics | |
| parent | 53e4f67c6dff411646c56663a2e86c45b613f7b9 (diff) | |
Remplacement des hacks pour les noms longs par un appel à Declare.global_qualified_reference
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@871 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 6d1cc5a691..f86e538f19 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -669,19 +669,22 @@ let h_discrHyp = hide_ident_tactic "DiscrHyp" discrHyp let existS_pattern = put_pat mmk "(existS ? ? ? ?)" let existT_pattern = put_pat mmk "(existT ? ? ? ?)" +let constant dir id = + Declare.global_qualified_reference (make_path dir (id_of_string id) CCI) + let build_sigma_set () = - { proj1 = get_reference ["Specif"] "projS1"; - proj2 = get_reference ["Specif"] "projS2"; - elim = get_reference ["Specif"] "sigS_rec"; - intro = get_reference ["Specif"] "existS"; - ex = get_reference ["Specif"] "sigS" } + { proj1 = constant ["Specif"] "projS1"; + proj2 = constant ["Specif"] "projS2"; + elim = constant ["Specif"] "sigS_rec"; + intro = constant ["Specif"] "existS"; + ex = constant ["Specif"] "sigS" } let build_sigma_type () = - { proj1 = get_reference ["Specif"] "projT1"; - proj2 = get_reference ["Specif"] "projT2"; - elim = get_reference ["Specif"] "sigT_rec"; - intro = get_reference ["Specif"] "existT"; - ex = get_reference ["Specif"] "sigT" } + { proj1 = constant ["Specif"] "projT1"; + proj2 = constant ["Specif"] "projT2"; + elim = constant ["Specif"] "sigT_rec"; + intro = constant ["Specif"] "existT"; + ex = constant ["Specif"] "sigT" } (* returns the sigma type (sigS, sigT) with the respective constructor depending on the sort *) |