let argsno = List.length args' - rel.rel_quantifiers_no in
let args1 = list_sub args' 0 argsno in
let args2 = list_sub args' argsno rel.rel_quantifiers_no in
let argsno = List.length args' - rel.rel_quantifiers_no in
let args1 = list_sub args' 0 argsno in
let args2 = list_sub args' argsno rel.rel_quantifiers_no in
let hyp = CicSubstitution.subst (CicSubstitution.lift 1 c2) hyp in
(* Since CicSubstitution.subst has killed Rel 1 and decreased the other Rels,
Rel 1 is now coding for c2, we can build the let-in factorizing c2 *)
let hyp = CicSubstitution.subst (CicSubstitution.lift 1 c2) hyp in
(* Since CicSubstitution.subst has killed Rel 1 and decreased the other Rels,
Rel 1 is now coding for c2, we can build the let-in factorizing c2 *)
in
let new_hyp = (*COQ Termops.replace_term c1 c2 hyp*) assert false in
let oppdir = opposite_direction direction in
in
let new_hyp = (*COQ Termops.replace_term c1 c2 hyp*) assert false in
let oppdir = opposite_direction direction in
let setoid_reflexivity_tac =
let tac ((proof,goal) as status) =
let setoid_reflexivity_tac =
let tac ((proof,goal) as status) =
- let (_,metasenv,_,_, _) = proof in
+ let (_,metasenv,_subst,_,_, _) = proof in