...

[helm.git] / helm / software / components / cic_proof_checking / cicDischarge.ml

diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml
index f8ad074fb67081198cabf45c38d00d67c27b8e3a..52b841952a2158e47784108e62ea5f740ece3ca0 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicDischarge.ml
+++ b/helm/software/components/cic_proof_checking/cicDischarge.ml
@@ -33,6 +33,8 @@ let hashtbl_size = 11
 let not_implemented =
    "discharge of current proofs is not implemented yet"
 
+let debug = ref false
+
 (* helper functions *********************************************************)
 
 let list_pos found l =
@@ -108,11 +110,10 @@ let rec discharge_term st t = match t with
       let s = List.map (mk_arg s) args in
       C.Appl (C.MutConstruct (st.du u, m, n, []) :: discharge_nsubst st s)
    | C.Var (u, s)                 ->
-(* FG: We do not discharge the nsubst here ?? *)   
-      let args = get_args st u in
-      if args = [] then C.Rel (discharge st u) else
-      let s = List.map (mk_arg s) args in
-      (* C.Appl ( *) C.Rel (discharge st u) (* :: discharge_nsubst st s) *)
+(* We do not discharge the nsubst because variables are not closed *)
+(* thus only the identity nsubst should be allowed                 *)
+      if s <> [] then assert false else
+      C.Rel (discharge st u)
    | C.Meta (i, s)                ->
       let s' = list_map_sh (discharge_usubst st) s in
       if s' == s then t else C.Meta (i, s')
@@ -232,9 +233,9 @@ let rec discharge_object dn du obj =
 
 and discharge_uri dn du uri =
    let obj, _ = E.get_obj Un.default_ugraph uri in
-   prerr_endline ("Plain     : " ^ CicPp.ppobj obj); 
+   if !debug then prerr_endline ("Plain     : " ^ CicPp.ppobj obj); 
    let obj' = discharge_object dn du obj in
-   prerr_endline ("Discharged: " ^ CicPp.ppobj obj'); 
+   if !debug then prerr_endline ("Discharged: " ^ CicPp.ppobj obj'); 
    obj', obj' == obj
 
 and discharge_vars dn du vars =