From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 9 Jun 2009 13:17:14 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3899
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f3c6deea5fa1ed58847d7fcdf597193e2c5c7ddb;p=helm.git

...
---

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index f9916befc..fd383f7c1 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -554,11 +554,20 @@ let assert_tac seqs status =
      ) status
 ;;
 
-let auto ~params status goal =
+let auto ~params:(l,_) status goal =
   let gty = get_goalty status goal in
   let n,h,metasenv,subst,o = status.pstatus in
   let status,t = term_of_cic_term status gty (ctx_of gty) in
-    Paramod.nparamod metasenv subst (ctx_of gty) t;      
+  let status, l = 
+    List.fold_left
+      (fun (status, l) t ->
+        let status, t = disambiguate status t None (ctx_of gty) in
+        let status, ty = typeof status (ctx_of t) t in
+        let status, ty = term_of_cic_term status ty (ctx_of ty) in
+        (status, ty :: l))
+      (status,[]) l
+  in
+  Paramod.nparamod metasenv subst (ctx_of gty) t l;      
     status
 ;;