diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 13 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 28 |
4 files changed, 25 insertions, 24 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index fa43536304..889c064b24 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1497,7 +1497,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) Decl_kinds.Finite with | UserError(s,msg) as e -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 9e22ad3063..071599d9c5 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -158,8 +158,8 @@ let build_newrecursive (fun (env,impls) (((_,recname),_),bl,arityc,_) -> let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in - let evdref = ref (Evd.from_env env0) in - let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in + let evd = Evd.from_env env0 in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in let open Context.Named.Declaration in (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) @@ -406,7 +406,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp match fixpoint_exprl with | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - Command.do_definition + ComDefinition.do_definition + ~program_mode:false fname (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); @@ -426,7 +427,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> @@ -616,8 +617,8 @@ and rebuild_nal aux bk bl' nal typ = let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = - let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in + let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in + let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 9e2774ff32..9fcb35f89e 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -889,11 +889,11 @@ let merge_inductive (ind1: inductive) (ind2: inductive) } in *) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) - let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,pl,impls = Command.interp_mutual_inductive indl [] + 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 (* Declare the mutual inductive block with its associated schemes *) - ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) + ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls) (* Find infos on identifier id. *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 766adfc63a..363ad5dfc9 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1427,7 +1427,7 @@ let com_terminate nb_args ctx hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = - let evmap, env = Pfedit.get_current_context () in + let evd, env = Pfedit.get_current_context () in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; @@ -1479,13 +1479,13 @@ let (com_eqn : int -> Id.t -> | ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in - let evmap, env = Pfedit.get_current_context () in - let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in + let evd, env = Pfedit.get_current_context () in + let evd = Evd.from_ctx (Evd.evar_universe_context evd) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in (Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign:(Environ.named_context_val env) - evmap + evd (EConstr.of_constr equation_lemma_type) (Lemmas.mk_hook (fun _ _ -> ())); ignore (by @@ -1528,14 +1528,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let open Constr in let open CVars in let env = Global.env() in - let evd = ref (Evd.from_env env) in - let function_type = interp_type_evars env evd type_of_f in + let evd = Evd.from_env env in + let evd, function_type = interp_type_evars env evd type_of_f in let function_type = EConstr.Unsafe.to_constr function_type in let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) - let ty = interp_type_evars env evd ~impls:rec_impls eq in + let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in let ty = EConstr.Unsafe.to_constr ty in - let evm, nf = Evarutil.nf_evars_and_universes !evd in + let evd, nf = Evarutil.nf_evars_and_universes evd in let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in let function_type = nf function_type in let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in @@ -1560,16 +1560,16 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in + let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res in (* Refresh the global universes, now including those of _F *) - let evm = Evd.from_env (Global.env ()) in + let evd = Evd.from_env (Global.env ()) in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in let relation, evuctx = - interp_constr env_with_pre_rec_args evm r + interp_constr env_with_pre_rec_args evd r in - let evm = Evd.from_ctx evuctx in + let evd = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) @@ -1599,7 +1599,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num and functional_ref = destConst (constr_of_global functional_ref) and eq_ref = destConst (constr_of_global eq_ref) in generate_induction_principle f_ref tcc_lemma_constr - functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation); + functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evd (EConstr.of_constr res)) (EConstr.of_constr relation); Flags.if_verbose msgnl (h 1 (Ppconstr.pr_id function_name ++ spc () ++ str"is defined" )++ fnl () ++ @@ -1618,5 +1618,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num term_id using_lemmas (List.length res_vars) - evm (Lemmas.mk_hook hook)) + evd (Lemmas.mk_hook hook)) () |