X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.mli;h=6ad40b8bb555c91f1f339fcb97861918b40eb724;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=1c3080826158f1fe4b46aa2a5ac16029dc21cf34;hpb=0bd584a839bae570f44c4a5f8a06cdbc55fe0726;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli
index 1c3080826..6ad40b8bb 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.mli
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli
@@ -34,6 +34,27 @@ val typeof:
     NCic.term
 
 val get_relevance : 
-  subst:NCic.substitution ->
+  metasenv:NCic.metasenv -> subst:NCic.substitution ->
   NCic.context -> NCic.term -> NCic.term list -> bool list
 
+(* type_of_branch subst context leftno outtype 
+ *   (constr @ lefts) (ty_constr @ lefts)  *)
+val type_of_branch : 
+  subst:NCic.substitution ->
+    NCic.context -> int -> NCic.term -> NCic.term -> NCic.term -> 
+     NCic.term
+
+(* ind = indtype @ lefts
+ * arity1 = constructor type @ lefts
+ * arity2 = outtype *)
+val check_allowed_sort_elimination : 
+  subst:NCic.substitution ->
+  metasenv:NCic.metasenv ->
+  NReference.reference -> NCic.context -> 
+    NCic.term -> NCic.term -> NCic.term -> unit
+
+(* Functions to be used by the refiner *)
+val debruijn: NUri.uri -> int -> NCic.context -> NCic.term -> NCic.term
+val are_all_occurrences_positive: 
+ subst:NCic.substitution ->
+  NCic.context -> NUri.uri -> int -> int -> int -> int -> NCic.term -> bool