From a7a6fa3219134004f1fc6c757f1c16281724f38f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 24 May 2019 14:57:33 +0200
Subject: [vernac] more precise types for Add Morph, Instance, and Function

---
 plugins/funind/indfun.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index bb6db1f5cf..241da053b7 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -434,7 +434,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        None, evd,List.rev rev_pconstants
     | _ ->
-      let pstate = ComFixpoint.do_fixpoint Global false fixpoint_exprl in
+       ComFixpoint.do_fixpoint Global false fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
@@ -448,7 +448,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
        in
-       pstate,evd,List.rev rev_pconstants
+       None,evd,List.rev rev_pconstants
 
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
-- 
cgit v1.2.3