From 5cac24428e448c12ab292265bb2ffd1146b38c25 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 13 Sep 2020 14:37:43 +0200
Subject: Almost fully moving funind to new proof engine.

---
 plugins/funind/functional_principles_proofs.mli | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/functional_principles_proofs.mli')

diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 52089ca7fb..096ea5fed5 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
 open Names
 
 val prove_princ_for_struct :
@@ -7,7 +17,7 @@ val prove_princ_for_struct :
   -> Constant.t array
   -> EConstr.constr array
   -> int
-  -> Tacmach.tactic
+  -> unit Proofview.tactic
 
 val prove_principle_for_gen :
      Constant.t * Constant.t * Constant.t
@@ -22,6 +32,6 @@ val prove_principle_for_gen :
   -> (* the type of the recursive argument *)
      EConstr.constr
   -> (* the wf relation used to prove the function *)
-     Tacmach.tactic
+     unit Proofview.tactic
 
 (* val is_pte  : rel_declaration -> bool  *)
-- 
cgit v1.2.3