Bug fixed in generalization: the goals opened by lazy parsing of the

[helm.git] / helm / ocaml / content_pres / termContentPres.ml

diff --git a/helm/ocaml/content_pres/termContentPres.ml b/helm/ocaml/content_pres/termContentPres.ml
index 3236fb43357068afd584d5c929da3a1274e48079..4c8bbc7d4e4af42ff8defbee358438dd0f139cf5 100644 (file)
--- a/helm/ocaml/content_pres/termContentPres.ml
+++ b/helm/ocaml/content_pres/termContentPres.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 module Ast = CicNotationPt
@@ -289,7 +291,7 @@ let instantiate21 idrefs env l1 =
         Ast.AttributedTerm (attr, subst_singleton pos env t)
     | t -> CicNotationUtil.group (subst pos env t)
   and subst pos env = function
-    | Ast.AttributedTerm (attr, t) as term ->
+    | Ast.AttributedTerm (attr, t) ->
 (*         prerr_endline ("loosing attribute " ^ CicNotationPp.pp_attribute attr); *)
         subst pos env t
     | Ast.Variable var ->