From 9b3e404f92b716d704e053c7d3011b09ddf55d24 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 22 Apr 2004 12:38:16 +0000 Subject: [PATCH] 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. --- helm/ocaml/tactics/primitiveTactics.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 30d08c9bd..812094d5a 100644 --- 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)) -- 2.39.2