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

It is interesting to understand whether it is still necessary (after
the CicUnification bug fix) or not.

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 30d08c9bd76f7cdb52758a816c2dd653f422ef68..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))