From b0612e00b2a905510439d9a6e8908497c1b74c61 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 29 Nov 2006 08:00:09 +0000
Subject: [PATCH] Demodulate_tac now depends on the universe
---
components/grafite_engine/grafiteEngine.ml | 4 +++-
components/tactics/auto.ml | 7 ++++---
components/tactics/auto.mli | 5 ++++-
components/tactics/tactics.mli | 3 ++-
4 files changed, 13 insertions(+), 6 deletions(-)
diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index a8ee6752c..df01f8467 100644
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -86,7 +86,9 @@ let tactic_of_ast status ast =
let dbd = LibraryDb.instance () in
let mk_fresh_name_callback = namer_of names in
Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
- | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ())
+ | GrafiteAst.Demodulate _ ->
+ Tactics.demodulate
+ ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
| GrafiteAst.Destruct (_,term) -> Tactics.destruct term
| GrafiteAst.Elim (_, what, using, depth, names) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 92d66ef72..3c35013aa 100644
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -1190,14 +1190,14 @@ let eq_of_goal = function
;;
(* DEMODULATE *)
-let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
+let demodulate_tac ~dbd ~universe (proof,goal)=
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let initgoal = [], [], ty in
let eq_uri = eq_of_goal ty in
let (active,passive,bag), cache, maxm =
- init_cache_and_tables dbd true true Universe.empty (proof,goal) in
+ init_cache_and_tables dbd false true universe (proof,goal) in
let equalities = (Saturation.list_of_passive passive) in
(* we demodulate using both actives passives *)
let table =
@@ -1232,7 +1232,8 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
;;
-let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);;
+let demodulate_tac ~dbd ~universe =
+ ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
diff --git a/components/tactics/auto.mli b/components/tactics/auto.mli
index d749a26af..d8efa613e 100644
--- a/components/tactics/auto.mli
+++ b/components/tactics/auto.mli
@@ -37,4 +37,7 @@ val applyS_tac:
universe:Universe.universe ->
ProofEngineTypes.tactic
-val demodulate_tac : dbd:HMysql.dbd -> ProofEngineTypes.tactic
+val demodulate_tac :
+ dbd:HMysql.dbd ->
+ universe:Universe.universe ->
+ ProofEngineTypes.tactic
diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index 3379fbe77..88179e4c8 100644
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -26,7 +26,8 @@ val decompose :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
?user_types:(UriManager.uri * int) list ->
?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
-val demodulate : dbd:HMysql.dbd -> ProofEngineTypes.tactic
+val demodulate : dbd:HMysql.dbd ->
+ universe:Universe.universe -> ProofEngineTypes.tactic
val destruct : term:Cic.term -> ProofEngineTypes.tactic
val elim_intros :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
--
2.39.2