From f3c6deea5fa1ed58847d7fcdf597193e2c5c7ddb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 9 Jun 2009 13:17:14 +0000 Subject: [PATCH] ... --- helm/software/components/ng_tactics/nTactics.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) 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 ;; -- 2.39.2