Patches to generate ?1 : ?2 : Type in place of ?1 : Type removed.

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 5909075d82f7aaf395d41ff5be5a2b2e4f887cc0..812094d5a41f24f603bbf7a3c86a922a08761af8 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -160,6 +160,7 @@ let new_metasenv_for_apply newmeta proof context ty =
   let rec aux newmeta =
    function
       C.Cast (he,_) -> aux newmeta he
+(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type
       (* If the expected type is a Type, then also Set is OK ==>
       *  we accept any term of type Type *)
       (*CSC: BUG HERE: in this way it is possible for the term of
@@ -175,6 +176,7 @@ let new_metasenv_for_apply newmeta proof context ty =
           res,
            (newmeta,[],s)::(newmeta+1,context,C.Meta (newmeta,[]))::newmetasenv,
            newargument::arguments,lastmeta
+*)
     | C.Prod (name,s,t) ->
        let irl =
          CicMkImplicit.identity_relocation_list_for_metavariable context
@@ -217,6 +219,7 @@ let
                CicSubstitution.subst_vars !exp_named_subst_diff ty
             | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
           in
+(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type
            (match ty with
                C.Sort C.Type as s ->
                  let fresh_meta = !next_fresh_meta in
@@ -229,6 +232,7 @@ let
                    exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ;
                    subst_item::(aux (tl,[]))
              | _ ->
+*)
               let irl =
                 CicMkImplicit.identity_relocation_list_for_metavariable context
               in
@@ -237,7 +241,7 @@ let
                 (!next_fresh_meta,context,ty)::!newmetasenvfragment ;
                exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ;
                incr next_fresh_meta ;
-               subst_item::(aux (tl,[])))
+               subst_item::(aux (tl,[]))(*)*)
        | uri::tl1,((uri',_) as s)::tl2 ->
           assert (UriManager.eq uri uri') ;
           s::(aux (tl1,tl2))
@@ -250,7 +254,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
@@ -328,16 +332,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
@@ -354,7 +358,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
@@ -386,7 +390,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
@@ -410,7 +414,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
@@ -428,7 +432,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
@@ -571,7 +575,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 *)