diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-12 18:12:45 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-15 19:18:41 +0100 |
| commit | 9aa416c0c66ad7e14c4704898b74b99237d81c78 (patch) | |
| tree | 7b2519a4aa91a80c6c2c6e463389b13bbc5fa47e /pretyping/unification.ml | |
| parent | 4fec6bdf0ad0f49c98a82538c5caf4511ba5e95c (diff) | |
Documenting check_record + changing a possibly undefined int into int option.
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3c89bf27a..7ea074b74 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -970,11 +970,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb let (evd,ks,_) = List.fold_left (fun (evd,ks,m) b -> - if Int.equal m n then (evd,t2::ks, m-1) else + if match n with Some n -> Int.equal m n | None -> false then + (evd,t2::ks, m-1) + else let mv = new_meta () in let evd' = meta_declare mv (substl ks b) evd in (evd', mkMeta mv :: ks, m - 1)) - (sigma,[],List.length bs - 1) bs + (sigma,[],List.length bs) bs in try let opt' = {opt with with_types = false} in |