Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.

1 files changed, 12 insertions, 10 deletions

diff --git a/kernel/constr.mli b/kernel/constr.mli
index fdc3296a6a..7fc57cdb8a 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -45,6 +45,7 @@ type case_info =
                                        in addition to the parameters of the related inductive type
                                        NOTE: "lets" are therefore excluded from the count
                                        NOTE: parameters of the inductive type are also excluded from the count *)
+    ci_relevance : Sorts.relevance; (* relevance of the predicate (not of the inductive!) *)
     ci_pp_info    : case_printing   (* not interpreted by the kernel *)
   }
 
@@ -84,6 +85,7 @@ val mkEvar : existential -> constr
 
 (** Construct a sort *)
 val mkSort : Sorts.t -> types
+val mkSProp : types
 val mkProp : types
 val mkSet  : types
 val mkType : Univ.Universe.t -> types
@@ -97,13 +99,13 @@ type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
 val mkCast : constr * cast_kind * constr -> constr
 
 (** Constructs the product [(x:t1)t2] *)
-val mkProd : Name.t * types * types -> types
+val mkProd : Name.t Context.binder_annot * types * types -> types
 
 (** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *)
-val mkLambda : Name.t * types * constr -> constr
+val mkLambda : Name.t Context.binder_annot * types * constr -> constr
 
 (** Constructs the product [let x = t1 : t2 in t3] *)
-val mkLetIn : Name.t * constr * types * constr -> constr
+val mkLetIn : Name.t Context.binder_annot * constr * types * constr -> constr
 
 (** [mkApp (f, [|t1; ...; tN|]] constructs the application
     {%html:(f t<sub>1</sub> ... t<sub>n</sub>)%}
@@ -160,7 +162,7 @@ val mkCase : case_info * constr * constr * constr array -> constr
    where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
 *)
 type ('constr, 'types) prec_declaration =
-    Name.t array * 'types array * 'constr array
+    Name.t Context.binder_annot array * 'types array * 'constr array
 type ('constr, 'types) pfixpoint =
     (int array * int) * ('constr, 'types) prec_declaration
   (* The array of [int]'s tells for each component of the array of
@@ -213,9 +215,9 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Evar      of 'constr pexistential
   | Sort      of 'sort
   | Cast      of 'constr * cast_kind * 'types
-  | Prod      of Name.t * 'types * 'types             (** Concrete syntax ["forall A:B,C"] is represented as [Prod (A,B,C)]. *)
-  | Lambda    of Name.t * 'types * 'constr            (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)].  *)
-  | LetIn     of Name.t * 'constr * 'types * 'constr  (** Concrete syntax ["let A:C := B in D"] is represented as [LetIn (A,B,C,D)]. *)
+  | Prod      of Name.t Context.binder_annot * 'types * 'types             (** Concrete syntax ["forall A:B,C"] is represented as [Prod (A,B,C)]. *)
+  | Lambda    of Name.t Context.binder_annot * 'types * 'constr            (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)].  *)
+  | LetIn     of Name.t Context.binder_annot * 'constr * 'types * 'constr  (** Concrete syntax ["let A:C := B in D"] is represented as [LetIn (A,B,C,D)]. *)
   | App       of 'constr * 'constr array              (** Concrete syntax ["(F P1 P2 ...  Pn)"] is represented as [App (F, [|P1; P2; ...; Pn|])].
 
                                                           The {!mkApp} constructor also enforces the following invariant:
@@ -297,13 +299,13 @@ val destSort : constr -> Sorts.t
 val destCast : constr -> constr * cast_kind * constr
 
 (** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *)
-val destProd : types -> Name.t * types * types
+val destProd : types -> Name.t Context.binder_annot * types * types
 
 (** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *)
-val destLambda : constr -> Name.t * types * constr
+val destLambda : constr -> Name.t Context.binder_annot * types * constr
 
 (** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *)
-val destLetIn : constr -> Name.t * constr * types * constr
+val destLetIn : constr -> Name.t Context.binder_annot * constr * types * constr
 
 (** Destructs an application *)
 val destApp : constr -> constr * constr array