Pretty-printing of "match ... with" pattern syntax fixed. We need an

[helm.git] / components / tactics / proofEngineHelpers.ml

diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml
index fa5c77d7170928091cbd50a29917b9fc40ec883c..b5db34d17c8b852bdd2ca9988f10dd46feb4ed0b 100644 (file)
--- a/components/tactics/proofEngineHelpers.ml
+++ b/components/tactics/proofEngineHelpers.ml
@@ -363,25 +363,25 @@ let pattern_of ?(equality=(==)) ~term terms =
         if b1||b2 then true,Cic.Cast (te, ty)
         else
          not_found
-    | Cic.Prod (name, s, t) ->
+    | Cic.Prod (_, s, t) ->
        let b1,s = aux s in
        let b2,t = aux t in
         if b1||b2 then
-         true, Cic.Prod (name, s, t)
+         true, Cic.Prod (Cic.Anonymous, s, t)
         else
          not_found
-    | Cic.Lambda (name, s, t) ->
+    | Cic.Lambda (_, s, t) ->
        let b1,s = aux s in
        let b2,t = aux t in
         if b1||b2 then
-         true, Cic.Lambda (name, s, t)
+         true, Cic.Lambda (Cic.Anonymous, s, t)
         else
          not_found
-    | Cic.LetIn (name, s, t) ->
+    | Cic.LetIn (_, s, t) ->
        let b1,s = aux s in
        let b2,t = aux t in
         if b1||b2 then
-         true, Cic.LetIn (name, s, t)
+         true, Cic.LetIn (Cic.Anonymous, s, t)
         else
          not_found
     | Cic.Appl terms ->