diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 8 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
4 files changed, 9 insertions, 9 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 87609296bc..2fd6f53c4a 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)) + (Vernacexpr.(VernacExpr(VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 889c064b24..b4e17c5d1c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1498,7 +1498,7 @@ let do_build_inductive try with_full_print (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) - Decl_kinds.Finite + Declarations.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in @@ -1509,7 +1509,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ msg in @@ -1524,7 +1524,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 9fcb35f89e..8f5d3f22f4 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -20,10 +20,10 @@ open Names open Term open Constr open Vars -open Declarations open Glob_term open Glob_termops open Decl_kinds +open Declarations open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -353,8 +353,8 @@ let ind2name = Id.of_string "__ind2" be co-inductive, and for the moment they must not be mutual either. *) let verify_inds mib1 mib2 = - if mib1.mind_finite == Decl_kinds.CoFinite then error "First argument is coinductive"; - if mib2.mind_finite == Decl_kinds.CoFinite then error "Second argument is coinductive"; + if mib1.mind_finite == CoFinite then error "First argument is coinductive"; + if mib2.mind_finite == CoFinite then error "Second argument is coinductive"; if not (Int.equal mib1.mind_ntypes 1) then error "First argument is mutual"; if not (Int.equal mib2.mind_ntypes 1) then error "Second argument is mutual"; () @@ -891,7 +891,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) (* Declare inductive *) let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in let mie,pl,impls = ComInductive.interp_mutual_inductive indl [] - false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in + false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 363ad5dfc9..8fe05b4978 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -861,7 +861,7 @@ let rec prove_le g = | App (c, [| x0 ; _ |]) -> EConstr.isVar sigma x0 && Id.equal (destVar sigma x0) (destVar sigma x) && - is_global sigma (le ()) c + EConstr.is_global sigma (le ()) c | _ -> false in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) |