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
- if fst (CicReduction.are_convertible [] rel.rel_a (Cic.Appl (he'::args1)) CicUniv.empty_ugraph) then
+ if fst (CicReduction.are_convertible [] rel.rel_a (Cic.Appl (he'::args1))
+ CicUniv.oblivion_ugraph) then
args2
else
raise_error rel.rel_quantifiers_no
| _ ->
- if rel.rel_quantifiers_no = 0 && fst (CicReduction.are_convertible [] rel.rel_a t CicUniv.empty_ugraph) then
+ if rel.rel_quantifiers_no = 0 && fst (CicReduction.are_convertible []
+ rel.rel_a t CicUniv.oblivion_ugraph) then
[]
else
begin
(*COQ
let evars,args,instantiated_rel_a =
- let ty = CicTypeChecker.type_of_aux' [] [] rel.rel_a CicUniv.empty_ugraph in
+ let ty = CicTypeChecker.type_of_aux' [] [] rel.rel_a
+ CicUniv.oblivion_ugraph in
let evd = Evd.create_evar_defs Evd.empty in
let evars,args,concl =
Clenv.clenv_environments_evars env evd
let unify_relation_class_carrier_with_type env rel t =
match rel with
Leibniz (Some t') ->
- if fst (CicReduction.are_convertible [] t t' CicUniv.empty_ugraph) then
+ if fst (CicReduction.are_convertible [] t t' CicUniv.oblivion_ugraph) then
rel
else
raise (ProofEngineTypes.Fail (lazy
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 *)
- Cic.LetIn (Cic.Anonymous,c2,hyp)
+ Cic.LetIn (Cic.Anonymous,c2,assert false,hyp)
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 (_,metasenv,_,_) = proof in
+ let (_,metasenv,_subst,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
try
let relation_class =