CicTypeChecker.typecheck now takes an additional parameter:

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.mli

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.mli b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
index 98cb72ad773577cd9d2b2e5dc3952dbdf57bc657..a3361fc7be609f6c860cd5788de5662bb59fd148 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
@@ -37,7 +37,9 @@ val debrujin_constructor :
  ?check_exp_named_subst: bool ->
   UriManager.uri -> int -> Cic.context -> Cic.term -> Cic.term
 
-val typecheck : UriManager.uri -> Cic.obj * CicUniv.universe_graph
+  (* defaults to true *)
+val typecheck : 
+  ?trust:bool -> UriManager.uri -> Cic.obj * CicUniv.universe_graph
 
 (* FUNCTIONS USED ONLY IN THE TOPLEVEL *)