Add source location for Derive Inversion

Author: SkySkimmer

doc/tools/docgram/common.edit_mlg

@@ -1293,12 +1293,12 @@ command: [
 | REPLACE "Debug" "Off"
 | WITH "Debug" [ "On" | "Off" ]
 | EDIT "Defined" ADD_OPT identref
-| REPLACE "Derive" "Inversion" ident "with" constr "Sort" sort_family
-| WITH "Derive" "Inversion" ident "with" constr OPT ( "Sort" sort_family )
-| DELETE "Derive" "Inversion" ident "with" constr
-| REPLACE "Derive" "Inversion_clear" ident "with" constr "Sort" sort_family
-| WITH "Derive" "Inversion_clear" ident "with" constr OPT ( "Sort" sort_family )
-| DELETE "Derive" "Inversion_clear" ident "with" constr
+| REPLACE "Derive" "Inversion" identref "with" constr "Sort" sort_family
+| WITH "Derive" "Inversion" identref "with" constr OPT ( "Sort" sort_family )
+| DELETE "Derive" "Inversion" identref "with" constr
+| REPLACE "Derive" "Inversion_clear" identref "with" constr "Sort" sort_family
+| WITH "Derive" "Inversion_clear" identref "with" constr OPT ( "Sort" sort_family )
+| DELETE "Derive" "Inversion_clear" identref "with" constr
 | EDIT "Focus" ADD_OPT natural
 | DELETE "Hint" "Rewrite" orient LIST1 constr ":" LIST1 preident
 | REPLACE "Hint" "Rewrite" orient LIST1 constr "using" tactic ":" LIST1 preident

doc/tools/docgram/fullGrammar

@@ -599,12 +599,12 @@ command: [
 | "Hint" "Rewrite" orient LIST1 constr "using" tactic ":" LIST1 preident
 | "Hint" "Rewrite" orient LIST1 constr
 | "Hint" "Rewrite" orient LIST1 constr "using" tactic
-| "Derive" "Inversion_clear" ident "with" constr "Sort" sort_family
-| "Derive" "Inversion_clear" ident "with" constr
-| "Derive" "Inversion" ident "with" constr "Sort" sort_family
-| "Derive" "Inversion" ident "with" constr
-| "Derive" "Dependent" "Inversion" ident "with" constr "Sort" sort_family
-| "Derive" "Dependent" "Inversion_clear" ident "with" constr "Sort" sort_family
+| "Derive" "Inversion_clear" identref "with" constr "Sort" sort_family
+| "Derive" "Inversion_clear" identref "with" constr
+| "Derive" "Inversion" identref "with" constr "Sort" sort_family
+| "Derive" "Inversion" identref "with" constr
+| "Derive" "Dependent" "Inversion" identref "with" constr "Sort" sort_family
+| "Derive" "Dependent" "Inversion_clear" identref "with" constr "Sort" sort_family
 | "Declare" "Left" "Step" constr
 | "Declare" "Right" "Step" constr
 | "Unshelve"

plugins/ltac/extratactics.mlg

@@ -292,7 +292,7 @@ END
 open Inv
 open Leminv
 
-let seff id = VtSideff ([id], VtLater)
+let seff id = VtSideff ([id.CAst.v], VtLater)
 
 }
 
@@ -303,36 +303,36 @@ let seff id = VtSideff ([id], VtLater)
 END*)
 
 VERNAC COMMAND EXTEND DeriveInversionClear
-| #[ polymorphic; ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
+| #[ polymorphic; ] [ "Derive" "Inversion_clear" identref(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
       add_inversion_lemma_exn ~poly:polymorphic na c s false inv_clear_tac }
 
-| #[ polymorphic; ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na }
+| #[ polymorphic; ] [ "Derive" "Inversion_clear" identref(na) "with" constr(c) ] => { seff na }
   -> {
       add_inversion_lemma_exn ~poly:polymorphic na c Sorts.InProp false inv_clear_tac }
 END
 
 VERNAC COMMAND EXTEND DeriveInversion
-| #[ polymorphic; ] [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
+| #[ polymorphic; ] [ "Derive" "Inversion" identref(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
       add_inversion_lemma_exn ~poly:polymorphic na c s false inv_tac }
 
-| #[ polymorphic; ] [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na }
+| #[ polymorphic; ] [ "Derive" "Inversion" identref(na) "with" constr(c) ] => { seff na }
   -> {
       add_inversion_lemma_exn ~poly:polymorphic na c Sorts.InProp false inv_tac }
 END
 
 VERNAC COMMAND EXTEND DeriveDependentInversion
-| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
+| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion" identref(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
       add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_tac }
 END
 
 VERNAC COMMAND EXTEND DeriveDependentInversionClear
-| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
+| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion_clear" identref(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
       add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_clear_tac }

plugins/ltac/leminv.ml

@@ -229,9 +229,9 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
   let invProof = it_mkNamedLambda_or_LetIn sigma c !ownSign in
   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 cinfo = Declare.CInfo.make ~name ~typ:None () in
+let add_inversion_lemma ~poly (name:lident) env sigma t sort dep inv_op =
+  let invProof, sigma = inversion_scheme ~name:name.v ~poly env sigma t sort dep inv_op in
+  let cinfo = Declare.CInfo.make ?loc:name.loc ~name:name.v ~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

plugins/ltac/leminv.mli

@@ -17,5 +17,5 @@ val lemInv_clause :
   quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
 
 val add_inversion_lemma_exn : poly:bool ->
-  Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) ->
+  lident -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) ->
     unit