X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.mli;h=6d4ef50da0bae3a7a135f9af1397644e1ca357cc;hb=5b45f78ed4293ebbe8cc73ad925bca11a300d021;hp=239c789c2645876dc28455578665fb8b8d343042;hpb=2ea5357bace160aaf57750d9dcfb3077fe5a1b38;p=helm.git diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli index 239c789c2..6d4ef50da 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.mli +++ b/helm/software/components/acic_procedural/proceduralHelpers.mli @@ -23,14 +23,14 @@ * http://cs.unibo.it/helm/. *) -val print_times: - string -> unit -val pp_term: - (string -> unit) -> Cic.metasenv -> Cic.context -> Cic.term -> unit val mk_fresh_name: Cic.context -> Cic.name -> Cic.name +val list_fold_right_cps: + ('b -> 'c) -> (('b -> 'c) -> 'a -> 'b -> 'c) -> 'a list -> 'b -> 'c +val list_fold_left_cps: + ('b -> 'c) -> (('b -> 'c) -> 'b -> 'a -> 'c) -> 'b -> 'a list -> 'c val list_map_cps: - ('a list -> 'b) -> (('a -> 'b) -> 'c -> 'b) -> 'c list -> 'b + ('b list -> 'c) -> (('b -> 'c) -> 'a -> 'c) -> 'a list -> 'c val identity: 'a -> 'a val compose: @@ -41,6 +41,8 @@ val refine: Cic.context -> Cic.term -> Cic.term val get_type: string -> Cic.context -> Cic.term -> Cic.term +val is_prop: + Cic.context -> Cic.term -> bool val is_proof: Cic.context -> Cic.term -> bool val is_sort: