X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FprimitiveTactics.ml;h=2447fe1ef64d7c10e9ab70d80da9da79d92588f0;hb=6beda5aa100b617b75d88a5a519b5022c99208a0;hp=70502d1b28030650e0540348f5582b9b9ba06369;hpb=eeed0d603ddadba6b5ee5041e87794051b9283dd;p=helm.git

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 70502d1b2..2447fe1ef 100644
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -444,13 +444,13 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
      raise 
        (ProofEngineTypes.Fail (lazy
          "You can't letin a term containing the current goal"));
-    let _,_ =
+    let tty,_ =
       CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
      let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
      let fresh_name =
       mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in
      let context_for_newmeta =
-      (Some (fresh_name,C.Def (term,None)))::context in
+      (Some (fresh_name,C.Def (term,Some tty)))::context in
      let irl =
       CicMkImplicit.identity_relocation_list_for_metavariable
        context_for_newmeta
@@ -517,12 +517,12 @@ let mk_predicate_for_elim
       | _                              -> assert false
    in
 (* let _, upto = PEH.split_with_whd (List.nth splits pred_pos) in *)
-   let rec mk_pred metasenv context' pred arg' = function
+   let rec mk_pred metasenv context' pred arg' cpattern' = function
       | []           -> metasenv, pred, arg'
       | arg :: tail -> 
 (* FG: we find the predicate for the eliminator as in the rewrite tactic ****)
-         let argty, _ugraph = TC.type_of_aux' metasenv context' arg ugraph in
-         let argty = CicReduction.whd context' argty in         
+	 let argty, _ugraph = TC.type_of_aux' metasenv context arg ugraph in
+         let argty = CicReduction.whd context argty in         
 	       let fresh_name = 
             FreshNamesGenerator.mk_fresh_name 
             ~subst:[] metasenv context' C.Anonymous ~typ:argty
@@ -532,7 +532,7 @@ let mk_predicate_for_elim
             let distance  = List.length c - List.length context in
             S.lift distance arg, m, u
          in
-         let pattern = Some lazy_term, [], Some cpattern in
+         let pattern = Some lazy_term, [], Some cpattern' in
          let subst, metasenv, _ugraph, _conjecture, selected_terms =
             ProofEngineHelpers.select
             ~metasenv ~ugraph ~conjecture:(0, context, pred) ~pattern
@@ -545,10 +545,13 @@ let mk_predicate_for_elim
          let pred = PER.replace_with_rel_1_from ~equality:(==) ~what 1 pred in
          let pred = MS.apply_subst subst pred in
          let pred = C.Lambda (fresh_name, argty, pred) in
-         mk_pred metasenv (hyp :: context') pred arg' tail 
+	 let cpattern' = C.Lambda (C.Anonymous, C.Implicit None, cpattern') in
+         mk_pred metasenv (hyp :: context') pred arg' cpattern' tail 
    in
-   let metasenv, pred, arg = mk_pred metasenv context goal arg actual_args in
-   HLog.debug ("PRED: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args));
+   let metasenv, pred, arg = 
+      mk_pred metasenv context goal arg cpattern (List.rev actual_args)
+   in
+   HLog.debug ("PREDICATE: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args));
    metasenv, pred, arg, actual_args
 
 let beta_after_elim_tac upto predicate =