From: Stefano Zacchiroli Date: Wed, 27 Apr 2005 17:02:06 +0000 (+0000) Subject: ported to svn-cvs merge X-Git-Tag: after_svn_merge~4 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=06eea22fd7bfe29d103decac4dddce899cd20fbd;p=helm.git ported to svn-cvs merge --- diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 8bc736bea..d28c5220f 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -1,6 +1,6 @@ termEditor.cmi: disambiguatingParser.cmi texTermEditor.cmi: disambiguatingParser.cmi -invokeTactics.cmi: termEditor.cmi termViewer.cmi +invokeTactics.cmi: termViewer.cmi termEditor.cmi hbugs.cmi: invokeTactics.cmi chosenTermEditor.cmi: disambiguatingParser.cmi proofEngine.cmo: proofEngine.cmi @@ -13,26 +13,28 @@ termEditor.cmo: disambiguatingParser.cmi termEditor.cmi termEditor.cmx: disambiguatingParser.cmx termEditor.cmi texTermEditor.cmo: disambiguatingParser.cmi texTermEditor.cmi texTermEditor.cmx: disambiguatingParser.cmx texTermEditor.cmi +chosenTransformer.cmo: chosenTransformer.cmi +chosenTransformer.cmx: chosenTransformer.cmi termViewer.cmo: logicalOperations.cmi termViewer.cmi termViewer.cmx: logicalOperations.cmx termViewer.cmi -invokeTactics.cmo: logicalOperations.cmi proofEngine.cmi termEditor.cmi \ - termViewer.cmi invokeTactics.cmi -invokeTactics.cmx: logicalOperations.cmx proofEngine.cmx termEditor.cmx \ - termViewer.cmx invokeTactics.cmi -hbugs.cmo: invokeTactics.cmi proofEngine.cmi hbugs.cmi -hbugs.cmx: invokeTactics.cmx proofEngine.cmx hbugs.cmi +invokeTactics.cmo: termViewer.cmi termEditor.cmi proofEngine.cmi \ + logicalOperations.cmi invokeTactics.cmi +invokeTactics.cmx: termViewer.cmx termEditor.cmx proofEngine.cmx \ + logicalOperations.cmx invokeTactics.cmi +hbugs.cmo: proofEngine.cmi invokeTactics.cmi hbugs.cmi +hbugs.cmx: proofEngine.cmx invokeTactics.cmx hbugs.cmi chosenTermEditor.cmo: termEditor.cmi chosenTermEditor.cmi chosenTermEditor.cmx: termEditor.cmx chosenTermEditor.cmi helmGtkLogger.cmo: helmGtkLogger.cmi helmGtkLogger.cmx: helmGtkLogger.cmi -gTopLevel.cmo: chosenTermEditor.cmi disambiguatingParser.cmi hbugs.cmi \ - helmGtkLogger.cmi invokeTactics.cmi logicalOperations.cmi proofEngine.cmi \ - termEditor.cmi termViewer.cmi -gTopLevel.cmx: chosenTermEditor.cmx disambiguatingParser.cmx hbugs.cmx \ - helmGtkLogger.cmx invokeTactics.cmx logicalOperations.cmx proofEngine.cmx \ - termEditor.cmx termViewer.cmx -regtest.cmo: batchParser.cmi disambiguatingParser.cmi -regtest.cmx: batchParser.cmx disambiguatingParser.cmx +gTopLevel.cmo: termViewer.cmi termEditor.cmi proofEngine.cmi \ + logicalOperations.cmi invokeTactics.cmi helmGtkLogger.cmi hbugs.cmi \ + disambiguatingParser.cmi chosenTermEditor.cmi +gTopLevel.cmx: termViewer.cmx termEditor.cmx proofEngine.cmx \ + logicalOperations.cmx invokeTactics.cmx helmGtkLogger.cmx hbugs.cmx \ + disambiguatingParser.cmx chosenTermEditor.cmx +regtest.cmo: disambiguatingParser.cmi batchParser.cmi +regtest.cmx: disambiguatingParser.cmx batchParser.cmx testlibrary.cmo: batchParser.cmi testlibrary.cmx: batchParser.cmx batchParser.cmo: disambiguatingParser.cmi batchParser.cmi diff --git a/helm/gTopLevel/disambiguatingParser.mli b/helm/gTopLevel/disambiguatingParser.mli index 3d2c91f25..710401f4a 100644 --- a/helm/gTopLevel/disambiguatingParser.mli +++ b/helm/gTopLevel/disambiguatingParser.mli @@ -37,11 +37,11 @@ module Make (C : DisambiguateTypes.Callbacks) : sig val disambiguate_term : dbd:Mysql.dbd -> - Cic.context -> - Cic.metasenv -> - string -> - EnvironmentP3.t -> (* previous interpretation status *) + context:Cic.context -> + metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> + aliases:EnvironmentP3.t -> (* previous interpretation status *) + string -> (EnvironmentP3.t * (* new interpretation status *) Cic.metasenv * (* new metasenv *) Cic.term * diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml index 4cca70221..1b9986caa 100644 --- a/helm/gTopLevel/termEditor.ml +++ b/helm/gTopLevel/termEditor.ml @@ -101,9 +101,9 @@ module Make(C:DisambiguateTypes.Callbacks) = in let environment',metasenv,expr,ugraph = match - Disambiguate'.disambiguate_term ~dbd context metasenv + Disambiguate'.disambiguate_term ~dbd ~context ~metasenv (input#buffer#get_text ()) ~initial_ugraph:CicUniv.empty_ugraph - !environment + ~aliases:!environment with [environment',metasenv,expr,u] -> environment',metasenv,expr,u | _ -> assert false diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml index a59fb3489..5ea965f2f 100644 --- a/helm/gTopLevel/texTermEditor.ml +++ b/helm/gTopLevel/texTermEditor.ml @@ -221,8 +221,8 @@ module Make(C:DisambiguateTypes.Callbacks) = let environment',metasenv,expr,ugraph = match Disambiguate'.disambiguate_term ~dbd - context metasenv (Mathml_editor.get_tex tex_editor) - ~initial_ugraph:CicUniv.empty_ugraph !environment + ~context ~metasenv (Mathml_editor.get_tex tex_editor) + ~initial_ugraph:CicUniv.empty_ugraph ~aliases:!environment with [environment',metasenv,expr,u] -> environment',metasenv,expr,u | _ -> assert false