diff options
| -rw-r--r-- | contrib/funind/tacinv.ml4 | 4 |
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 = |