summaryrefslogtreecommitdiff
path: root/pretyping/evarconv.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:28:35 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:28:35 +0200
commite4282ea99c664d8d58067bee199cbbcf881b60d5 (patch)
treed4c4a873eb055c728666f367469fa26c3417793a /pretyping/evarconv.ml
parenta0a94c1340a63cdb824507b973393882666ba52a (diff)
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'pretyping/evarconv.ml')
-rw-r--r--pretyping/evarconv.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4c5ebe3e..043a326d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evarconv.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: evarconv.ml 12205 2009-06-22 16:10:15Z barras $ *)
open Pp
open Util
@@ -474,11 +474,11 @@ and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
let (evd',ks,_) =
List.fold_left
(fun (i,ks,m) b ->
- if m=0 then (i,t2::ks, n-1) else
+ if m=n then (i,t2::ks, m-1) else
let dloc = (dummy_loc,InternalHole) in
let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
- (i', ev :: ks, n - 1))
- (evd,[],n) bs
+ (i', ev :: ks, m - 1))
+ (evd,[],List.length bs - 1) bs
in
ise_and evd'
[(fun i ->
@@ -505,7 +505,7 @@ let first_order_unification env evd (ev1,l1) (term2,l2) =
if is_defined_evar i ev1 then
evar_conv_x env i CONV t2 (mkEvar ev1)
else
- solve_simple_eqn evar_conv_x env i (CONV,ev1,t2))]
+ solve_simple_eqn ~choose:true evar_conv_x env i (CONV,ev1,t2))]
let choose_less_dependent_instance evk evd term args =
let evi = Evd.find (evars_of evd) evk in