diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:38 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:38 +0200 |
| commit | 3a420f4ad929e8372d32c735fd0fd89dfc0346a1 (patch) | |
| tree | 943a01d103c1296dc7c07cb188af994354c4d9a3 /contrib/subtac/subtac_utils.mli | |
| parent | 1769cbaddea77112dd6f336316d8eb9a0945a1e6 (diff) | |
| parent | e4282ea99c664d8d58067bee199cbbcf881b60d5 (diff) | |
Merge commit 'upstream/8.2.pl1+dfsg'
Diffstat (limited to 'contrib/subtac/subtac_utils.mli')
| -rw-r--r-- | contrib/subtac/subtac_utils.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 964f668f..9c014286 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -45,9 +45,9 @@ val and_typ : constr lazy_t val eqdep_ind : constr lazy_t val eqdep_rec : constr lazy_t -val jmeq_ind : constr lazy_t -val jmeq_rec : constr lazy_t -val jmeq_refl : constr lazy_t +val jmeq_ind : unit -> constr +val jmeq_rec : unit -> constr +val jmeq_refl : unit -> constr val boolind : constr lazy_t val sumboolind : constr lazy_t @@ -103,7 +103,7 @@ val mk_ex_pi1 : constr -> constr -> constr -> constr val mk_ex_pi1 : constr -> constr -> constr -> constr val mk_eq : types -> constr -> constr -> types val mk_eq_refl : types -> constr -> constr -val mk_JMeq : types -> constr-> types -> constr -> types +val mk_JMeq : types -> constr -> types -> constr -> types val mk_JMeq_refl : types -> constr -> constr val mk_conj : types list -> types val mk_not : types -> types |