From 8801a2304d54e687dafc8614af38f69ada2cbee1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 7 Jan 2019 14:09:58 +0100 Subject: plugin_tutorial: ignore Coqlib.find_reference deprecation warning. Not sure what the right solution is here, but we can improve after the merge. --- doc/plugin_tutorial/tuto3/src/construction_game.ml | 26 ++++++++++++---------- doc/plugin_tutorial/tuto3/src/tuto_tactic.ml | 2 +- 2 files changed, 15 insertions(+), 13 deletions(-) (limited to 'doc/plugin_tutorial/tuto3') diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.ml b/doc/plugin_tutorial/tuto3/src/construction_game.ml index 22b02f6893..9d9f894e18 100644 --- a/doc/plugin_tutorial/tuto3/src/construction_game.ml +++ b/doc/plugin_tutorial/tuto3/src/construction_game.ml @@ -1,5 +1,7 @@ open Pp +let find_reference = Coqlib.find_reference [@ocaml.warning "-3"] + let example_sort evd = (* creating a new sort requires that universes should be recorded in the evd datastructure, so this datastructure also needs to be @@ -12,10 +14,10 @@ let c_one evd = (* In the general case, global references may refer to universe polymorphic objects, and their universe has to be made afresh when creating an instance. *) let gr_S = - Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in + find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in (* the long name of "S" was found with the command "About S." *) let gr_O = - Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in + find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in let evd, c_O = Evarutil.new_global evd gr_O in let evd, c_S = Evarutil.new_global evd gr_S in (* Here is the construction of a new term by applying functions to argument. *) @@ -63,43 +65,43 @@ let example_sort_app_lambda () = let c_S evd = - let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in Evarutil.new_global evd gr let c_O evd = - let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in Evarutil.new_global evd gr let c_E evd = - let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in Evarutil.new_global evd gr let c_D evd = - let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in Evarutil.new_global evd gr let c_Q evd = - let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in Evarutil.new_global evd gr let c_R evd = - let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in Evarutil.new_global evd gr let c_N evd = - let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in Evarutil.new_global evd gr let c_C evd = - let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "C" in + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "C" in Evarutil.new_global evd gr let c_F evd = - let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in Evarutil.new_global evd gr let c_P evd = - let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in Evarutil.new_global evd gr (* If c_S was universe polymorphic, we should have created a new constant diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml index 9818867621..8f2c387d09 100644 --- a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml +++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml @@ -7,9 +7,9 @@ let constants = ref ([] : EConstr.t list) c_U *) let collect_constants () = if (!constants = []) then - let open Coqlib in let open EConstr in let open UnivGen in + let find_reference = Coqlib.find_reference [@ocaml.warning "-3"] in let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "pack" in let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "packer" in let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in -- cgit v1.2.3 From cb2ee2d949899a897022894b750afd1f3d2eb478 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 5 Nov 2018 19:37:11 +0100 Subject: Integrate plugin tutorial after code import --- doc/plugin_tutorial/tuto3/theories/Data.v | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'doc/plugin_tutorial/tuto3') diff --git a/doc/plugin_tutorial/tuto3/theories/Data.v b/doc/plugin_tutorial/tuto3/theories/Data.v index 0b07fee4f2..f7395d686b 100644 --- a/doc/plugin_tutorial/tuto3/theories/Data.v +++ b/doc/plugin_tutorial/tuto3/theories/Data.v @@ -1,4 +1,4 @@ -Require Import ArithRing. + Inductive pack (A: Type) : Type := packer : A -> pack A. @@ -18,7 +18,11 @@ Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}. Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}. Lemma even_rec n h : 2 * h = n -> 2 * S h = S (S n). -Proof. intros H; ring [H]. Qed. +Proof. + intros []. + simpl. rewrite <-plus_n_O, <-plus_n_Sm. + reflexivity. +Qed. Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) := {half := S (@half _ p); half_prop := even_rec n (@half _ p) (@half_prop _ p)}. @@ -51,7 +55,8 @@ Canonical Structure can_ev0 : S_ev 0 := Lemma can_ev_rec n : forall (s : S_ev n), S_ev (S n). Proof. intros s; exists (S (S (double_of _ s))). -destruct s as [a P]. simpl. ring [P]. +destruct s as [a P]. +exact (even_rec _ _ P). Defined. Canonical Structure can_ev_rec. -- cgit v1.2.3