decompose construction of typed term containing evars

1 files changed, 24 insertions, 16 deletions

diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
index fbd93e593c..aaeabcf34f 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.ml4
@@ -5,33 +5,41 @@ open Pp
 (* This one is necessary, to avoid message about missing wit_string *)
 open Stdarg
 
-VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
+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 new_type_2 = EConstr.mkSort s in
+    let evd, _ =
+      Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in
+    Feedback.msg_notice
+      (Termops.print_constr_env env evd new_type_2) ]
+END
+
+VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
+| [ "Tuto3_2" ] ->
   [ 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_S = EConstr.of_constr (Universes.constr_of_global gr_S) in
     let c_O = EConstr.of_constr (Universes.constr_of_global gr_O) in
-    let c_v = EConstr.mkApp (c_S, [| c_O |]) in
     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 new_type_2 = Constr.mkSort s in
-    let evd, bare_evar = Evd.new_evar evd
-        (Evd.make_evar (Environ.named_context_val env) new_type_2) in
-    let arg_type = EConstr.mkEvar (bare_evar, [| |]) in
+    let new_type_2 = EConstr.mkSort s in
+    let evd, arg_type = Evarutil.new_evar env evd new_type_2 in
     let c_f =
        EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
           EConstr.mkRel 1) in
-    let c_1 = EConstr.mkApp (c_f, [| c_v |]) in
-    (* type verification happens here.  In this case, we don't care about
-       the type, but usually, typing will update existential variables and
-       universes, all this being stored in the new "evar_map" object *)
-    let evd, _ =
-      Typing.type_of (Global.env()) (Evd.from_env (Global.env())) c_1 in
-    ()
-(*    Feedback.msg_notice
-      (Termops.print_constr_env (Global.env()) evd c_1) *) ]
+    let c_1 = EConstr.mkApp (c_f, [| c_O |]) 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
+    Feedback.msg_notice
+      ((Termops.print_constr_env env evd c_1) ++
+       str " has type " ++
+       (Termops.print_constr_env env evd the_type)) ]
 END