X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=7a732a57257304dd89835b7e31aac819f047bea2;hb=0c8963a0f3aef05cf4866e8bcd3fdbebddac8b87;hp=96ff130c5c8b5499d37220135dbd5a171f51badd;hpb=dbe5d5ee749b3d5d36c91f96b73d7554967fc8cd;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 96ff130c5..7a732a572 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 open ProofEngineHelpers
 open ProofEngineTypes
 
@@ -152,7 +154,12 @@ let classify_metas newmeta in_subst_domain subst_in metasenv =
             | Some (n,Cic.Def (s,None)) ->
                Some (n,Cic.Def ((subst_in canonical_context' s),None))
             | None -> None
-            | Some (_,Cic.Def (_,Some _)) -> assert false
+            | Some (n,Cic.Def (bo,Some ty)) ->
+               Some
+                (n,
+                  Cic.Def
+                   (subst_in canonical_context' bo,
+                    Some (subst_in canonical_context' ty)))
           in
            entry'::canonical_context'
         ) canonical_context []