got rid of ~status label so that tactics can now be applied partially,

[helm.git] / helm / ocaml / tactics / primitiveTactics.ml

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 55b9d2e420ec8def3d11fd93902dfe1bb320486c..30d08c9bd76f7cdb52758a816c2dd653f422ef68 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -219,13 +219,10 @@ let
           in
            (match ty with
                C.Sort C.Type as s ->
-                let irl =
-                  CicMkImplicit.identity_relocation_list_for_metavariable context
-                in
                  let fresh_meta = !next_fresh_meta in
                  let fresh_meta' = fresh_meta + 1 in
                   next_fresh_meta := !next_fresh_meta + 2 ;
-                  let subst_item = uri,C.Meta (fresh_meta',irl) in
+                  let subst_item = uri,C.Meta (fresh_meta',[]) in
                    newmetasenvfragment :=
                     (fresh_meta,[],C.Sort C.Type) ::
                      (fresh_meta',[],C.Meta (fresh_meta,[])) :: !newmetasenvfragment ;
@@ -253,7 +250,7 @@ let
     new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
 ;;
 
-let apply_tac ~term ~status:(proof, goal) =
+let apply_tac ~term (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
  let module R = CicReduction in
@@ -331,16 +328,16 @@ let apply_tac ~term ~status:(proof, goal) =
 
   (* TODO per implementare i tatticali e' necessario che tutte le tattiche
   sollevino _solamente_ Fail *)
-let apply_tac ~term ~status =
+let apply_tac ~term status =
   try
-    apply_tac ~term ~status
+    apply_tac ~term status
       (* TODO cacciare anche altre eccezioni? *)
   with CicUnification.UnificationFailure _ as e ->
     raise (Fail (Printexc.to_string e))
 
 let intros_tac
  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()
- ~status:(proof, goal)
+ (proof, goal)
 =
  let module C = Cic in
  let module R = CicReduction in
@@ -357,7 +354,7 @@ let intros_tac
 
 let cut_tac
  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
- term ~status:(proof, goal)
+ term (proof, goal)
 =
  let module C = Cic in
   let curi,metasenv,pbo,pty = proof in
@@ -389,7 +386,7 @@ let cut_tac
 
 let letin_tac
  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
- term ~status:(proof, goal)
+ term (proof, goal)
 =
  let module C = Cic in
   let curi,metasenv,pbo,pty = proof in
@@ -413,7 +410,7 @@ let letin_tac
        (newproof, [newmeta])
 
   (** functional part of the "exact" tactic *)
-let exact_tac ~term ~status:(proof, goal) =
+let exact_tac ~term (proof, goal) =
  (* Assumption: the term bo must be closed in the current context *)
  let (_,metasenv,_,_) = proof in
  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
@@ -431,7 +428,7 @@ let exact_tac ~term ~status:(proof, goal) =
 
 (* not really "primitive" tactics .... *)
 
-let elim_tac ~term ~status:(proof, goal) =
+let elim_tac ~term (proof, goal) =
  let module T = CicTypeChecker in
  let module U = UriManager in
  let module R = CicReduction in
@@ -574,7 +571,7 @@ exception NotConvertible
 (*CSC: while [what] can have a richer context (because of binders)           *)
 (*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *)
 (*CSC: Is that evident? Is that right? Or should it be changed?              *)
-let change_tac ~what ~with_what ~status:(proof, goal) =
+let change_tac ~what ~with_what (proof, goal) =
  let curi,metasenv,pbo,pty = proof in
  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   (* are_convertible works only on well-typed terms *)