...

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index f9916befc851b48a2eeca70d6aa7d476fc819740..fd383f7c1df778898d153aabca4721e41c7c030a 100644 (file)
--- 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
 ;;