diff options
| author | Hugo Herbelin | 2015-07-03 21:13:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-08-02 19:13:51 +0200 |
| commit | 21525bae8801d98ff2f1b52217d7603505ada2d2 (patch) | |
| tree | c456d9401d98198d30bca1b2c6df5390b858f893 | |
| parent | b78d86d50727af61e0c4417cf2ef12cbfc73239d (diff) | |
Cosmetic in evarconv.ml: naming a local function for better readibility.
| -rw-r--r-- | pretyping/evarconv.ml | 35 |
1 files changed, 18 insertions, 17 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index bb07bf0563..4fed09d6f4 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -425,8 +425,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM else quick_fail i) ev lF tM i - and consume (termF,skF as apprF) (termM,skM as apprM) i = + and consume (termF,skF as apprF) (termM,skM as apprM) i = if not (Stack.is_empty skF && Stack.is_empty skM) then + (* This tries first-order matching *) consume_stack on_left apprF apprM i else quick_fail i and delta i = @@ -469,28 +470,28 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Construct u -> eta_constructor ts env evd skR u skF termF | _ -> UnifFailure (evd,NotSameHead) in + let postpone tR lF evd = + (* Postpone the use of an heuristic *) + if not (occur_rigidly (fst ev) evd tR) then + let evd,tF = + if isRel tR || isVar tR then + (* Optimization so as to generate candidates *) + let evd,ev = evar_absorb_arguments env evd ev lF in + evd,mkEvar ev + else + evd,Stack.zip apprF in + switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) evd)) + tF tR + else + UnifFailure (evd,OccurCheck (fst ev,tR)) + in match Stack.list_of_app_stack skF with | None -> ise_try evd [consume_stack on_left apprF apprR; eta] | Some lF -> let tR = Stack.zip apprR in miller_pfenning on_left - (fun () -> - ise_try evd - [eta;(* Postpone the use of an heuristic *) - (fun i -> - if not (occur_rigidly (fst ev) i tR) then - let i,tF = - if isRel tR || isVar tR then - (* Optimization so as to generate candidates *) - let i,ev = evar_absorb_arguments env i ev lF in - i,mkEvar ev - else - i,Stack.zip apprF in - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) - tF tR - else - UnifFailure (evd,OccurCheck (fst ev,tR)))]) + (fun () -> ise_try evd [eta;postpone tR lF]) ev lF tR evd in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in |