huge commit regarding the grafite_status:

[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 a0d8eba48a6b555718c45625968ccc6ddc451666..147df78f857f8be9979772a154a3d1c26af10a39 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -553,3 +553,25 @@ let assert_tac seqs status =
           [merge_tac])
      ) status
 ;;
+
+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
+  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, 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, (t,ty) :: l))
+      (status,[]) l
+  in
+  Paramod.nparamod metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l;      
+    status
+;;
+
+let auto_tac ~params status =
+  distribute_tac (auto ~params) status
+;;