Universes introduction

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 812094d5a41f24f603bbf7a3c86a922a08761af8..388ac2056ef6fb560480aa43ac91403a7b4a9404 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -160,12 +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
+(* 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
@@ -219,15 +220,16 @@ 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
+(* 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,[]))
@@ -461,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")