diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-23 15:52:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-23 15:52:48 +0200 |
| commit | ddd99ca6b4a23286405ec995379e4b07d42b0f78 (patch) | |
| tree | e2e328b78d9fca7383973bf46014410ea08bac4f /pretyping | |
| parent | 38b180984b09840e0b1023cc441917acc77dd438 (diff) | |
| parent | 994f869496b3edd76a903cac16b13e8b6f247d63 (diff) | |
Merge PR #7827: [engine] safe [add_unification_pb] interface
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 88a91af88..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)))]) |