From 1cdd34d7c286ab22d942e2dd1b1420e1c1caeff6 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 18 Jan 2010 07:25:27 +0000 Subject: [PATCH] Keeping Implicit for refinement (instead of transforming them to Metas: context bug). --- helm/software/components/ng_paramodulation/nCicParamod.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index 739e76f05..b3ab4d504 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -35,6 +35,7 @@ let readback rdb metasenv subst context (bag,i,fo_subst,l) = let proofterm,prooftype = NCicProof.mk_proof bag i fo_subst l in (* debug (lazy (Printf.sprintf "Got proof term in %fs" (Unix.gettimeofday() -. stamp))); *) +(* let metasenv, proofterm = let rec aux k metasenv = function | NCic.Meta _ as t -> metasenv, t @@ -47,7 +48,7 @@ let readback rdb metasenv subst context (bag,i,fo_subst,l) = (fun _ k -> k+1) k aux metasenv t in aux 0 metasenv proofterm - in + in *) debug (lazy (NCicPp.ppterm ~metasenv ~subst ~context proofterm)); (* let stamp = Unix.gettimeofday () in -- 2.39.2