diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b1eb7b6efd..9dd71b75d2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1525,10 +1525,11 @@ let contradiction_on_hyp id gl = error "Not a contradiction" let constant dir s = - Declare.global_absolute_reference (make_path dir (id_of_string s) CCI) + Declare.global_absolute_reference + (make_path ("Coq"::"Init"::dir) (id_of_string s) CCI) -let coq_False = lazy (constant ["Init";"Logic"] "False") -let coq_not = lazy (constant ["Init";"Logic"] "not") +let coq_False = lazy (constant ["Logic"] "False") +let coq_not = lazy (constant ["Logic"] "not") (* Absurd *) let absurd c gls = |