X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=ca6b0e58234d59737de1c71660887231e51ee9d6;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=d26221d3951bac5c6e82bf3437ffbaf3fba6477c;hpb=8b55faddb06e3c4b0a13839210bb49170939b33e;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index d26221d39..ca6b0e582 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -152,7 +152,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 []
@@ -517,10 +522,8 @@ let elim_tac ~term =
           in
            C.Appl (eliminator_ref :: make_tl term (args_no - 1))
          in
-          let metasenv', term_to_refine' =
-           CicMkImplicit.expand_implicits metasenv' [] context term_to_refine in
           let refined_term,_,metasenv'',_ = 
-           CicRefine.type_of_aux' metasenv' context term_to_refine' 
+           CicRefine.type_of_aux' metasenv' context term_to_refine
              CicUniv.empty_ugraph
           in
            let new_goals =