diff options
| author | Hugo Herbelin | 2015-01-03 15:41:14 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-03 16:03:18 +0100 |
| commit | 353b523c0c808d0650cd77821363b0c865aedecf (patch) | |
| tree | 7ec71e045ed1d80b60d63b55b36e766344ab83c9 /pretyping | |
| parent | 3bd9cb26be01d0791fdf2dc56d3aacaa1379e50c (diff) | |
Fixing #3895 (thanks to PMP for diagnosis).
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 1a1cd92ed6..f8518beaa6 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1128,8 +1128,8 @@ let solve_evar_evar_aux f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) with CannotProject (evd,ev2) -> add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd -let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = - let (evd,ev1,ev2),pbty = +let solve_evar_evar ?(force=false) f g env evd pbty ev1 ev2 = + let (evd,(evk1,args1 as ev1),(evk2,args2 as ev2)),pbty = (* If an evar occurs in the instance of the other evar and the use of an heuristic is forced, we restrict *) if force then ensure_evar_independent g env evd ev1 ev2, None |