Active goals are now demodulated after selecting a positive clause.

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index fd383f7c1df778898d153aabca4721e41c7c030a..147df78f857f8be9979772a154a3d1c26af10a39 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -563,11 +563,12 @@ let auto ~params:(l,_) status goal =
       (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, t =  term_of_cic_term status t (ctx_of gty) in
         let status, ty = term_of_cic_term status ty (ctx_of ty) in
-        (status, ty :: l))
+        (status, (t,ty) :: l))
       (status,[]) l
   in
-  Paramod.nparamod metasenv subst (ctx_of gty) t l;      
+  Paramod.nparamod metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l;      
     status
 ;;