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 30d08c9bd76f7cdb52758a816c2dd653f422ef68..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,18 +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 ->
+               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',[]) 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
@@ -237,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))
@@ -457,7 +463,7 @@ let elim_tac ~term (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")