-
- let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
- let pos, equality = eq_found in
- let (_, proof', (ty, what, other, _), menv',id) =
- Equality.open_equality equality in
- let what, other = if pos = Utils.Left then what, other else other, what in
- let ty =
- try fst (CicTypeChecker.type_of_aux' menv' context what ugraph)
- with
- | CicUtil.Meta_not_found _
- | Invalid_argument("List.fold_left2") -> ty
- in
- let newterm, newgoalproof =
- let bo =
- Utils.guarded_simpl context (apply_subst subst(S.subst other t))
- in
- let bo' = (*apply_subst subst*) t in
- let name = C.Name "x" in
- incr demod_counter;
- let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
- bo, (newgoalproofstep::goalproof)
- in
- let newmetasenv = (* Inference.filter subst *) menv in
- !maxmeta, (newgoalproof, newmetasenv, newterm)
- in
- let res =
- demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term