From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 9 Mar 2004 09:52:33 +0000 (+0000)
Subject: Meta no longer raise a failure. Instead they return an empty set of
X-Git-Tag: v0_0_4~31
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=70b2f6a3f29be2e1e898fe7d63bd985a5b31ae35;p=helm.git

Meta no longer raise a failure. Instead they return an empty set of
constraints. This is just a temporary patch. To be understood.
---

diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml
index 7640a6b76..559bee6d9 100644
--- a/helm/ocaml/mathql_generator/cGSearchPattern.ml
+++ b/helm/ocaml/mathql_generator/cGSearchPattern.ml
@@ -100,7 +100,7 @@ let get_constraints term =
             in
             [],[],[!!kind,s']
          | _ -> [],[],[])
-    | C.Meta _
+    | C.Meta _ -> [],[],[] (* ???? To be understood *)
     | C.Implicit _ -> assert false
     | C.Cast (te,_) ->
        (* type ignored *)