diff options
| author | herbelin | 2000-11-22 21:32:03 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-22 21:32:03 +0000 |
| commit | 937ca7a6dbc1a031b7c4540c665b8774440c1bb9 (patch) | |
| tree | 3a2c73669cb40011c2e62a11d3364d39f74040ba /tactics | |
| parent | de9150e6033467fd2fa8fc93d5f057e8c2f6537f (diff) | |
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 'section_path' pour les noms absolus
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 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, 2 insertions, 4 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 9228013be5..7d59ecf215 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -669,8 +669,7 @@ 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 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) let build_sigma_set () = { proj1 = constant ["Specif"] "projS1"; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4f4afec9ba..3b152c27c1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1516,8 +1516,7 @@ let contradiction_on_hyp id gl = else error "Not a contradiction" -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) let coq_False = lazy (constant ["Logic"] "False") let coq_not = lazy (constant ["Logic"] "not") |