From b0612e00b2a905510439d9a6e8908497c1b74c61 Mon Sep 17 00:00:00 2001 From: Andrea Asperti 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