let not_implemented =
"discharge of current proofs is not implemented yet"
+let debug = ref false
+
(* helper functions *********************************************************)
let list_pos found l =
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')
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 =