From 3658ae24886eb42b62243ded5beca059363971f1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 17 May 2020 05:01:40 +0200
Subject: [leminv] Remove unused catch.

---
 plugins/ltac/leminv.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml
index 0024d1a4ba..9841d3a14c 100644
--- a/plugins/ltac/leminv.ml
+++ b/plugins/ltac/leminv.ml
@@ -246,11 +246,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac =
   let sigma = Evd.from_env env in
   let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in
   let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
-  try
-    add_inversion_lemma ~poly na env sigma c sort bool tac
-  with
-    |   UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
-          user_err ~hdr:"Inv needs Nodep Prop Set" s
+  add_inversion_lemma ~poly na env sigma c sort bool tac
 
 (* ================================= *)
 (* Applying a given inversion lemma  *)
-- 
cgit v1.2.3


From 9cc65e592fda6c84e7f1eb8bee3e79a7ce777323 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 17 May 2020 05:07:21 +0200
Subject: [leminv] Use higher-level Declare API.

---
 plugins/ltac/leminv.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml
index 9841d3a14c..47df3ec34f 100644
--- a/plugins/ltac/leminv.ml
+++ b/plugins/ltac/leminv.ml
@@ -228,14 +228,15 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
   let c = fill_holes pfterm in
   (* warning: side-effect on ownSign *)
   let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
-  let p = EConstr.to_constr sigma invProof in
-  p, sigma
+  invProof, sigma
 
 let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
   let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
-  let univs = Evd.univ_entry ~poly sigma in
-  let entry = Declare.definition_entry ~univs invProof in
-  let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in
+  let cinfo = Declare.CInfo.make ~name ~typ:None () in
+  let info = Declare.Info.make ~poly ~kind:Decls.(IsProof Lemma) () in
+  let _ : Names.GlobRef.t =
+    Declare.declare_definition ~cinfo ~info ~opaque:false ~body:invProof sigma
+  in
   ()
 
 (* inv_op = Inv (derives de complete inv. lemma)
-- 
cgit v1.2.3