first moogle template checkin

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 55b9d2e420ec8def3d11fd93902dfe1bb320486c..388ac2056ef6fb560480aa43ac91403a7b4a9404 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -160,11 +160,13 @@ 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 to simulate ?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
       * type Type to be different from a Sort!!! *)
-    | C.Prod (name,(C.Sort C.Type as s),t) ->
+    | C.Prod (name,(C.Sort (C.Type _) as s),t) ->
+       (* TASSI: ask CSC if BUG HERE refers to the C.Cast or C.Propd case *)
        let irl =
          CicMkImplicit.identity_relocation_list_for_metavariable context
        in
@@ -175,6 +177,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,21 +220,21 @@ 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 to simulate ?1 :< Type
            (match ty with
-               C.Sort C.Type as s ->
-                let irl =
-                  CicMkImplicit.identity_relocation_list_for_metavariable context
-                in
+               C.Sort (C.Type _) as s -> (* TASSI: ?? *)
                  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.Sort (C.Type (CicUniv.fresh()))) ::
+                    (* TASSI: ?? *)
                      (fresh_meta',[],C.Meta (fresh_meta,[])) :: !newmetasenvfragment ;
                    exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ;
                    subst_item::(aux (tl,[]))
              | _ ->
+*)
               let irl =
                 CicMkImplicit.identity_relocation_list_for_metavariable context
               in
@@ -240,7 +243,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))
@@ -253,7 +256,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 +334,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 +360,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 +392,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 +416,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 +434,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
@@ -460,7 +463,7 @@ let elim_tac ~term ~status:(proof, goal) =
          C.Sort C.Prop -> "_ind"
        | C.Sort C.Set  -> "_rec"
        | C.Sort C.CProp -> "_rec"
-       | C.Sort C.Type -> "_rect"
+       | C.Sort (C.Type _)-> "_rect" (* TASSI *)
        | _ -> assert false
      in
       U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
@@ -574,7 +577,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 *)