From 47e5f716f7ded0eec43b00d49955d56c370c3596 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 8 Jun 2008 16:13:37 +0000
Subject: - Extension de "generalize" en "generalize c as id at occs". - Ajout
 clause "in" à "remember" (et passage du code en ML). - Ajout clause "in" à
 "induction"/"destruct" qui, en ce cas, ajoute   aussi une égalité pour se
 souvenir du terme sur lequel l'induction   ou l'analyse de cas s'applique. -
 Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de   Programs
 qui avait la sémantique de "pose proof" tandis que le nouveau   a la même
 sémantique que "pose (id:=t)"). - Un peu de réorganisation, uniformisation de
 noms dans Arith, et   ajout EqNat dans Arith. - Documentation tactiques et
 notations de tactiques.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/coqlib.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 73614797a7..ecc48dfe29 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -102,7 +102,8 @@ let init_id = id_of_string "Init"
 let arith_id = id_of_string "Arith"
 let datatypes_id = id_of_string "Datatypes"
 
-let logic_module = make_dir ["Coq";"Init";"Logic"]
+let logic_module_name = ["Coq";"Init";"Logic"]
+let logic_module = make_dir logic_module_name
 let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"]
 let datatypes_module = make_dir ["Coq";"Init";"Datatypes"]
 let arith_module = make_dir ["Coq";"Arith";"Arith"]
@@ -202,7 +203,8 @@ let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal"
 let coq_eq_sym  = lazy_init_constant ["Logic"] "sym_eq"
 let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2"
 
-let build_coq_eq_data () = {
+let build_coq_eq_data () =
+  let _ = check_required_library logic_module_name in {
   eq = Lazy.force coq_eq_eq;
   refl = Lazy.force coq_eq_refl;
   ind = Lazy.force coq_eq_ind;
-- 
cgit v1.2.3