Update tutorial plugin to use sigma, in keeping with doc recommendations

3 files changed, 95 insertions, 95 deletions

diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.ml b/doc/plugin_tutorial/tuto3/src/construction_game.ml
index 663113d012..2a2acb6001 100644
--- a/doc/plugin_tutorial/tuto3/src/construction_game.ml
+++ b/doc/plugin_tutorial/tuto3/src/construction_game.ml
@@ -3,15 +3,15 @@ open Context
 
 let find_reference = Coqlib.find_reference [@ocaml.warning "-3"]
 
-let example_sort evd =
+let example_sort sigma =
 (* creating a new sort requires that universes should be recorded
   in the evd datastructure, so this datastructure also needs to be
   passed around. *)
-  let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
+  let sigma, s = Evd.new_sort_variable Evd.univ_rigid sigma in
   let new_type = EConstr.mkSort s in
-  evd, new_type
+  sigma, new_type
 
-let c_one evd =
+let c_one sigma =
 (* 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 =
@@ -19,129 +19,129 @@ let c_one evd =
 (* the long name of "S" was found with the command "About S." *)
   let gr_O =
     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
+  let sigma, c_O = Evarutil.new_global sigma gr_O in
+  let sigma, c_S = Evarutil.new_global sigma gr_S in
 (* Here is the construction of a new term by applying functions to argument. *)
-  evd, EConstr.mkApp (c_S, [| c_O |])
+  sigma, EConstr.mkApp (c_S, [| c_O |])
 
-let dangling_identity env evd =
+let dangling_identity env sigma =
 (* I call this a dangling identity, because it is not polymorph, but
    the type on which it applies is left unspecified, as it is
    represented by an existential variable.  The declaration for this
    existential variable needs to be added in the evd datastructure. *)
-  let evd, type_type = example_sort evd in
-  let evd, arg_type = Evarutil.new_evar env evd type_type in
+  let sigma, type_type = example_sort sigma in
+  let sigma, arg_type = Evarutil.new_evar env sigma type_type in
 (* Notice the use of a De Bruijn index for the inner occurrence of the
   bound variable. *)
-  evd, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type,
+  sigma, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type,
           EConstr.mkRel 1)
 
-let dangling_identity2 env evd =
+let dangling_identity2 env sigma =
 (* This example uses directly a function that produces an evar that
   is meant to be a type. *)
-  let evd, (arg_type, type_type) =
-    Evarutil.new_type_evar env evd Evd.univ_rigid in
-  evd, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type,
+  let sigma, (arg_type, type_type) =
+    Evarutil.new_type_evar env sigma Evd.univ_rigid in
+  sigma, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type,
           EConstr.mkRel 1)
 
 let example_sort_app_lambda () =
     let env = Global.env () in
-    let evd = Evd.from_env env in
-    let evd, c_v = c_one evd in
+    let sigma = Evd.from_env env in
+    let sigma, c_v = c_one sigma in
 (* dangling_identity and dangling_identity2 can be used interchangeably here *)
-    let evd, c_f = dangling_identity2 env evd in
+    let sigma, c_f = dangling_identity2 env sigma in
     let c_1 = EConstr.mkApp (c_f, [| c_v |]) in
     let _ = Feedback.msg_notice
-       (Printer.pr_econstr_env env evd c_1) in
+       (Printer.pr_econstr_env env sigma 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 env evd c_1 in
+    let sigma, the_type = Typing.type_of env sigma 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. *)
     Feedback.msg_notice
-      ((Printer.pr_econstr_env env evd c_1) ++
+      ((Printer.pr_econstr_env env sigma c_1) ++
        str " has type " ++
-       (Printer.pr_econstr_env env evd the_type))
+       (Printer.pr_econstr_env env sigma the_type))
 
 
-let c_S evd =
+let c_S sigma =
   let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_O evd =
+let c_O sigma =
   let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_E evd =
+let c_E sigma =
   let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_D evd =
+let c_D sigma =
   let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_Q evd =
+let c_Q sigma =
   let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_R evd =
+let c_R sigma =
   let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_N evd =
+let c_N sigma =
   let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_C evd =
+let c_C sigma =
   let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "C" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_F evd =
+let c_F sigma =
   let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma gr
 
-let c_P evd =
+let c_P sigma =
   let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in
-  Evarutil.new_global evd gr
+  Evarutil.new_global sigma 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 mk_nat sigma n =
+  let sigma, c_S = c_S sigma in
+  let sigma, c_O = c_O sigma in
   let rec buildup = function
     | 0 -> c_O
     | n -> EConstr.mkApp (c_S, [| buildup (n - 1) |]) in
-  if n <= 0 then evd, c_O else evd, buildup n
+  if n <= 0 then sigma, c_O else sigma, buildup n
 
 let example_classes n =
   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 sigma = Evd.from_env env in
+  let sigma, c_n = mk_nat sigma n in
+  let sigma, n_half = mk_nat sigma (n / 2) in
+  let sigma, c_N = c_N sigma in
+  let sigma, c_div = c_D sigma in
+  let sigma, c_even = c_E sigma in
+  let sigma, c_Q = c_Q sigma in
+  let sigma, c_R = c_R sigma 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 sigma0 = sigma in
+  let sigma, instance = Evarutil.new_evar env sigma arg_type in
   let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in
-  let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in
-  let evd, the_type = Typing.type_of env evd c_half in
-  let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in
+  let _ = Feedback.msg_notice (Printer.pr_econstr_env env sigma c_half) in
+  let sigma, the_type = Typing.type_of env sigma c_half in
+  let _ = Feedback.msg_notice (Printer.pr_econstr_env env sigma c_half) in
   let proved_equality =
     EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.DEFAULTcast,
       EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in
 (* This is where we force the system to compute with type classes. *)
 (* Question to coq developers: why do we pass two evd arguments to
-   solve_remaining_evars? Is the choice of evd0 relevant here? *)
-  let evd = Pretyping.solve_remaining_evars
-    (Pretyping.default_inference_flags true) env evd ~initial:evd0 in
-  let evd, final_type = Typing.type_of env evd proved_equality in
-  Feedback.msg_notice (Printer.pr_econstr_env env evd proved_equality)
+   solve_remaining_evars? Is the choice of sigma0 relevant here? *)
+  let sigma = Pretyping.solve_remaining_evars
+    (Pretyping.default_inference_flags true) env sigma ~initial:sigma0 in
+  let sigma, final_type = Typing.type_of env sigma proved_equality in
+  Feedback.msg_notice (Printer.pr_econstr_env env sigma proved_equality)
 
 (* This function, together with definitions in Data.v, shows how to
    trigger automatic proofs at the time of typechecking, based on
@@ -152,36 +152,36 @@ let example_classes n =
 *)
 let example_canonical n =
   let env = Global.env () in
-  let evd = Evd.from_env env in
+  let sigma = Evd.from_env env in
 (* Construct a natural representation of this integer. *)
-  let evd, c_n = mk_nat evd n in
+  let sigma, c_n = mk_nat sigma n in
 (* terms for "nat", "eq", "S_ev", "eq_refl", "C" *)
-  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
+  let sigma, c_N = c_N sigma in
+  let sigma, c_F = c_F sigma in
+  let sigma, c_R = c_R sigma in
+  let sigma, c_C = c_C sigma in
+  let sigma, c_P = c_P sigma in
 (* the last argument of C *)
   let refl_term = EConstr.mkApp (c_R, [|c_N; c_n |]) 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
+  let sigma, ev1 = Evarutil.new_evar env sigma c_N in
 (* This is the type for the second existential variable *)
   let csev = EConstr.mkApp (c_F, [| ev1 |]) in
-  let evd, ev2 = Evarutil.new_evar env evd csev in
+  let sigma, ev2 = Evarutil.new_evar env sigma csev in
 (* Now we build the C structure. *)
   let test_term = EConstr.mkApp (c_C, [| c_n; ev1; ev2; refl_term |]) in
 (* Type-checking this term will compute values for the existential variables *)
-  let evd, final_type = Typing.type_of env evd test_term in
+  let sigma, final_type = Typing.type_of env sigma test_term in
 (* The computed type has two parameters, the second one is the proof. *)
-  let value = match EConstr.kind evd final_type with
+  let value = match EConstr.kind sigma final_type with
       | Constr.App(_, [| _; the_half |]) -> the_half
       | _ -> failwith "expecting the whole type to be \"cmp _ the_half\"" in
-  let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd value) in
+  let _ = Feedback.msg_notice (Printer.pr_econstr_env env sigma value) in
 (* I wish for a nicer way to get the value of ev2 in the evar_map *)
-  let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in
+  let prf_struct = EConstr.of_constr (EConstr.to_constr sigma ev2) in
   let the_prf = EConstr.mkApp (c_P, [| ev1; prf_struct |]) in
-  let evd, the_statement = Typing.type_of env evd the_prf in
+  let sigma, the_statement = Typing.type_of env sigma the_prf in
   Feedback.msg_notice
-    (Printer.pr_econstr_env env evd the_prf ++ str " has type " ++
-     Printer.pr_econstr_env env evd the_statement)
+    (Printer.pr_econstr_env env sigma the_prf ++ str " has type " ++
+     Printer.pr_econstr_env env sigma the_statement)
diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
index f4d9e7fd5b..14b8eb5f07 100644
--- a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
+++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
@@ -14,13 +14,13 @@ open Stdarg
 VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
 | [ "Tuto3_1" ] ->
   { let env = Global.env () in
-    let evd = Evd.from_env env in
-    let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
+    let sigma = Evd.from_env env in
+    let sigma, s = Evd.new_sort_variable Evd.univ_rigid sigma in
     let new_type_2 = EConstr.mkSort s in
-    let evd, _ =
+    let sigma, _ =
       Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in
     Feedback.msg_notice
-      (Printer.pr_econstr_env env evd new_type_2) }
+      (Printer.pr_econstr_env env sigma new_type_2) }
 END
 
 VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
index 2d541087ce..796a65f40d 100644
--- a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
+++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
@@ -65,10 +65,10 @@ let package i = Goal.enter begin fun gl ->
    and return the value a.  *)
 
 (* Remark by Maxime: look for destApp combinator. *)
-let unpack_type evd term =
+let unpack_type sigma term =
   let report () =
     CErrors.user_err (Pp.str "expecting a packed type") in
-  match EConstr.kind evd term with
+  match EConstr.kind sigma term with
   | Constr.App (_, [| ty |]) -> ty
   | _ -> report ()
 
@@ -76,19 +76,19 @@ let unpack_type evd term =
    A -> pack B -> C and return A, B, C
   but it is not used in the current version of our tactic.
   It is kept as an example. *)
-let two_lambda_pattern evd term =
+let two_lambda_pattern sigma term =
   let report () =
     CErrors.user_err (Pp.str "expecting two nested implications") in
 (* Note that pattern-matching is always done through the EConstr.kind function,
    which only provides one-level deep patterns. *)
-  match EConstr.kind evd term with
+  match EConstr.kind sigma term with
   (* Here we recognize the outer implication *)
   | Constr.Prod (_, ty1, l1) ->
       (* Here we recognize the inner implication *)
-      (match EConstr.kind evd l1 with
+      (match EConstr.kind sigma l1 with
       | Constr.Prod (n2, packed_ty2, deep_conclusion) ->
         (* Here we recognized that the second type is an application *)
-        ty1, unpack_type evd packed_ty2, deep_conclusion
+        ty1, unpack_type sigma packed_ty2, deep_conclusion
       | _ -> report ())
   | _ -> report ()
 
@@ -104,22 +104,22 @@ let get_type_of_hyp env id =
 
 let repackage i h_hyps_id = Goal.enter begin fun gl ->
     let env = Goal.env gl in
-    let evd = Tacmach.New.project gl in
+    let sigma = Tacmach.New.project gl in
     let concl = Tacmach.New.pf_concl gl in
     let (ty1 : EConstr.t) = get_type_of_hyp env i in
     let (packed_ty2 : EConstr.t) = get_type_of_hyp env h_hyps_id in
-    let ty2 = unpack_type evd packed_ty2 in
+    let ty2 = unpack_type sigma packed_ty2 in
     let new_packed_type = EConstr.mkApp (c_P (), [| ty1; ty2 |]) in
     let open EConstr in
     let new_packed_value =
         mkApp (c_R (), [| ty1; ty2; mkVar i;
           mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in
-    Refine.refine ~typecheck:true begin fun evd ->
-      let evd, new_goal = Evarutil.new_evar env evd
+    Refine.refine ~typecheck:true begin fun sigma ->
+      let sigma, new_goal = Evarutil.new_evar env sigma
           (mkArrowR (mkApp(c_H (), [| new_packed_type |]))
              (Vars.lift 1 concl))
       in
-      evd, mkApp (new_goal,
+      sigma, mkApp (new_goal,
                   [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |])
       end
     end