]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_procedural/proceduralHelpers.mli
- Procedural: new flag "level=n" to control the reconstruction level (defaults to...
[helm.git] / helm / software / components / acic_procedural / proceduralHelpers.mli
index 358012c8765de46f551660d0fca12e62cccfc463..203224371f72f724b01bd472b85c9f3edac98d18 100644 (file)
@@ -71,3 +71,6 @@ val cic_bc:
    Cic.context -> Cic.term -> Cic.term
 val acic_bc:
    Cic.context -> Cic.annterm -> Cic.annterm
+val is_acic_proof:
+   (Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.context -> Cic.annterm ->
+   bool