From b36adb2124d3ba8a5547605e7f89bb0835d0ab10 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 15:50:17 +0100 Subject: Removing some return type compatibility layers in Termops. --- tactics/eqschemes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/eqschemes.ml') diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index a8ea7446f..e68267584 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -77,7 +77,7 @@ let build_dependent_inductive ind (mib,mip) = @ Context.Rel.to_extended_list 0 realargs) let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s -let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn c s +let my_it_mkProd_or_LetIn s c = Term.it_mkProd_or_LetIn c s let my_it_mkLambda_or_LetIn_name s c = it_mkLambda_or_LetIn_name (Global.env()) c s -- cgit v1.2.3