diff options
| author | Emilio Jesus Gallego Arias | 2020-04-11 17:14:38 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-15 11:12:53 -0400 |
| commit | 1dc70876b4a5ad027b3b73aa6ba741e89320d17d (patch) | |
| tree | 13a69ee4c6d0bf42219fef0f090195c3082449f4 /plugins/funind | |
| parent | e262a6262ebb6c3010cb58e96839b0e3d66e09ac (diff) | |
[declare] Rename `Declare.t` to `Declare.Proof.t`
This still needs API cleanup but we defer it to the moment we are
ready to make the internals private.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/recdef.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 51d3286715..ffb9a7e69b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -27,7 +27,6 @@ open Tacticals open Tacmach open Tactics open Nametab -open Declare open Tacred open Glob_term open Pretyping @@ -54,8 +53,9 @@ let find_reference sl s = locate (make_qualid dp (Id.of_string s)) let declare_fun name kind ?univs value = - let ce = definition_entry ?univs value (*FIXME *) in - GlobRef.ConstRef (declare_constant ~name ~kind (DefinitionEntry ce)) + let ce = Declare.definition_entry ?univs value (*FIXME *) in + GlobRef.ConstRef + (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce)) let defined lemma = Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None @@ -1336,7 +1336,7 @@ let whole_start concl_tac nb_args is_mes func input_type relation rec_arg_num : g let get_current_subgoals_types pstate = - let p = Declare.get_proof pstate in + let p = Declare.Proof.get_proof pstate in let Proof.{goals = sgs; sigma; _} = Proof.data p in (sigma, List.map (Goal.V82.abstract_type sigma) sgs) @@ -1416,7 +1416,7 @@ let is_opaque_constant c = let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type, decompose_and_tac, nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) - let current_proof_name = Lemmas.pf_fold Declare.get_proof_name lemma in + let current_proof_name = Lemmas.pf_fold Declare.Proof.get_proof_name lemma in let name = match goal_name with | Some s -> s @@ -1514,7 +1514,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name g)) lemma in - if Lemmas.(pf_fold Declare.get_open_goals) lemma = 0 then ( + if Lemmas.(pf_fold Declare.Proof.get_open_goals) lemma = 0 then ( defined lemma; None ) else Some lemma |