2 Declaration of Cic.name * Cic.term
3 | Definition of Cic.name * Cic.term
6 type metasenv = (int * Cic.term) list;;
8 type named_context = binder_type list;;
10 type sequent = named_context * Cic.term;;
13 ref (None : (UriManager.uri * metasenv * Cic.term * Cic.term) option)
15 (*CSC: Quando facciamo Clear di una ipotesi, cosa succede? *)
16 (* Note: the sequent is redundant: it can be computed from the type of the *)
17 (* metavariable and its context in the proof. We keep it just for efficiency *)
18 (* because computing the context of a term may be quite expensive. *)
19 let goal = ref (None : (int * sequent) option);;
21 exception NotImplemented
23 let cic_context_of_named_context =
26 Declaration (_,t) -> Cic.Decl t
27 | Definition (_,t) -> Cic.Def t
31 (* refine_meta_with_brand_new_metasenv meta term apply_subst_replacing *)
33 (* This (heavy) function must be called when a tactic can instantiate old *)
34 (* metavariables (i.e. existential variables). It substitues the metasenv *)
35 (* of the proof with the result of removing [meta] from the domain of *)
36 (* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
37 (* in the current proof. Finally it applies [apply_subst_replacing] to *)
39 (*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
40 (*CSC: ci ripasso sopra apply_subst!!! *)
41 (*CSC: Inoltre, potrebbe essere questa funzione ad applicare apply_subst a *)
42 (*CSC: newmetasenv!!! *)
43 let refine_meta_with_brand_new_metasenv meta term apply_subst_replacing
49 | Some (uri,_,bo,ty) -> uri,bo,ty
52 ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t
54 let bo' = apply_subst_replacing (subst_in bo) in
55 let metasenv' = List.remove_assoc meta newmetasenv in
56 proof := Some (uri,metasenv',bo',ty)
59 let refine_meta meta term newmetasenv =
60 let (uri,metasenv,bo,ty) =
63 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
66 ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t
68 let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in
69 let metasenv'' = List.map (function i,ty -> i,(subst_in ty)) metasenv' in
70 let bo' = subst_in bo in
71 proof := Some (uri,metasenv'',bo',ty)
74 (* Returns the first meta whose number is above the *)
75 (* number of the higher meta. *)
80 | Some (_,metasenv,_,_) -> metasenv
86 | None,(n,_)::tl -> aux (Some n,tl)
87 | Some m,(n,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
89 1 + aux (None,metasenv)
92 (* metas_in_term term *)
93 (* Returns the ordered list of the metas that occur in [term]. *)
94 (* Duplicates are removed. The implementation is not very efficient. *)
95 let metas_in_term term =
104 | C.Cast (te,ty) -> (aux te) @ (aux ty)
105 | C.Prod (_,s,t) -> (aux s) @ (aux t)
106 | C.Lambda (_,s,t) -> (aux s) @ (aux t)
107 | C.LetIn (_,s,t) -> (aux s) @ (aux t)
108 | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
112 | C.MutConstruct _ -> []
113 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
114 (aux outt) @ (aux t) @
115 (List.fold_left (fun i t -> i @ (aux t)) [] pl)
117 List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
119 List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
121 let metas = aux term in
122 let rec elim_duplicates =
126 he::(elim_duplicates (List.filter (function el -> he <> el) tl))
128 elim_duplicates metas
131 (* perforate context term ty *)
132 (* replaces the term [term] in the proof with a new metavariable whose type *)
133 (* is [ty]. [context] must be the context of [term] in the whole proof. This *)
134 (* could be easily computed; so the only reasons to have it as an argument *)
135 (* are efficiency reasons. *)
136 let perforate context term ty =
137 let module C = Cic in
138 let newmeta = new_meta () in
141 | Some (uri,metasenv,bo,gty) ->
142 (* We push the new meta at the end of the list for pretty-printing *)
143 (* purposes: in this way metas are ordered. *)
144 let metasenv' = metasenv@[newmeta,ty] in
145 let bo' = ProofEngineReduction.replace term (C.Meta newmeta) bo in
146 (* It may be possible that some metavariables occurred only in *)
147 (* the term we are perforating and they now occurs no more. We *)
148 (* get rid of them, collecting the really useful metavariables *)
150 let newmetas = metas_in_term bo' in
152 List.filter (function (n,_) -> List.mem n newmetas) metasenv'
154 proof := Some (uri,metasenv'',bo',gty) ;
155 goal := Some (newmeta,(context,ty)) ;
159 (************************************************************)
160 (* Some easy tactics. *)
161 (************************************************************)
163 exception Fail of string;;
165 (* lambda_abstract newmeta ty *)
166 (* returns a triple [bo],[context],[ty'] where *)
167 (* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *)
168 (* and [bo] = Lambda/LetIn [context].(Meta [newmeta]) *)
169 (* So, lambda_abstract is the core of the implementation of *)
170 (* the Intros tactic. *)
171 let lambda_abstract newmeta ty =
172 let module C = Cic in
173 let rec collect_context =
175 C.Cast (te,_) -> collect_context te
177 let (ctx,ty,bo) = collect_context t in
181 (*CSC: generatore di nomi? Chiedere il nome? *)
182 | C.Anonimous -> C.Name "fresh_name"
184 ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo))
186 let (ctx,ty,bo) = collect_context t in
187 ((Definition (n,s))::ctx,ty,C.LetIn(n,s,bo))
188 | _ as t -> [], t, (C.Meta newmeta)
190 let revcontext,ty',bo = collect_context ty in
191 bo,(List.rev revcontext),ty'
195 let module C = Cic in
196 let module R = CicReduction in
200 | Some (_,metasenv,_,_) -> metasenv
202 let (metano,context,ty) =
205 | Some (metano,(context,ty)) -> metano,context,ty
207 let newmeta = new_meta () in
208 let (bo',newcontext,ty') = lambda_abstract newmeta ty in
209 let context'' = newcontext @ context in
210 refine_meta metano bo' [newmeta,ty'] ;
211 goal := Some (newmeta,(context'',ty'))
214 (* The term bo must be closed in the current context *)
216 let module T = CicTypeChecker in
217 let module R = CicReduction in
221 | Some (_,metasenv,_,_) -> metasenv
223 let (metano,context,ty) =
226 | Some (metano,(context,ty)) ->
227 assert (ty = List.assoc metano metasenv) ;
228 (* Invariant: context is the actual context of the meta in the proof *)
231 let context = cic_context_of_named_context context in
232 if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
234 refine_meta metano bo [] ;
238 raise (Fail "The type of the provided term is not the one expected.")
241 (*CSC: The call to the Intros tactic is embedded inside the code of the *)
242 (*CSC: Elim tactic. Do we already need tacticals? *)
243 (* Auxiliary function for apply: given a type (a backbone), it returns its *)
244 (* head, a META environment in which there is new a META for each hypothesis,*)
245 (* a list of arguments for the new applications and the indexes of the first *)
246 (* and last new METAs introduced. The nth argument in the list of arguments *)
247 (* is the nth new META lambda-abstracted as much as possible. Hence, this *)
248 (* functions already provides the behaviour of Intros on the new goals. *)
249 let new_metasenv_for_apply_intros ty =
250 let module C = Cic in
251 let module S = CicSubstitution in
252 let rec aux newmeta =
254 C.Cast (he,_) -> aux newmeta he
256 let newargument,newcontext,ty' = lambda_abstract newmeta s in
257 let (res,newmetasenv,arguments,lastmeta) =
258 aux (newmeta + 1) (S.subst newargument t)
260 res,(newmeta,ty')::newmetasenv,newargument::arguments,lastmeta
261 | t -> t,[],[],newmeta
263 let newmeta = new_meta () in
264 (* WARNING: here we are using the invariant that above the most *)
265 (* recente new_meta() there are no used metas. *)
266 let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
267 res,newmetasenv,arguments,newmeta,lastmeta
270 (* Auxiliary function for apply: given a type (a backbone), it returns its *)
271 (* head, a META environment in which there is new a META for each hypothesis,*)
272 (* a list of arguments for the new applications and the indexes of the first *)
273 (* and last new METAs introduced. The nth argument in the list of arguments *)
274 (* is just the nth new META. *)
275 let new_metasenv_for_apply ty =
276 let module C = Cic in
277 let module S = CicSubstitution in
278 let rec aux newmeta =
280 C.Cast (he,_) -> aux newmeta he
282 let newargument = C.Meta newmeta in
283 let (res,newmetasenv,arguments,lastmeta) =
284 aux (newmeta + 1) (S.subst newargument t)
286 res,(newmeta,s)::newmetasenv,newargument::arguments,lastmeta
287 | t -> t,[],[],newmeta
289 let newmeta = new_meta () in
290 (* WARNING: here we are using the invariant that above the most *)
291 (* recente new_meta() there are no used metas. *)
292 let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
293 res,newmetasenv,arguments,newmeta,lastmeta
297 (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
298 let classify_metas newmeta in_subst_domain apply_subst metasenv =
300 (fun (i,ty) (old_uninst,new_uninst) ->
301 if in_subst_domain i then
302 old_uninst,new_uninst
304 let ty' = apply_subst ty in
306 ((i,ty')::old_uninst),new_uninst
308 old_uninst,((i,ty')::new_uninst)
312 (* The term bo must be closed in the current context *)
314 let module T = CicTypeChecker in
315 let module R = CicReduction in
316 let module C = Cic in
320 | Some (_,metasenv,_,_) -> metasenv
322 let (metano,context,ty) =
325 | Some (metano,(context,ty)) ->
326 assert (ty = List.assoc metano metasenv) ;
327 (* Invariant: context is the actual context of the meta in the proof *)
330 let ciccontext = cic_context_of_named_context context in
331 let termty = CicTypeChecker.type_of_aux' metasenv ciccontext term in
332 (* newmeta is the lowest index of the new metas introduced *)
333 let (consthead,newmetas,arguments,newmeta,_) =
334 new_metasenv_for_apply termty
336 let newmetasenv = newmetas@metasenv in
337 let subst = CicUnification.fo_unif newmetasenv ciccontext consthead ty in
338 let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
339 let apply_subst = CicUnification.apply_subst subst in
340 (*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
341 let apply_subst_replacing t =
344 ProofEngineReduction.replace
345 ~what:(Cic.Meta i) ~with_what:bo ~where:t)
348 let old_uninstantiatedmetas,new_uninstantiatedmetas =
349 classify_metas newmeta in_subst_domain apply_subst newmetasenv
352 if List.length newmetas = 0 then
355 let arguments' = List.map apply_subst arguments in
356 Cic.Appl (term::arguments')
358 refine_meta_with_brand_new_metasenv metano bo' apply_subst_replacing
359 (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
360 match new_uninstantiatedmetas with
362 | (i,ty)::_ -> goal := Some (i,(context,ty))
365 let eta_expand metasenv ciccontext t arg =
366 let module T = CicTypeChecker in
367 let module S = CicSubstitution in
368 let module C = Cic in
371 t' when t' = S.lift n arg -> C.Rel (1 + n)
372 | C.Rel m -> if m <= n then C.Rel m else C.Rel (m+1)
376 | C.Implicit as t -> t
377 | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
378 | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
379 | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
380 | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
381 | C.Appl l -> C.Appl (List.map (aux n) l)
382 | C.Const _ as t -> t
383 | C.Abst _ -> assert false
385 | C.MutConstruct _ as t -> t
386 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
387 C.MutCase (sp,cookingsno,i,aux n outt, aux n t,
390 let tylen = List.length fl in
393 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
396 C.Fix (i, substitutedfl)
398 let tylen = List.length fl in
401 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
404 C.CoFix (i, substitutedfl)
407 T.type_of_aux' metasenv ciccontext arg
409 (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg])
412 exception NotAnInductiveTypeToEliminate;;
413 exception NotTheRightEliminatorShape;;
414 exception NoHypothesesFound;;
416 let elim_intros term =
417 let module T = CicTypeChecker in
418 let module U = UriManager in
419 let module R = CicReduction in
420 let module C = Cic in
424 | Some (curi,metasenv,_,_) -> curi,metasenv
426 let (metano,context,ty) =
429 | Some (metano,(context,ty)) ->
430 assert (ty = List.assoc metano metasenv) ;
431 (* Invariant: context is the actual context of the meta in the proof *)
434 let ciccontext = cic_context_of_named_context context in
435 let termty = T.type_of_aux' metasenv ciccontext term in
436 let uri,cookingno,typeno,args =
438 C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
439 | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
440 (uri,cookingno,typeno,args)
441 | _ -> raise NotAnInductiveTypeToEliminate
444 let buri = U.buri_of_uri uri in
446 match CicEnvironment.get_cooked_obj uri cookingno with
447 C.InductiveDefinition (tys,_,_) ->
448 let (name,_,_,_) = List.nth tys typeno in
453 match T.type_of_aux' metasenv ciccontext ty with
454 C.Sort C.Prop -> "_ind"
455 | C.Sort C.Set -> "_rec"
456 | C.Sort C.Type -> "_rect"
459 U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
461 let eliminator_cookingno =
462 UriManager.relative_depth curi eliminator_uri 0
464 let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
466 T.type_of_aux' [] [] eliminator_ref
468 let (econclusion,newmetas,arguments,newmeta,lastmeta) =
469 new_metasenv_for_apply ety
471 (* Here we assume that we have only one inductive hypothesis to *)
472 (* eliminate and that it is the last hypothesis of the theorem. *)
473 (* A better approach would be fingering the hypotheses in some *)
475 let meta_of_corpse = Cic.Meta (lastmeta - 1) in
476 let newmetasenv = newmetas @ metasenv in
477 prerr_endline ("ECONCLUSION: " ^ CicPp.ppterm econclusion) ;
480 CicUnification.fo_unif newmetasenv ciccontext term meta_of_corpse
482 let ueconclusion = CicUnification.apply_subst subst1 econclusion in
483 prerr_endline ("ECONCLUSION DOPO UNWIND: " ^ CicPp.ppterm ueconclusion) ;
485 (* The conclusion of our elimination principle is *)
486 (* (?i farg1 ... fargn) *)
487 (* The conclusion of our goal is ty. So, we can *)
488 (* eta-expand ty w.r.t. farg1 .... fargn to get *)
489 (* a new ty equal to (P farg1 ... fargn). Now *)
490 (* ?i can be instantiated with P and we are ready *)
491 (* to refine the term. *)
493 match ueconclusion with
494 (*CSC: Code to be used for Apply *)
495 C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs
496 | C.Meta emeta -> emeta,[]
497 (*CSC: Code to be used for ApplyIntros
498 C.Appl (he::fargs) ->
501 C.Meta emeta -> emeta
502 | C.Lambda (_,_,t) -> find_head t
503 | C.LetIn (_,_,t) -> find_head t
504 | _ ->raise NotTheRightEliminatorShape
508 | _ -> raise NotTheRightEliminatorShape
510 let ty' = CicUnification.apply_subst subst1 ty in
511 let eta_expanded_ty =
512 List.fold_left (eta_expand metasenv ciccontext) ty' fargs
514 prerr_endline ("ETAEXPANDEDTY:" ^ CicPp.ppterm eta_expanded_ty) ; flush stdout ;
516 (*CSC: passo newmetasenv, ma alcune variabili sono gia' state sostituite
517 da subst1!!!! Dovrei rimuoverle o sono innocue?*)
518 CicUnification.fo_unif
519 newmetasenv ciccontext ueconclusion eta_expanded_ty
521 prerr_endline "Dopo la seconda unificazione" ; flush stdout ;
522 prerr_endline "unwind"; flush stderr;
523 let in_subst_domain i =
524 let eq_to_i = function (j,_) -> i=j in
525 List.exists eq_to_i subst1 ||
526 List.exists eq_to_i subst2
528 (* When unwinding the META that corresponds to the elimination *)
529 (* predicate (which is emeta), we must also perform one-step *)
530 (* beta-reduction. *)
532 let t' = CicUnification.apply_subst subst1 t in
533 CicUnification.apply_subst_reducing
534 subst2 (Some (emeta,List.length fargs)) t'
536 (*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
537 let apply_subst_replacing t =
541 ProofEngineReduction.replace
542 ~what:(Cic.Meta i) ~with_what:bo ~where:t)
547 ProofEngineReduction.replace
548 ~what:(Cic.Meta i) ~with_what:bo ~where:t)
552 List.map (function (i,ty) -> i, apply_subst ty) newmetasenv
554 let old_uninstantiatedmetas,new_uninstantiatedmetas =
555 classify_metas newmeta in_subst_domain apply_subst newmetasenv
557 let arguments' = List.map apply_subst arguments in
558 let bo' = Cic.Appl (eliminator_ref::arguments') in
559 prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ;
560 List.iter (function (i,t) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm t)) (new_uninstantiatedmetas@old_uninstantiatedmetas) ; flush stderr ;
561 refine_meta_with_brand_new_metasenv metano bo'
562 apply_subst_replacing
563 (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
564 match new_uninstantiatedmetas with
566 | (i,ty)::_ -> goal := Some (i,(context,ty))
569 let reduction_tactic reduction_function term =
570 let curi,metasenv,pbo,pty =
573 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
575 let (metano,context,ty) =
578 | Some (metano,(context,ty)) -> metano,context,ty
580 let term' = reduction_function term in
581 (* We don't know if [term] is a subterm of [ty] or a subterm of *)
582 (* the type of one metavariable. So we replace it everywhere. *)
583 (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
584 (*CSC: che si guadagni nulla in fatto di efficienza. *)
585 let replace = ProofEngineReduction.replace ~what:term ~with_what:term' in
586 let ty' = replace ty in
590 Definition (n,t) -> Definition (n,replace t)
591 | Declaration (n,t) -> Declaration (n,replace t)
597 (n,_) when n = metano -> (metano,ty')
601 proof := Some (curi,metasenv',pbo,pty) ;
602 goal := Some (metano,(context',ty'))
605 let reduction_tactic_in_scratch reduction_function ty term =
609 | Some (_,metasenv,_,_) -> metasenv
614 | Some (_,(context,_)) -> context
616 let term' = reduction_function term in
617 ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty
620 let whd = reduction_tactic CicReduction.whd;;
621 let reduce = reduction_tactic ProofEngineReduction.reduce;;
622 let simpl = reduction_tactic ProofEngineReduction.simpl;;
624 let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd;;
625 let reduce_in_scratch =
626 reduction_tactic_in_scratch ProofEngineReduction.reduce;;
627 let simpl_in_scratch =
628 reduction_tactic_in_scratch ProofEngineReduction.simpl;;
630 (* It is just the opposite of whd. The code should probably be merged. *)
632 let curi,metasenv,pbo,pty =
635 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
637 let (metano,context,ty) =
640 | Some (metano,(context,ty)) -> metano,context,ty
642 let term' = CicReduction.whd term in
643 (* We don't know if [term] is a subterm of [ty] or a subterm of *)
644 (* the type of one metavariable. So we replace it everywhere. *)
645 (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
646 (*CSC: che si guadagni nulla in fatto di efficienza. *)
647 let replace = ProofEngineReduction.replace ~what:term' ~with_what:term in
648 let ty' = replace ty in
652 Declaration (n,t) -> Declaration (n,replace t)
653 | Definition (n,t) -> Definition (n,replace t)
659 (n,_) when n = metano -> (metano,ty')
663 proof := Some (curi,metasenv',pbo,pty) ;
664 goal := Some (metano,(context',ty'))
668 let module C = Cic in
669 let curi,metasenv,pbo,pty =
672 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
674 let (metano,context,ty) =
677 | Some (metano,(context,ty)) -> metano,context,ty
679 let newmeta1 = new_meta () in
680 let newmeta2 = newmeta1 + 1 in
681 let newmeta1ty = CicSubstitution.lift 1 ty in
684 [C.Lambda (C.Name "dummy_for_cut",term,C.Meta newmeta1) ;
687 prerr_endline ("BO': " ^ CicPp.ppterm bo') ; flush stderr ;
688 refine_meta metano bo' [newmeta2,term; newmeta1,newmeta1ty];
691 (newmeta1,((Declaration (C.Name "dummy_for_cut", term))::context,
696 let module C = Cic in
697 let curi,metasenv,pbo,pty =
700 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
702 let (metano,context,ty) =
705 | Some (metano,(context,ty)) -> metano,context,ty
707 let ciccontext = cic_context_of_named_context context in
708 let _ = CicTypeChecker.type_of_aux' metasenv ciccontext term in
709 let newmeta = new_meta () in
710 let newmetaty = CicSubstitution.lift 1 ty in
711 let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta newmeta) in
712 refine_meta metano bo' [newmeta,newmetaty];
716 ((Definition (C.Name "dummy_for_letin", term))::context, newmetaty))
719 exception NotConvertible;;
721 (*CSC: Bug (or feature?). [input] is parsed in the context of the goal, *)
722 (*CSC: while [goal_input] can have a richer context (because of binders) *)
723 (*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
724 (*CSC: Is that evident? Is that right? Or should it be changed? *)
725 let change ~goal_input ~input =
726 let curi,metasenv,pbo,pty =
729 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
731 let (metano,context,ty) =
734 | Some (metano,(context,ty)) -> metano,context,ty
736 let ciccontext = cic_context_of_named_context context in
737 (* are_convertible works only on well-typed terms *)
738 ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ;
739 if CicReduction.are_convertible goal_input input then
741 let ty' = ProofEngineReduction.replace goal_input input ty in
745 (n,_) when n = metano -> (metano,ty')
749 proof := Some (curi,metasenv',pbo,pty) ;
750 goal := Some (metano,(context,ty'))