X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineHelpers.ml;h=b38512273081907ab6cff86c16cd56f35be304a1;hb=8da8820a77f2104dd1bf17c01fa77f75ee31c8fb;hp=fa5c77d7170928091cbd50a29917b9fc40ec883c;hpb=3e25c8d9f6e7802a2fc28697795b9128af731494;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml
index fa5c77d71..b38512273 100644
--- a/helm/software/components/tactics/proofEngineHelpers.ml
+++ b/helm/software/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 ->
@@ -706,4 +706,3 @@ let relations_of_menv m c =
 let sort_metasenv (m : Cic.metasenv) =
   (MS.topological_sort m (relations_of_menv m) : Cic.metasenv)
 ;;
-