remove uses of Universes.constr_of_global

1 files changed, 71 insertions, 103 deletions

diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index 1bbfc70cb5..e69d65f975 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -8,19 +8,18 @@ let example_sort evd =
   let new_type = EConstr.mkSort s in
   evd, new_type
 
-let c_one () =
-(* What happens in constructing a new natural number from the datatype
-   constructors does not require any handling of existential variables
-   or universes, so evd datastructures don't appear here. *)
+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
 (* the long name of "S" was found with the command "About S." *)
   let gr_O =
     Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
-  let c_O = EConstr.of_constr (Universes.constr_of_global gr_O) in
-  let c_S = EConstr.of_constr (Universes.constr_of_global gr_S) 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. *)
-  EConstr.mkApp (c_S, [| c_O |])
+  evd, EConstr.mkApp (c_S, [| c_O |])
 
 let dangling_identity env evd =
 (* I call this a dangling identity, because it is not polymorph, but
@@ -45,7 +44,7 @@ let dangling_identity2 env evd =
 let example_sort_app_lambda () =
     let env = Global.env () in
     let evd = Evd.from_env env in
-    let c_v = c_one () in
+    let evd, c_v = c_one evd in
 (* dangling_identity and dangling_identity2 can be used interchangeably here *)
     let evd, c_f = dangling_identity2 env evd in
     let c_1 = EConstr.mkApp (c_f, [| c_v |]) in
@@ -53,8 +52,7 @@ let example_sort_app_lambda () =
        (Termops.print_constr_env env evd c_1) in
     (* type verification happens here.  Type verification will update
        existential variable information in the evd part. *)
-    let evd, the_type =
-      Typing.type_of (Global.env()) evd c_1 in
+    let evd, the_type = Typing.type_of env evd c_1 in
 (* At display time, you will notice that the system knows about the
   existential variable being instantiated to the "nat" type, even
   though c_1 still contains the meta-variable. *)
@@ -63,98 +61,68 @@ let example_sort_app_lambda () =
        str " has type " ++
        (Termops.print_constr_env env evd the_type))
 
-let constants = ref ([] : EConstr.t list)
-
-let collect_constants () =
-  if (!constants = []) then
-    let open Coqlib in
-    let open EConstr in
-    let open Universes in
-    let gr_S = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
-    let gr_O = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
-    let gr_E = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in
-    let gr_D = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in
-    let gr_Q = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in
-    let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in
-    let gr_N = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in
-    let gr_C = find_reference "Tuto3" ["Tuto3"; "Data"] "C" in
-    let gr_F = find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in
-    let gr_P = find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in
-    constants := List.map (fun x -> of_constr (constr_of_global x))
-      [gr_S; gr_O; gr_E; gr_D; gr_Q; gr_R; gr_N; gr_C; gr_F; gr_P];
-    !constants
-  else
-    !constants
-
-let c_S () =
-  match collect_constants () with
-    it :: _ -> it
-  | _ -> failwith "could not obtain an internal representation of S : nat"
-
-let c_O () =
-  match collect_constants () with
-    _ :: it :: _ -> it
-  | _ -> failwith "could not obtain an internal representation of 0 : nat"
-
-let c_E () =
-  match collect_constants () with
-    _ :: _ :: it :: _ -> it
-  | _ -> failwith "could not obtain an internal representation of EvenNat"
-
-let c_D () =
-  match collect_constants () with
-    _ :: _ :: _ :: it :: _ -> it
-  | _ -> failwith "could not obtain an internal representation of tuto_div2"
-
-let c_Q () =
-  match collect_constants () with
-    _ :: _ :: _ :: _ :: it :: _ -> it
-  | _ -> failwith "could not obtain an internal representation of eq"
-
-let c_R () =
-  match collect_constants () with
-    _ :: _ :: _ :: _ :: _ :: it :: _ -> it
-  | _ -> failwith "could not obtain an internal representation of eq_refl"
-
-let c_N () =
-  match collect_constants () with
-    _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
-  | _ -> failwith "could not obtain an internal representation of nat"
-
-let c_C () =
-  match collect_constants () with
-    _ :: _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
-  | _ -> failwith "could not obtain an internal representation of cmp"
-
-let c_F () =
-  match collect_constants () with
-    _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
-  | _ -> failwith "could not obtain an internal representation of S_ev"
-
-let c_P () =
-  match collect_constants () with
-    _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
-  | _ -> failwith "could not obtain an internal representation of s_half_proof"
-
-let mk_nat n =
-  let c_S = c_S () in
-  let c_O = c_O () in
+
+let c_S evd =
+  let gr = Coqlib.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
+  Evarutil.new_global evd gr
+
+let c_E evd =
+  let gr = Coqlib.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
+  Evarutil.new_global evd gr
+
+let c_Q evd =
+  let gr = Coqlib.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
+  Evarutil.new_global evd gr
+
+let c_N evd =
+  let gr = Coqlib.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
+  Evarutil.new_global evd gr
+
+let c_F evd =
+  let gr = Coqlib.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
+  Evarutil.new_global evd gr
+
+(* If c_S was universe polymorphic, we should have created a new constant
+   at each iteration of buildup. *)
+let mk_nat evd n =
+  let evd, c_S = c_S evd in
+  let evd, c_O = c_O evd in
   let rec buildup = function
     | 0 -> c_O
     | n -> EConstr.mkApp (c_S, [| buildup (n - 1) |]) in
-  if n <= 0 then c_O else buildup n
+  if n <= 0 then evd, c_O else evd, buildup n
 
 let example_classes n =
-  let c_n = mk_nat n in
-  let n_half = mk_nat (n / 2) in
-  let c_N = c_N () in
-  let c_div = c_D () in
-  let c_even = c_E () in
-  let c_Q = c_Q () in
-  let c_R = c_R () in
-  let arg_type = EConstr.mkApp (c_even, [| c_n |]) in
   let env = Global.env () in
   let evd = Evd.from_env env in
+  let evd, c_n = mk_nat evd n in
+  let evd, n_half = mk_nat evd (n / 2) in
+  let evd, c_N = c_N evd in
+  let evd, c_div = c_D evd in
+  let evd, c_even = c_E evd in
+  let evd, c_Q = c_Q evd in
+  let evd, c_R = c_R evd in
+  let arg_type = EConstr.mkApp (c_even, [| c_n |]) in
   let evd0 = evd in
   let evd, instance = Evarutil.new_evar env evd arg_type in
   let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in
@@ -180,18 +148,18 @@ let example_classes n =
    this half is indeed the half)
 *)
 let example_canonical n =
+  let env = Global.env () in
+  let evd = Evd.from_env env in
 (* Construct a natural representation of this integer. *)
-  let c_n = mk_nat n in
+  let evd, c_n = mk_nat evd n in
 (* terms for "nat", "eq", "S_ev", "eq_refl", "C" *)
-  let c_N = c_N () in
-  let c_F = c_F () in
-  let c_R = c_R () in
-  let c_C = c_C () in
-  let c_P = c_P () in
+  let evd, c_N = c_N evd in
+  let evd, c_F = c_F evd in
+  let evd, c_R = c_R evd in
+  let evd, c_C = c_C evd in
+  let evd, c_P = c_P evd in
 (* the last argument of C *)
   let refl_term = EConstr.mkApp (c_R, [|c_N; c_n |]) in
-  let env = Global.env () in
-  let evd = Evd.from_env env in
 (* Now we build two existential variables, for the value of the half and for
    the "S_ev" structure that triggers the proof search. *)
   let evd, ev1 = Evarutil.new_evar env evd c_N in