From f613bad27923c0154d5576e87a9dc104f024eb8d Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 17 Oct 2014 16:25:03 +0200
Subject: Proofview: clean up commented out code.

---
 proofs/proofview.ml | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 98a6e7c140..836101ce54 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -156,12 +156,6 @@ let return_constr { solution = defs } c = Evarutil.nf_evar defs c
 
 let partial_proof entry pv = List.map (return_constr pv) (List.map fst entry)
 
-(* let return { initial=init; solution=defs }  = *)
-(*   let evdref = ref defs in *)
-(*   let nf,subst = Evarutil.e_nf_evars_and_universes evdref in *)
-(*   ((List.map (fun (c,t) -> (nf c, nf t)) init, subst), *)
-(*    Evd.universe_context !evdref) *)
-
 (* spiwack: this function should probably go in the Util section,
     but I'd rather have Util (or a separate module for lists)
     raise proper exceptions before *)
-- 
cgit v1.2.3