Code mort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6420 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 3 deletions

diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index 7d7de9de48..792507abaf 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -68,6 +68,7 @@ let id_of_name = function
 let string_of_name nme = string_of_id (id_of_name nme)
  (*end debugging *)
 
+(* Interpretation of constr's *)
 let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
 
 let rec collect_cases l =
@@ -539,9 +540,6 @@ let rec proofPrinc mi lst_vars lst_eqs lst_recs:
 
 let mkevarmap_aux ex = let x,y = ex in	(mkevarmap_from_listex x),y
 
-(* Interpretation of constr's *)
-let constr_of_Constr c = Constrintern.interp_constr Evd.empty (Global.env()) c
-
 
 (* TODO: deal with any term, not only a constant. *)
 let interp_fonc_tacarg fonctac gl =