diff options
| author | Maxime Dénès | 2017-11-23 17:36:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-23 17:36:03 +0100 |
| commit | 915554785ffed11370f5d700d11a8b5614408096 (patch) | |
| tree | 4b5b4120c896cf99c863fab4fd5e1ec22af20d53 /engine/evd.ml | |
| parent | ebe133a0df0656de82a566c4f1673257f60f7c0c (diff) | |
| parent | 9f47342d890dc3ef7f4950004513a47d940af5ca (diff) | |
Merge PR #6186: [api] Miscellaneous consolidation.
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 8d465384b1..60bd6de2ae 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -243,7 +243,7 @@ let evar_instance_array test_id info args = instrec filter (evar_context info) 0 let make_evar_instance_array info args = - evar_instance_array (NamedDecl.get_id %> Term.isVarId) info args + evar_instance_array (NamedDecl.get_id %> isVarId) info args let instantiate_evar_array info c args = let inst = make_evar_instance_array info args in @@ -707,10 +707,10 @@ let extract_all_conv_pbs evd = extract_conv_pbs evd (fun _ -> true) let loc_of_conv_pb evd (pbty,env,t1,t2) = - match kind (fst (Term.decompose_app t1)) with + match kind (fst (decompose_app t1)) with | Evar (evk1,_) -> fst (evar_source evk1 evd) | _ -> - match kind (fst (Term.decompose_app t2)) with + match kind (fst (decompose_app t2)) with | Evar (evk2,_) -> fst (evar_source evk2 evd) | _ -> None |