diff options
| author | herbelin | 2009-05-09 20:20:22 +0000 |
|---|---|---|
| committer | herbelin | 2009-05-09 20:20:22 +0000 |
| commit | 8654111ba8e98680aa7965468a82746352b362a7 (patch) | |
| tree | 2f3224d3aa6628a06997078e476b7cfd1e756553 /interp | |
| parent | eceac2ae83fe49e235be8fd930030e80f484f66f (diff) | |
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
as hints (see wish #2104).
- New type hint_entry for interpreted hint.
- Better centralization of functions dealing with evaluable_global_reference.
- Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had
uglily to be factorized by hand.
- Typography in RefMan-tac.tex.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12121 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/coqlib.ml | 14 | ||||
| -rw-r--r-- | interp/coqlib.mli | 5 |
2 files changed, 17 insertions, 2 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 43c7747077..087a519826 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -258,6 +258,10 @@ let coq_and = lazy_init_constant ["Logic"] "and" let coq_conj = lazy_init_constant ["Logic"] "conj" let coq_or = lazy_init_constant ["Logic"] "or" let coq_ex = lazy_init_constant ["Logic"] "ex" +let coq_iff = lazy_init_constant ["Logic"] "iff" + +let coq_iff_left_proj = lazy_init_constant ["Logic"] "proj1" +let coq_iff_right_proj = lazy_init_constant ["Logic"] "proj2" (* Runtime part *) let build_coq_True () = Lazy.force coq_True @@ -267,8 +271,13 @@ let build_coq_False () = Lazy.force coq_False let build_coq_not () = Lazy.force coq_not let build_coq_and () = Lazy.force coq_and let build_coq_conj () = Lazy.force coq_conj -let build_coq_or () = Lazy.force coq_or -let build_coq_ex () = Lazy.force coq_ex +let build_coq_or () = Lazy.force coq_or +let build_coq_ex () = Lazy.force coq_ex +let build_coq_iff () = Lazy.force coq_iff + +let build_coq_iff_left_proj () = Lazy.force coq_iff_left_proj +let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj + (* The following is less readable but does not depend on parsing *) let coq_eq_ref = lazy (init_reference ["Logic"] "eq") @@ -280,4 +289,5 @@ let coq_False_ref = lazy (init_reference ["Logic"] "False") let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool") let coq_sig_ref = lazy (init_reference ["Specif"] "sig") let coq_or_ref = lazy (init_reference ["Logic"] "or") +let coq_iff_ref = lazy (init_reference ["Logic"] "iff") diff --git a/interp/coqlib.mli b/interp/coqlib.mli index a4751f6e79..7e13b1b1ed 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -137,6 +137,10 @@ val build_coq_not : constr delayed (* Conjunction *) val build_coq_and : constr delayed val build_coq_conj : constr delayed +val build_coq_iff : constr delayed + +val build_coq_iff_left_proj : constr delayed +val build_coq_iff_right_proj : constr delayed (* Disjunction *) val build_coq_or : constr delayed @@ -154,3 +158,4 @@ val coq_sumbool_ref : global_reference lazy_t val coq_sig_ref : global_reference lazy_t val coq_or_ref : global_reference lazy_t +val coq_iff_ref : global_reference lazy_t |