diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6d08f66c1..a71ef6508 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -510,7 +510,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let tM = Stack.zip evd apprM in miller_pfenning on_left (fun () -> if not_only_app then (* Postpone the use of an heuristic *) - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM + switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM else quick_fail i) ev lF tM i and consume (termF,skF as apprF) (termM,skM as apprM) i = @@ -578,7 +578,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty i,mkEvar ev else i,Stack.zip evd apprF in - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) + switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) tF tR else UnifFailure (evd,OccurCheck (fst ev,tR)))]) @@ -984,9 +984,11 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) else UnifFailure(evd,(*dummy*)NotSameHead) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = + let open Declarations in let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite -> + | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite -> + let (_, projs, _) = info.(snd ind) in let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in |