From 93273e29708ff5c24024bde0e4b9955cb94a0dc0 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Thu, 3 May 2018 22:57:55 +0200
Subject: little cleanup on the defining command, and question in comments

---
 tuto1/src/simple_declare.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index 932c4c9bb3..4740de435f 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -4,18 +4,22 @@ let packed_declare_definition ident
     let evalue, st = value_with_constraints in
     let evd = Evd.from_ctx st in
     let value = EConstr.to_constr evd evalue in
+(* Question to developers: could the next 3 lines be removed:
+   similar stuff present in comDefinition and elpi, but not in Mtac2 *)
     let evd = Evd.minimize_universes evd in
     let used = Univops.universes_of_constr (Global.env()) value in
-    let norm_used = Evd.restrict_universe_context evd used in
+    let evd = Evd.restrict_universe_context evd used in
     let decl = Univdecls.default_univ_decl in
-    let uctx = Evd.check_univ_decl ~poly:true norm_used decl in
+    let uctx = Evd.check_univ_decl ~poly:true evd decl in
     let ce = Declare.definition_entry ~univs:uctx value in
     let _  =
-      Pretyping.check_evars_are_solved (Global.env ()) norm_used Evd.empty in
+      Pretyping.check_evars_are_solved (Global.env ()) evd Evd.empty in
     let k = (Decl_kinds.Global,
              true (* polymorphic *), Decl_kinds.Definition) in
     let binders = Evd.universe_binders evd in
     let implicits = [] in
     let hook = Lemmas.mk_hook (fun _ x -> x) in
     ignore(DeclareDef.declare_definition ident k ce binders implicits hook)
-  end
\ No newline at end of file
+  end
+
+(* But this definition cannot be undone by Reset ident *)
\ No newline at end of file
-- 
cgit v1.2.3