diff options
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/hipattern.ml | 2 | ||||
-rw-r--r-- | tactics/leminv.ml | 7 | ||||
-rw-r--r-- | tactics/leminv.mli | 2 | ||||
-rw-r--r-- | tactics/tactics.ml | 2 |
4 files changed, 6 insertions, 7 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 2c8ca1972..a3a3e0a9e 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -48,7 +48,7 @@ let match_with_non_recursive_type sigma t = let (hdapp,args) = decompose_app sigma t in (match EConstr.kind sigma hdapp with | Ind (ind,u) -> - if (Global.lookup_mind (fst ind)).mind_finite == Decl_kinds.CoFinite then + if (Global.lookup_mind (fst ind)).mind_finite == CoFinite then Some (hdapp,args) else None diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 01065868d..197b3030d 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -234,10 +234,9 @@ let inversion_scheme env sigma t sort dep_option inv_op = let p = Evarutil.nf_evars_universes sigma invProof in p, sigma -let add_inversion_lemma name env sigma t sort dep inv_op = +let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in let univs = - let poly = Flags.use_polymorphic_flag () in Evd.const_univ_entry ~poly sigma in let entry = definition_entry ~univs invProof in @@ -247,13 +246,13 @@ let add_inversion_lemma name env sigma t sort dep inv_op = (* inv_op = Inv (derives de complete inv. lemma) * inv_op = InvNoThining (derives de semi inversion lemma) *) -let add_inversion_lemma_exn na com comsort bool tac = +let add_inversion_lemma_exn ~poly na com comsort bool tac = let env = Global.env () in let sigma = Evd.from_env env in let sigma, c = Constrintern.interp_type_evars env sigma com in let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in try - add_inversion_lemma na env sigma c sort bool tac + 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 diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 8745ad397..f221b1fd9 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -14,6 +14,6 @@ open Misctypes val lemInv_clause : quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic -val add_inversion_lemma_exn : +val add_inversion_lemma_exn : poly:bool -> Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) -> unit diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 508040ec1..4ee0a8a7b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1492,7 +1492,7 @@ let simplest_ecase c = general_case_analysis true None (c,NoBindings) exception IsNonrec -let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Decl_kinds.BiFinite +let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite let find_ind_eliminator ind s gl = let gr = lookup_eliminator ind s in |