1. ProofEngineHelpers.locate_in_term, ProofEngineHelpers.locate_in_conjecture

[helm.git] / helm / matita / matitaMathView.ml

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index efda8cd7638e209fb4d580a9b6cf2bc9e8484e98..3cb9c8c0b2ba3d4a6ff69dbc11459bd12395d127 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -254,8 +254,12 @@ object (self)
       match term with
       | `Term t ->
           let context' =
+           match
             ProofEngineHelpers.locate_in_conjecture t
               (dummy_goal, context, conclusion)
+           with
+              [context,_] -> context
+            | _ -> assert false (* since it uses physical equality *)
           in
           dummy_goal, context', t
       | `Hyp context -> dummy_goal, context, Cic.Rel 1