(try
(match CicTypeChecker.type_of_aux' [] context typ with
C.Sort C.Prop -> "H"
+ | C.Sort C.CProp -> "H"
| C.Sort C.Set -> "x"
| _ -> "H"
)
try_next 1
;;
-(* identity_relocation_list_for_metavariable i canonical_context *)
-(* returns the identity relocation list, which is the list [1 ; ... ; n] *)
-(* where n = List.length [canonical_context] *)
-(*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
-let identity_relocation_list_for_metavariable canonical_context =
- let canonical_context_length = List.length canonical_context in
- let rec aux =
- function
- (_,[]) -> []
- | (n,None::tl) -> None::(aux ((n+1),tl))
- | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
- in
- aux (1,canonical_context)
-
-(* Returns the first meta whose number is above the *)
-(* number of the higher meta. *)
-let new_meta ~proof =
- let (_,metasenv,_,_) = proof in
- let rec aux =
- function
- None,[] -> 1
- | Some n,[] -> n
- | None,(n,_,_)::tl -> aux (Some n,tl)
- | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
- in
- 1 + aux (None,metasenv)
+let new_meta_of_proof ~proof:(_, metasenv, _, _) =
+ CicMkImplicit.new_meta metasenv
let subst_meta_in_proof proof meta term newmetasenv =
let uri,metasenv,bo,ty = proof in
- let subst_in = CicUnification.apply_subst [meta,term] in
+ let subst_in = CicMetaSubst.apply_subst [meta,term] in
let metasenv' =
newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
in
List.map
(function
Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
- | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s))
+ | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
| None -> None
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) canonical_context
in
i,canonical_context',(subst_in ty)
(function
None -> None
| Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
- | Some (i,Cic.Def t) -> Some (i,Cic.Def (subst_in t))
+ | Some (i,Cic.Def (t,None)) ->
+ Some (i,Cic.Def ((subst_in t),None))
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) canonical_context
in
(m,canonical_context',subst_in ty)::i