From 62792f5bfe558e6ba0e52e4e51841f4bc02a960a Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 24 Mar 2004 16:52:15 +0000
Subject: [PATCH] CSC: hack to make applications of constants that have a Type
 sort which occurs in contravariant position work. The idea is to generate in
 place of a metavariable of type Type (that should be of type <Type) a
 metavariable of type "a metavariable of type Type". The problem is that in
 this way the metavariable can also be instantiated that is not a sort.

---
 helm/ocaml/tactics/primitiveTactics.ml | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 1de72fb5d..1631e767f 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -160,6 +160,21 @@ let new_metasenv_for_apply newmeta proof context ty =
   let rec aux newmeta =
    function
       C.Cast (he,_) -> aux newmeta he
+      (* 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) ->
+       let irl =
+         CicMkImplicit.identity_relocation_list_for_metavariable context
+       in
+        let newargument = C.Meta (newmeta+1,irl) in
+         let (res,newmetasenv,arguments,lastmeta) =
+          aux (newmeta + 2) (S.subst newargument t)
+         in
+          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
@@ -275,7 +290,7 @@ let apply_tac ~term ~status:(proof, goal) =
     in
      let newmetasenv = metasenv'@newmetas in
       let subst,newmetasenv' =
-       CicUnification.fo_unif newmetasenv context consthead ty
+        CicUnification.fo_unif newmetasenv context consthead ty
       in
        let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
        let apply_subst = CicMetaSubst.apply_subst subst in
-- 
2.39.2