in
(newproof,
List.map (function (i,_,_) -> i) new_uninstantiatedmetas)
+
+
+exception NotConvertible
+
+(*CSC: Bug (or feature?). [with_what] is parsed in the context of the goal, *)
+(*CSC: while [what] can have a richer context (because of binders) *)
+(*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *)
+(*CSC: Is that evident? Is that right? Or should it be changed? *)
+let change_tac ~what ~with_what ~status:(proof, goal) =
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ (* are_convertible works only on well-typed terms *)
+ ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ;
+ if CicReduction.are_convertible context what with_what then
+ begin
+ let replace =
+ ProofEngineReduction.replace ~equality:(==) ~what ~with_what
+ in
+ let ty' = replace ty in
+ let context' =
+ List.map
+ (function
+ Some (name,Cic.Def t) -> Some (name,Cic.Def (replace t))
+ | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
+ | None -> None
+ ) context
+ in
+ let metasenv' =
+ List.map
+ (function
+ (n,_,_) when n = metano -> (metano,context',ty')
+ | _ as t -> t
+ ) metasenv
+ in
+ (curi,metasenv',pbo,pty), [metano]
+ end
+ else
+ raise (ProofEngineTypes.Fail "Not convertible")