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.

---
 stm/lemmas.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 04f888a84d..9942e911ab 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -466,7 +466,7 @@ let start_proof_com ?inference_hook kind thms hook =
     evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref);
     let ids = List.map RelDecl.get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
-      (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
+      (nf_evar !evdref (Term.it_mkProd_or_LetIn t' ctx),
        (ids, imps @ lift_implicits (List.length ids) imps'),
        guard)))
     thms in
-- 
cgit v1.2.3